Theorem Proving in Lean 4

https://lean-lang.org/theorem_proving_in_lean4
Admin
Theorem Proving in Lean 4 is a comprehensive guide to developing and verifying proofs using Lean, an...
Tokens:110,958
Snippets:922
Trust Score:10
Update:3 months ago
Show doc for...
Tokens:
Raw
### Implicit Lambda Examples

Source: https://lean-lang.org/theorem_proving_in_lean4/Interacting-with-Lean

Examples showing how to define functions with implicit arguments and how to disable implicit lambda introduction.

```lean
set_option linter.unusedVariables false namespace Ex2 
def id1 : {α : Type} → α → α := fun x => x 
def listId : List ({α : Type} → α → α) := (fun x => x) :: [] 
-- In this example, implicit lambda introduction has been disabled because 
-- we use `@` before {kw}fun def id2 : {α : Type} → α → α := @fun α (x : α) => id1 x 
def id3 : {α : Type} → α → α := @fun α x => id1 x 
def id4 : {α : Type} → α → α := fun x => id1 x 
-- In this example, implicit lambda introduction has been disabled 
-- because we used the binder annotation `{...}` def id5 : {α : Type} → α → α := fun {α} x => id1 x 
end Ex2
```

--------------------------------

### Implicit Lambda Configuration

Source: https://lean-lang.org/theorem_proving_in_lean4/Interacting-with-Lean

Setup for demonstrating implicit lambda behavior in Lean.

```lean
variable (ρ : Type) (m : Type → Type) [Monad m] 
instance : Monad (ReaderT ρ m) where pure := ReaderT.pure bind := ReaderT.bind
```

--------------------------------

### Apply simp with specific configurations

Source: https://lean-lang.org/theorem_proving_in_lean4/Tactics

Examples showing how to use simp with different arguments to control simplification behavior.

```lean
example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := by
xs:List Nat
ys:List Nat
p:List Nat → Prop
h:p (xs ++ mk_symm ys).reverse
⊢ p (mk_symm ys ++ xs.reverse) 
simp at h
xs:List Nat
ys:List Nat
p:List Nat → Prop
h:p (mk_symm ys ++ xs.reverse)
⊢ p (mk_symm ys ++ xs.reverse); assumption
All goals completed! 🐙
```

```lean
example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p ((mk_symm ys).reverse ++ xs.reverse) := by
xs:List Nat
ys:List Nat
p:List Nat → Prop
h:p (xs ++ mk_symm ys).reverse
⊢ p ((mk_symm ys).reverse ++ xs.reverse) 
simp [-reverse_mk_symm] at h
xs:List Nat
ys:List Nat
p:List Nat → Prop
h:p ((mk_symm ys).reverse ++ xs.reverse)
⊢ p ((mk_symm ys).reverse ++ xs.reverse); assumption
All goals completed! 🐙
```

```lean
example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p ((mk_symm ys).reverse ++ xs.reverse) := by
xs:List Nat
ys:List Nat
p:List Nat → Prop
h:p (xs ++ mk_symm ys).reverse
⊢ p ((mk_symm ys).reverse ++ xs.reverse) 
simp only [List.reverse_append] at h
xs:List Nat
ys:List Nat
p:List Nat → Prop
h:p ((mk_symm ys).reverse ++ xs.reverse)
⊢ p ((mk_symm ys).reverse ++ xs.reverse); assumption
All goals completed! 🐙
```

--------------------------------

### Prove equality properties

Source: https://lean-lang.org/theorem_proving_in_lean4/Inductive-Types

Examples of proving symmetry, transitivity, and congruence for equality.

```lean
theorem symm (h : Eq a b) : Eq b a := match h with | rfl => rfl 
theorem trans (h₁ : Eq a b) (h₂ : Eq b c) : Eq a c := sorry 
theorem congr (f : α → β) (h : Eq a b) : Eq (f a) (f b) := sorry 
```

--------------------------------

### Equality proof with calc

Source: https://lean-lang.org/theorem_proving_in_lean4/Quantifiers-and-Equality

A basic example of proving equality using the calc command.

```lean
variable (a b c d e : Nat) theorem T (h1 : a = b) (h2 : b = c + 1) (h3 : c = d) (h4 : e = 1 + d) : a = e := calc a = b := h1 _ = c + 1 := h2 _ = d + 1 := congrArg Nat.succ h3 _ = 1 + d := Nat.add_comm d 1 _ = e := Eq.symm h4
```

