Lean 4 Built-in Tactic Reference for Proof Writing

a b : Nat
h : a < b
⊢ a ≤ b

theorem forall_imp (p q : α → Prop) : (∀ x, p x) → (∀ x, p x → q x) → ∀ x, q x := by
  intro hall hpq x
  exact hpq x (hall x)

-- intros introduces all binders at once, giving inaccessible names
example (p q : Prop) : p → q → p := by
  intros
  assumption

-- Introducing a pair: splits it into components
example : ∀ p : Nat × Nat, p.1 + p.2 = p.2 + p.1 := by
  intro (a, b)   -- destructs the pair into a and b
  omega

theorem exact_example (p : Prop) (hp : p) : p := by
  exact hp

theorem assumption_example (p q : Prop) (hp : p) (hq : q) : q := by
  assumption

example : True := by trivial
example : 1 ≠ 2 := by trivial

theorem contradiction_example (p : Prop) (hp : p) (hnp : ¬p) : False := by
  contradiction

theorem absurd_example (h : 0 = 1) : False := by
  contradiction

theorem apply_example (p q r : Prop) (h₁ : p → q) (h₂ : q → r) (hp : p) : r := by
  apply h₂
  apply h₁
  exact hp

theorem refine_example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  refine ⟨?_, ?_⟩
  · exact hp
  · exact hq

theorem rw_example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
  rw [h]

theorem rw_symm_example (a b : Nat) (h : a = b) : b + 1 = a + 1 := by
  rw [← h]

theorem simp_example (n : Nat) : n + 0 = n := by simp
theorem simp_list : [1, 2, 3].length = 3 := by simp

-- simp only is precise and faster for large goals
theorem simp_only_example (a b : Nat) (h : a = b) : a + 0 = b := by
  simp only [Nat.add_zero, h]

theorem omega_nat (n m : Nat) (h : n + m = 10) : m ≤ 10 := by omega

theorem omega_int (x y : Int) (h₁ : x > 0) (h₂ : y > 0) : x + y > 1 := by omega

theorem omega_mod (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 := by omega

theorem grind_example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by grind

theorem grind_logic (p q : Prop) (hp : p) (hq : q) : p ∧ q := by grind

theorem grind_arith (n m : Nat) (h₁ : n ≤ m) (h₂ : m ≤ n) : n = m := by grind

theorem lia_example (x y : Int) (h₁ : x ≥ 0) (h₂ : y ≥ 0) (h₃ : x + y ≤ 5) :
    x ≤ 5 := by lia

theorem lia_nat (n m : Nat) (h : n + m = 10) : m ≤ 10 := by lia

theorem decide_example : 2 + 2 = 4 := by decide
theorem decide_ne : 1 ≠ 2 := by decide
theorem decide_list : [1, 2, 3].contains 2 = true := by decide

theorem cases_example (p q : Prop) (h : p ∨ q) : q ∨ p := by
  cases h with
  | inl hp => right; exact hp
  | inr hq => left; exact hq

theorem cases_nat (n : Nat) : n = 0 ∨ ∃ m, n = m + 1 := by
  cases n with
  | zero => left; rfl
  | succ m => right; exact ⟨m, rfl⟩

theorem rcases_and (h : p ∧ q ∧ r) : r := by
  rcases h with ⟨_, _, hr⟩
  exact hr

theorem rcases_or (h : p ∨ q ∨ r) : r ∨ p ∨ q := by
  rcases h with hp | hq | hr
  · exact Or.inr (Or.inl hp)
  · exact Or.inr (Or.inr hq)
  · exact Or.inl hr

theorem obtain_exists (h : ∃ n : Nat, n > 5) : ∃ n : Nat, n > 0 := by
  obtain ⟨n, hn⟩ := h
  exact ⟨n, by omega⟩

theorem induction_example (n : Nat) : 0 + n = n := by
  induction n with
  | zero      => rfl
  | succ n ih => simp [Nat.add_succ, ih]

-- induction with explicit induction principle
theorem induction_on_list (l : List α) : l.length + 0 = l.length := by
  induction l with
  | nil        => rfl
  | cons x xs ih => simp [List.length_cons, ih]

theorem constructor_and (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp
  · exact hq

theorem left_example (hp : p) : p ∨ q := by left; exact hp

theorem use_example : ∃ n : Nat, n * n = 9 := by
  exact ⟨3, by decide⟩

-- The `exists` tactic macro:
theorem exists_tac : ∃ n : Nat, n > 100 := by
  exists 101

theorem have_example (n : Nat) (h : n > 5) : n > 3 := by
  have h' : n > 4 := by omega
  omega

theorem suffices_example (n : Nat) : n + 2 > n := by
  suffices h : n + 1 > n by omega
  omega

theorem show_example (n : Nat) : n + 0 = n := by
  show n = n  -- 0-add normalizes
  rfl

theorem conv_example (a b : Nat) : a + b = b + a := by
  conv_lhs => rw [Nat.add_comm]

-- Rewrite only the left-hand side of an inner addition
theorem conv_inner (a b c : Nat) : (a + b) + c = (b + a) + c := by
  conv_lhs => rw [Nat.add_comm a b]