--------------------------------

### Standard library namespace examples

Source: https://lean-lang.org/theorem_proving_in_lean4/Dependent-Type-Theory

Checking definitions within the standard List namespace.

```lean
#check List.nil
#check List.cons
#check List.map
```

```lean
open List
#check nil
#check cons
#check map
```

--------------------------------

### Demonstrate Computational Blocking with funext

Source: https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation

Example showing how funext prevents reduction in the Lean kernel.

```lean
def f (x : Nat) := x 
def g (x : Nat) := 0 + x 
theorem f_eq_g : f = g := funext fun x => (Nat.zero_add x).symm 
def val : Nat := Eq.recOn (motive := fun _ _ => Nat) f_eq_g 0 
#reduce val
f_eq_g ▸ 0
#eval val
0
```

--------------------------------

### Quotient Construction Example

Source: https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation

Demonstration of defining a relation, creating a quotient type, and lifting a function to that type.

```lean
def mod7Rel (x y : Nat) : Prop := x % 7 = y % 7 
-- the quotient type `Quot mod7Rel : Type`
#check (Quot mod7Rel : Type)
```

```lean
-- the class of numbers equivalent to 4 
Quot.mk mod7Rel 4 : Quot mod7Rel
#check (Quot.mk mod7Rel 4 : Quot mod7Rel)
```

```lean
def f (x : Nat) : Bool := x % 7 = 0 
theorem f_respects (a b : Nat) (h : mod7Rel a b) : f a = f b := by
a:Nat
b:Nat
h:mod7Rel a b
⊢ f a = f b 
simp [mod7Rel, f] at *
a:Nat
b:Nat
h:a % 7 = b % 7
⊢ a % 7 = 0 ↔ b % 7 = 0 
rw [h]
All goals completed! 🐙 
Quot.lift f f_respects : Quot mod7Rel → Bool
#check (Quot.lift f f_respects : Quot mod7Rel → Bool)
```

```lean
-- the computation principle 
example (a : Nat) : Quot.lift f f_respects (Quot.mk mod7Rel a) = f a := rfl 
```

--------------------------------

### Demonstrate Computational Blocking with propext

Source: https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation

Example showing how propext prevents reduction in the Lean kernel.

```lean
theorem tteq : (True ∧ True) = True := propext (Iff.intro (fun ⟨h, _⟩ => h) (fun h => ⟨h, h⟩)) 
def val : Nat := Eq.recOn (motive := fun _ _ => Nat) tteq 0 
#reduce val
tteq ▸ 0
#eval val
0
```

--------------------------------

### Check decidability instances

Source: https://lean-lang.org/theorem_proving_in_lean4/Type-Classes

Examples of checking decidability instances for propositional connectives.

```lean
@instDecidableAnd : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)
```

```lean
@instDecidableOr : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∨ q)
```

```lean
@instDecidableNot : {p : Prop} → [dp : Decidable p] → Decidable ¬p
```

--------------------------------

### Existential Quantifier Introduction

Source: https://lean-lang.org/theorem_proving_in_lean4/Quantifiers-and-Equality

Examples of proving existential statements using Exists.intro.

```lean
example : ∃ x : Nat, x > 0 := have h : 1 > 0 := Nat.zero_lt_succ 0
Exists.intro 1 h
```

```lean
example (x : Nat) (h : x > 0) : ∃ y, y < x := Exists.intro 0 h
```

```lean
example (x y z : Nat) (hxy : x < y) (hyz : y < z) : ∃ w, x < w ∧ w < z := Exists.intro y (And.intro hxy hyz)
```

```lean
#check @Exists.intro
```

--------------------------------

### Apply Propositional Extensionality

Source: https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation

Examples of using propext to prove equality between propositions.

```lean
variable (a b c d e : Prop) 
theorem thm₁ (h : a ↔ b) : (c ∧ a ∧ d → e) ↔ (c ∧ b ∧ d → e) := propext h ▸ Iff.refl _ 
theorem thm₂ (p : Prop → Prop) (h : a ↔ b) (h₁ : p a) : p b := propext h ▸ h₁ 
```

--------------------------------

### Simplify list operations

Source: https://lean-lang.org/theorem_proving_in_lean4/Tactics

Examples of using simp with list-related identities and custom rewrite rules.

```lean
open List
example (xs : List Nat) : reverse (xs ++ [1, 2, 3]) = [3, 2, 1] ++ reverse xs := by
  simp
```

```lean
example (xs ys : List α) : length (reverse (xs ++ ys)) = length xs + length ys := by
  simp [Nat.add_comm]
```

--------------------------------

### Verifying Definitional Equations for Natural Numbers

Source: https://lean-lang.org/theorem_proving_in_lean4/Induction-and-Recursion

Examples demonstrating that pattern-matched functions satisfy their equations definitionally.

```lean
open Nat def sub1 : Nat → Nat | zero => zero | succ x => x def isZero : Nat → Bool | zero => true | succ unused variable x  Note: This linter can be disabled with set_option linter.unusedVariables falsex => false 
example : sub1 0 = 0 := rfl example (x : Nat) : sub1 (succ x) = x := rfl example : isZero 0 = true := rfl example (x : Nat) : isZero (succ x) = false := rfl example : sub1 7 = 6 := rfl example (x : Nat) : isZero (x + 3) = false := rfl
```

--------------------------------

### Nested pattern matching example

Source: https://lean-lang.org/theorem_proving_in_lean4/Induction-and-Recursion

Demonstrates nested pattern matching with existential quantifiers.

```lean
set_option linter.unusedVariables false 
example (p q : α → Prop) : (∃ x, p x ∨ q x) → (∃ x, p x) ∨ (∃ x, q x) | Exists.intro x (Or.inl px) => Or.inl (Exists.intro x px) | Exists.intro x (Or.inr qx) => Or.inr (Exists.intro x qx)
```

--------------------------------

### Use Prod.casesOn Recursor

Source: https://lean-lang.org/theorem_proving_in_lean4/Inductive-Types

Example of using the casesOn recursor to define a function on a product type.

```Lean
def prod_example (p : Bool × Nat) : Nat := Prod.casesOn (motive := fun _ => Nat) p (fun b n => cond b (2 * n) (2 * n + 1))
```

```Lean
#eval prod_example (true, 3)
```

```Lean
#eval prod_example (false, 3)
```

--------------------------------

### Define a commutative conjunction theorem in Lean

Source: https://lean-lang.org/theorem_proving_in_lean4/Introduction

A basic example demonstrating the syntax for defining a theorem and proving it using logical conjunction.

```lean
theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := fun hpq : p ∧ q => have hp : p := And.left hpq have hq : q := And.right hpq show q ∧ p from And.intro hq hp
```

--------------------------------

### Use pattern matching with intro

Source: https://lean-lang.org/theorem_proving_in_lean4/Tactics

Shows how intro supports pattern matching on structures and multiple alternatives.

```lean
example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := byα:Sort u_1p:α → Propq:α → Prop⊢ (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x intro ⟨w, hpw, hqw⟩α:Sort u_1p:α → Propq:α → Propw:αhpw:p whqw:q w⊢ ∃ x, q x ∧ p x exact ⟨w, hqw, hpw⟩All goals completed! 🐙
```

```lean
example (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := byα:Sort u_1p:α → Propq:α → Prop⊢ (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x intro | ⟨w, Or.inl h⟩ =>α:Sort u_1p:α → Propq:α → Propx✝:∃ x, p x ∨ q xw:αh:p w⊢ ∃ x, q x ∨ p x exact ⟨w, Or.inr h⟩All goals completed! 🐙 | ⟨w, Or.inr h⟩ =>α:Sort u_1p:α → Propq:α → Propx✝:∃ x, p x ∨ q xw:αh:q w⊢ ∃ x, q x ∨ p x exact ⟨w, Or.inl h⟩All goals completed! 🐙
```

--------------------------------

### Evaluate Weekday Functions

Source: https://lean-lang.org/theorem_proving_in_lean4/Inductive-Types

Examples of evaluating functions on the Weekday type.

```lean
```Weekday.thursday`#eval next (next tuesday)````
```

```lean
```Weekday.tuesday`#eval next (previous tuesday)````
```

--------------------------------

### Introduce variables and hypotheses with intro

Source: https://lean-lang.org/theorem_proving_in_lean4/Tactics

Demonstrates using intro to introduce variables and hypotheses into the local context.

```lean
example (α : Type) : α → α := byα:Type⊢ α → α intro aα:Typea:α⊢ α exact aAll goals completed! 🐙
```

```lean
example (α : Type) : ∀ x : α, x = x := byα:Type⊢ ∀ (x : α), x = x intro xα:Typex:α⊢ x = x exact Eq.refl xAll goals completed! 🐙
```

```lean
example : ∀ a b c : Nat, a = b → a = c → c = b := by⊢ ∀ (a b c : Nat), a = b → a = c → c = b intro a ba:Natb:Nat⊢ ∀ (c : Nat), a = b → a = c → c = b ca:Natb:Natc:Nat⊢ a = b → a = c → c = b h₁a:Natb:Natc:Nath₁:a = b⊢ a = c → c = b h₂a:Natb:Natc:Nath₁:a = bh₂:a = c⊢ c = b exact Eq.trans (Eq.symm h₂) h₁All goals completed! 🐙
```

--------------------------------

### Natural Tactic Proof Example

Source: https://lean-lang.org/theorem_proving_in_lean4/Tactics

A standard tactic-based proof for logical equivalence.

```lean
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := byp:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r apply Iff.intrompp:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rmprp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) .mpp:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r intro hmpp:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r cases h.right with | inl hq =>mp.inlp:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r exact Or.inl ⟨h.left, hq⟩All goals completed! 🐙 | inr hr =>mp.inrp:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r exact Or.inr ⟨h.left, hr⟩All goals completed! 🐙 .mprp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) intro hmprp:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) cases h with | inl hpq =>mpr.inlp:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) exact ⟨hpq.left, Or.inl hpq.right⟩All goals completed! 🐙 | inr hpr =>mpr.inrp:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) exact ⟨hpr.left, Or.inr hpr.right⟩All goals completed! 🐙
```

--------------------------------

### Or-introduction rules

Source: https://lean-lang.org/theorem_proving_in_lean4/Propositions-and-Proofs

Demonstrates creating proofs of disjunctions using Or.intro_left and Or.intro_right.

```lean
variable (p q : Prop)
example (hp : p) : p ∨ q := Or.intro_left q hp
example (hq : q) : p ∨ q := Or.intro_right p hq
```

--------------------------------

### Use cases with with clause and dependencies

Source: https://lean-lang.org/theorem_proving_in_lean4/Inductive-Types

Shows how to name constructor arguments and handle local context dependencies that revert automatically.

```lean
open Nat

example (n : Nat) (h : n ≠ 0) : succ (pred n) = n := by
n:Nat
h:n ≠ 0
⊢ n.pred.succ = n

cases n with
| zero =>
  zero
  h:0 ≠ 0
  ⊢ (pred 0).succ = 0
  apply absurd rfl h
  All goals completed! 🐙
| succ m =>
  succ
  m:Nat
  h:m + 1 ≠ 0
  ⊢ (m + 1).pred.succ = m + 1
  rfl
  All goals completed! 🐙
```

--------------------------------

### Define and Open Namespaces

Source: https://lean-lang.org/theorem_proving_in_lean4/Interacting-with-Lean

Demonstrates creating a namespace and using open to create temporary aliases for definitions.

```lean
namespace Foo 
def bar : Nat := 1 
end Foo 
open Foo 
#check bar
```

```lean
#check Foo.bar
```

--------------------------------

### Handle multiple constructors with cases

Source: https://lean-lang.org/theorem_proving_in_lean4/Inductive-Types

Demonstrates matching on multiple constructors with arguments.

```lean
inductive Foo where
| bar1 : Nat → Nat → Foo
| bar2 : Nat → Nat → Nat → Foo
```

```lean
def silly (x : Foo) : Nat := by
x:Foo
⊢ Nat

cases x with
| bar1 a b =>
  bar1
  a:Nat
  b:Nat
  ⊢ Nat
  exact b
  All goals completed! 🐙
| bar2 c d e =>
  bar2
  c:Nat
  d:Nat
  e:Nat
  ⊢ Nat
  exact e
  All goals completed! 🐙
```

--------------------------------

### Defining Vectors and Equality

Source: https://lean-lang.org/theorem_proving_in_lean4/Inductive-Types

Examples of inductive families including vectors and the equality type.

```lean
inductive Vect (α : Type u) : Nat → Type u where | nil : Vect α 0 | cons : α → {n : Nat} → Vect α n → Vect α (n + 1)
```

```lean
namespace Hidden 
inductive Eq {α : Sort u} (a : α) : α → Prop where | refl : Eq a a 
end Hidden 
```

--------------------------------

### Rewrite under binders using conversion mode

Source: https://lean-lang.org/theorem_proving_in_lean4/The-Conversion-Tactic-Mode

Shows how to enter function binders using the intro command to perform rewrites that are otherwise inaccessible in standard tactic mode.

```lean
example : (fun x : Nat => 0 + x) = (fun x => x) := by
⊢ (fun x => 0 + x) = fun x => x
conv =>
| (fun x => 0 + x) = fun x => x
lhs
| fun x => 0 + x
intro x
hx:Nat
| 0 + x
rw [Nat.zero_add]
hx:Nat
| x
```

--------------------------------

### Use Decide Tactic

Source: https://lean-lang.org/theorem_proving_in_lean4/Type-Classes

Examples of using the decide tactic to solve simple goals.

```lean
example : 10 < 5 ∨ 1 > 0 := by
decide
```

```lean
example : ¬(True ∧ False) := by
decide
```

```lean
example : 10 * 20 = 200 := by
decide
```

```lean
theorem ex : True ∧ 2 = 1 + 1 := by
decide
```

--------------------------------

### Demonstrate let vs lambda abstraction

Source: https://lean-lang.org/theorem_proving_in_lean4/Dependent-Type-Theory

Compare the behavior of let expressions with lambda abstractions to understand scoping differences.

```lean
def foo := let a := Nat; fun x : a => x + 2
```

```lean
/-   def bar := (fun a => fun x : a => x + 2) Nat -/
```

--------------------------------

### Proof Simplification with rw and simp

Source: https://lean-lang.org/theorem_proving_in_lean4/Quantifiers-and-Equality

Shows how to use rewrite and simplification tactics to prove equalities concisely.

```lean
variable (x y : Nat)
example : (x + y) * (x + y) = x * x + y * x + x * y + y * y := by
  rw [Nat.mul_add, Nat.add_mul, Nat.add_mul, ←Nat.add_assoc]
```

```lean
example : (x + y) * (x + y) = x * x + y * x + x * y + y * y := by
  simp [Nat.mul_add, Nat.add_mul, Nat.add_assoc]
```

--------------------------------

### Alternative approaches for binder rewriting

Source: https://lean-lang.org/theorem_proving_in_lean4/The-Conversion-Tactic-Mode

Demonstrates alternative methods to prove equality under binders using funext or simp.

```lean
example : (fun x : Nat => 0 + x) = (fun x => x) := by
⊢ (fun x => 0 + x) = fun x => x
funext x
hx:Nat
⊢ 0 + x = x
; rw [Nat.zero_add]
All goals completed! 🐙
```

```lean
example : (fun x : Nat => 0 + x) = (fun x => x) := by
⊢ (fun x => 0 + x) = fun x => x
simp
All goals completed! 🐙
```

--------------------------------

### Check type coercion

Source: https://lean-lang.org/theorem_proving_in_lean4/Interacting-with-Lean

Examples of Lean automatically inserting coercions when checking types.

```lean
#check i + m
```

```lean
#check i + m + j
```

```lean
#check i + m + n
```

--------------------------------

### Proving Propositional Equality with Quotients

Source: https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation

Demonstrates the use of funext and propext to establish equality between predicates involving propositions.

```lean
have p_implies_uv : p → u = v := fun hp => have hpred : U = V := funext fun x => have hl : (x = True ∨ p) → (x = False ∨ p) := fun _ => Or.inr hp have hr : (x = False ∨ p) → (x = True ∨ p) := fun _ => Or.inr hp show (x = True ∨ p) = (x = False ∨ p) from propext (Iff.intro hl hr) have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := byp:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVnot_uv_or_p:u ≠ v ∨ p := match u_def, v_def with | Or.inr h, x => Or.inr h | x, Or.inr h => Or.inr h | Or.inl hut, Or.inl hvf => Or.inl (of_eq_true (Eq.trans (congr (congrArg Ne hut) hvf) (Eq.trans (congrArg Not (Eq.trans eq_iff_iff._simp_1 (Eq.trans (iff_false True) not_true_eq_false))) not_false_eq_true)))hp:phpred:U = V := funext fun x => have hl := fun x_1 => Or.inr hp; have hr := fun x_1 => Or.inr hp; have this := propext { mp := hl, mpr := hr }; this⊢ ∀ (exU : ∃ x, U x) (exV : ∃ x, V x), choose exU = choose exV rw [hpred]p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVnot_uv_or_p:u ≠ v ∨ p := match u_def, v_def with | Or.inr h, x => Or.inr h | x, Or.inr h => Or.inr h | Or.inl hut, Or.inl hvf => Or.inl (of_eq_true (Eq.trans (congr (congrArg Ne hut) hvf) (Eq.trans (congrArg Not (Eq.trans eq_iff_iff._simp_1 (Eq.trans (iff_false True) not_true_eq_false))) not_false_eq_true)))hp:phpred:U = V := funext fun x => have hl := fun x_1 => Or.inr hp; have hr := fun x_1 => Or.inr hp; have this := propext { mp := hl, mpr := hr }; this⊢ ∀ (exU exV : ∃ x, V x), choose exU = choose exV; introsp:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVnot_uv_or_p:u ≠ v ∨ p := match u_def, v_def with | Or.inr h, x => Or.inr h | x, Or.inr h => Or.inr h | Or.inl hut, Or.inl hvf => Or.inl (of_eq_true (Eq.trans (congr (congrArg Ne hut) hvf) (Eq.trans (congrArg Not (Eq.trans eq_iff_iff._simp_1 (Eq.trans (iff_false True) not_true_eq_false))) not_false_eq_true)))hp:phpred:U = V := funext fun x => have hl := fun x_1 => Or.inr hp; have hr := fun x_1 => Or.inr hp; have this := propext { mp := hl, mpr := hr }; thisexU✝:∃ x, V xexV✝:∃ x, V x⊢ choose exU✝ = choose exV✝; rflAll goals completed! 🐙 show u = v from h₀ _ _
```

--------------------------------

### Define function with exhaustive patterns

Source: https://lean-lang.org/theorem_proving_in_lean4/Induction-and-Recursion

Example of a function definition that the equation compiler checks for coverage.

```lean
def bar : Nat → List Nat → Bool → Nat | 0, _, false => 0 | 0, b :: _, _ => b | 0, [], true => 7 | a+1, [], false => a | a+1, [], true => a + 1 | a+1, b :: _, _ => a + b
```

--------------------------------

### Use Sum.casesOn Recursor

Source: https://lean-lang.org/theorem_proving_in_lean4/Inductive-Types

Example of using the casesOn recursor to define a function on a sum type.

```Lean
def sum_example (s : Sum Nat Nat) : Nat := Sum.casesOn (motive := fun _ => Nat) s (fun n => 2 * n) (fun n => 2 * n + 1)
```

```Lean
#eval sum_example (Sum.inl 3)
```

```Lean
#eval sum_example (Sum.inr 3)
```

--------------------------------

### Opening namespaces

Source: https://lean-lang.org/theorem_proving_in_lean4/Dependent-Type-Theory

Using the open command to bring short names into the current scope.

```lean
open Foo
```

--------------------------------

### Declare variables for coercion examples

Source: https://lean-lang.org/theorem_proving_in_lean4/Interacting-with-Lean

Variables used to demonstrate type coercion between Nat and Int.

```lean
variable (m n : Nat) 
variable (i j : Int)
```

--------------------------------

### Structured Proofs with calc

Source: https://lean-lang.org/theorem_proving_in_lean4/Quantifiers-and-Equality

Demonstrates using the calc environment to perform step-by-step algebraic proofs in Lean.

```lean
variable (x y : Nat)
example : (x + y) * (x + y) = x * x + y * x + x * y + y * y := calc
  (x + y) * (x + y) = (x + y) * x + (x + y) * y := by rw [Nat.mul_add]
  _ = x * x + y * x + (x + y) * y := by rw [Nat.add_mul]
  _ = x * x + y * x + (x * y + y * y) := by rw [Nat.add_mul]
  _ = x * x + y * x + x * y + y * y := by rw [←Nat.add_assoc]
```

```lean
variable (x y : Nat)
example : (x + y) * (x + y) = x * x + y * x + x * y + y * y := calc
  (x + y) * (x + y)
  _ = (x + y) * x + (x + y) * y := by rw [Nat.mul_add]
  _ = x * x + y * x + (x + y) * y := by rw [Nat.add_mul]
  _ = x * x + y * x + (x * y + y * y) := by rw [Nat.add_mul]
  _ = x * x + y * x + x * y + y * y := by rw [←Nat.add_assoc]
```

--------------------------------

### Introducing Local Definitions with let

Source: https://lean-lang.org/theorem_proving_in_lean4/Tactics

Uses the 'let' tactic to introduce local definitions that can be unfolded during the proof.

```lean
example : ∃ x, x + 2 = 8 := by⊢ ∃ x, x + 2 = 8 let a : Nat := 3 * 2a:Nat := 3 * 2⊢ ∃ x, x + 2 = 8 exists aAll goals completed! 🐙
```

--------------------------------

### Function Composition and Identity

Source: https://lean-lang.org/theorem_proving_in_lean4/Dependent-Type-Theory

Examples of identity functions and function composition using lambda abstraction.

```lean
def f (n : Nat) : String := toString n 
def g (s : String) : Bool := s.length > 0 
#check fun x : Nat => x
```

```lean
#check fun x : Nat => true
```

```lean
#check fun x : Nat => g (f x)
```

```lean
#check fun x => g (f x)
```

--------------------------------

### Swap Pair and Sum using Cases

Source: https://lean-lang.org/theorem_proving_in_lean4/Tactics

Demonstrates using the cases tactic to destruct product and sum types.

```lean
def swap_pair : α × β → β × α := by
α:Type ?u.18
β:Type ?u.17
⊢ α × β → β × α
intro p
α:Type ?u.18
β:Type ?u.17
p:α × β
⊢ β × α
cases p
mk
α:Type ?u.18
β:Type ?u.17
fst✝:α
snd✝:β
⊢ β × α
constructor
mk.fst
α:Type ?u.18
β:Type ?u.17
fst✝:α
snd✝:β
⊢ β
mk.snd
α:Type ?u.18
β:Type ?u.17
fst✝:α
snd✝:β
⊢ α
<;>
mk.fst
α:Type ?u.18
β:Type ?u.17
fst✝:α
snd✝:β
⊢ β
mk.snd
α:Type ?u.18
β:Type ?u.17
fst✝:α
snd✝:β
⊢ α
assumption
All goals completed! 🐙
```

```lean
def swap_sum : Sum α β → Sum β α := by
α:Type ?u.196
β:Type ?u.195
⊢ α ⊕ β → β ⊕ α
intro p
α:Type ?u.196
β:Type ?u.195
p:α ⊕ β
⊢ β ⊕ α
cases p
inl
α:Type ?u.196
β:Type ?u.195
val✝:α
⊢ β ⊕ α
inr
α:Type ?u.196
β:Type ?u.195
val✝:β
⊢ β ⊕ α
.inl
α:Type ?u.196
β:Type ?u.195
val✝:α
⊢ β ⊕ α
apply Sum.inr
inl.val
α:Type ?u.196
β:Type ?u.195
val✝:α
⊢ α; assumption
All goals completed! 🐙
.inr
α:Type ?u.196
β:Type ?u.195
val✝:β
⊢ β ⊕ α
apply Sum.inl
inr.val
α:Type ?u.196
β:Type ?u.195
val✝:β
⊢ β; assumption
All goals completed! 🐙
```

--------------------------------

### Define Vector Type and zipWith

Source: https://lean-lang.org/theorem_proving_in_lean4/Induction-and-Recursion

Setup for the Vect inductive type and the zipWith function definition.

```lean
set_option linter.unusedVariables false inductive Vect (α : Type u) : Nat → Type u | nil : Vect α 0 | cons : α → {n : Nat} → Vect α n → Vect α (n+1) namespace Vect 

def zipWith (f : α → β → γ) : {n : Nat} → Vect α n → Vect β n → Vect γ n | 0, nil, nil => nil | n+1, cons a as, cons b bs => cons (f a b) (zipWith f as bs)
```

--------------------------------

### Combine split with tactic combinators

Source: https://lean-lang.org/theorem_proving_in_lean4/Tactics

Shows how to chain split with other tactics using combinators like <;> and first.

```lean
def f (x y z : Nat) : Nat := match x, y, z with | 5, _, _ => y | _, 5, _ => y | _, _, 5 => y | _, _, _ => 1 
```

```lean
example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := byw:Natx:Naty:Natz:Nat⊢ x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 introsw:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ f x y w = 1; simp [f]w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ (match x, y, w with | 5, x, x_1 => y | x, 5, x_1 => y | x, x_1, 5 => y | x, x_1, x_2 => 1) = 1; splith_1w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1h_2w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1h_3x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1h_4w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 <;>h_1w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1h_2w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1h_3x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1h_4w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 first | contradictionh_4w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 | rflAll goals completed! 🐙
```

--------------------------------

### Define Vect type with namespace

Source: https://lean-lang.org/theorem_proving_in_lean4/Induction-and-Recursion

Initial setup for defining vector operations within a namespace.

```lean
set_option linter.unusedVariables false inductive Vect (α : Type u) : Nat → Type u | nil : Vect α 0 | cons : α → {n : Nat} → Vect α n → Vect α (n+1) namespace Vect
```

--------------------------------

### Prove logical equivalence with Iff

Source: https://lean-lang.org/theorem_proving_in_lean4/Propositions-and-Proofs

Demonstrates proving p ∧ q ↔ q ∧ p using Iff.intro and checking the result.

```lean
variable (p q : Prop) 
theorem and_swap : p ∧ q ↔ q ∧ p := Iff.intro (fun h : p ∧ q => show q ∧ p from And.intro (And.right h) (And.left h)) (fun h : q ∧ p => show p ∧ q from And.intro (And.right h) (And.left h)) 
#check and_swap p q
```

--------------------------------

### Tactics for Inductive Types

Source: https://lean-lang.org/theorem_proving_in_lean4/Inductive-Types

Examples demonstrating the use of tactics to manipulate inductive types and prove equality.

```lean
example : s ∧ q ∧ r → p ∧ r → q ∧ p := by
  intro ⟨_, ⟨hq, _⟩⟩ ⟨hp, _⟩
  exact ⟨hq, hp⟩
```

```lean
example : (fun (x : Nat × Nat) (y : Nat × Nat) => x.1 + y.2) = (fun (x : Nat × Nat) (z : Nat × Nat) => z.2 + x.1) := by
  funext (a, b) (c, d)
  show a + d = d + a
  rw [Nat.add_comm]
```

--------------------------------

### Defining global [instance] attribute

Source: https://lean-lang.org/theorem_proving_in_lean4/Interacting-with-Lean

Use the instance command to assign an attribute that enables notation like ≤.

```lean
def isPrefix (l₁ : List α) (l₂ : List α) : Prop := ∃ t, l₁ ++ t = l₂ 
instance : LE (List α) where le := isPrefix 
theorem List.isPrefix_self (as : List α) : as ≤ as := ⟨[], by
α:Type u_1
as:List α
⊢ as ++ [] = as 
simp
All goals completed! 🐙
⟩
```

--------------------------------

### Multiple Inheritance and Object Initialization

Source: https://lean-lang.org/theorem_proving_in_lean4/Structures-and-Records

Shows how to define a structure using multiple inheritance and initialize it using parent structure objects.

```lean
structure Point (α : Type u) where x : α y : α z : α
```

```lean
structure RGBValue where red : Nat green : Nat blue : Nat
```

```lean
structure RedGreenPoint (α : Type u) extends Point α, RGBValue where no_blue : blue = 0
```

```lean
def p : Point Nat := { x := 10, y := 10, z := 20 }
```

```lean
def rgp : RedGreenPoint Nat := { p with red := 200, green := 40, blue := 0, no_blue := rfl }
```

```lean
example : rgp.x = 10 := rfl
```

```lean
example : rgp.red = 200 := rfl
```

--------------------------------

### Equality proof with rw tactic

Source: https://lean-lang.org/theorem_proving_in_lean4/Quantifiers-and-Equality

Examples of using the rw tactic to perform sequential rewrites in proofs.

```lean
variable (a b c d e : Nat) theorem T (h1 : a = b) (h2 : b = c + 1) (h3 : c = d) (h4 : e = 1 + d) : a = e := calc a = b := by rw [h1] _ = c + 1 := by rw [h2] _ = d + 1 := by rw [h3] _ = 1 + d := by rw [Nat.add_comm] _ = e := by rw [h4]
```

```lean
variable (a b c d e : Nat) theorem T (h1 : a = b) (h2 : b = c + 1) (h3 : c = d) (h4 : e = 1 + d) : a = e := calc a = d + 1 := by rw [h1, h2, h3] _ = 1 + d := by rw [Nat.add_comm] _ = e := by rw [h4]
```

```lean
variable (a b c d e : Nat) theorem T (h1 : a = b) (h2 : b = c + 1) (h3 : c = d) (h4 : e = 1 + d) : a = e := by rw [h1, h2, h3, Nat.add_comm, h4]
```
Tokens:
Raw