### Lean 4: Example of Extfun Application and Equality

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

Demonstrates an example showing that if two functions `f₁` and `f₂` are extensionally equal, then applying `extfun_app` to their `extfun` representations results in equal values.

```Lean
example (f₁ f₂ : (x : α) → β x) (h : ∀ x, f₁ x = f₂ x) :=
  calc f₁ _ = extfun_app (.mk _ f₁)
    := rfl
    _ = extfun_app (.mk _ f₂)
    := by
      α : Sort u
      β : α → Sort v
      f₁ : (x : α) → β x
      f₂ : (x : α) → β x
      h : ∀ (x : α), f₁ x = f₂ x
      ⊢ extfun_app (Quot.mk (fun f g => ∀ (x : α), f x = g x) f₁) = extfun_app (Quot.mk (fun f g => ∀ (x : α), f x = g x) f₂)
      rw [Quot.sound]
      α : Sort u
      β : α → Sort v
      f₁ : (x : α) → β x
      f₂ : (x : α) → β x
      h : ∀ (x : α), f₁ x = f₂ x
      ⊢ ∀ (x : α), f₁ x = f₂ x
      ; trivial
    _ = f₂ := rfl
```

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

### Lean 4 Existential Quantifier Introduction Rule and Examples

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

Demonstrates the introduction rule for the existential quantifier in Lean 4 using `Exists.intro`. It shows how to construct proofs for `∃ x : α, p x` by providing a term `t` and a proof of `p t`. Includes examples with explicit and anonymous constructor notation.

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

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

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

-- Anonymous constructor notation
example : ∃ x : Nat, x > 0 :=
  have h : 1 > 0 := Nat.zero_lt_succ 0
  ⟨1, h⟩

example (x : Nat) (h : x > 0) : ∃ y, y < x :=
  ⟨0, h⟩

example (x y z : Nat) (hxy : x < y) (hyz : y < z) : ∃ w, x < w ∧ w < z :=
  ⟨y, hxy, hyz⟩
```

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

### Proving Universal Quantifiers in Lean 4

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

Examples demonstrating the use of the universal quantifier, including variable instantiation and the application of introduction and elimination rules.

```Lean 4
example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ y : α, p y := 
  fun h : ∀ x : α, p x ∧ q x => fun y : α => show p y from (h y).left
```

```Lean 4
example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ x : α, p x := 
  fun h : ∀ x : α, p x ∧ q x => fun z : α => show p z from And.left (h z)
```

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

### Lean 4 Calculational Proof Example with Equality

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

An example of a calculational proof in Lean 4 demonstrating how to prove an equality between two Nat values using a chain of equalities and hypotheses. This showcases the direct application of proofs to intermediate steps.

```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
```

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

### Verify Nat Library Theorems in Lean

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

Examples of using the #check command to inspect standard library theorems for natural numbers, demonstrating naming conventions.

```lean
#check Nat.succ_ne_zero
#check Nat.zero_add
#check Nat.mul_one
#check Nat.le_of_succ_le_succ
```

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

### Pretty Printing Examples in Lean 4

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

Illustrates the effect of pretty printing options on Lean's output. Shows how different combinations of `pp.explicit`, `pp.universes`, and `pp.notation` alter the display of terms and function applications.

```lean
#check 2 + 2 = 4
```

```lean
#reduce (fun x => x + 2) = (fun x => x + 3)
```

```lean
#check (fun x => x + 1) 1
```

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

### Using Standard Library Functions in Lean 4

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

Shows how to use functions from the Lean 4 standard library, such as `Nat.succ`, `Nat.add`, and tuple accessors (`.fst`, `.snd`). It includes type checking and evaluation examples.

```Lean
`Nat.succ (n : Nat) : Nat`
#check Nat.succ

`(0, 1) : Nat × Nat`
#check (0, 1)

`Nat.add : Nat → Nat → Nat`
#check Nat.add

``Nat.succ 2 : Nat`
#check Nat.succ 2

``Nat.add 3 : Nat → Nat`
#check Nat.add 3

``Nat.add 5 2 : Nat`
#check Nat.add 5 2

``(5, 9).fst : Nat`
#check (5, 9).1

``(5, 9).snd : Nat`
#check (5, 9).2

``3`
#eval Nat.succ 2

``7`
#eval Nat.add 5 2

``5`
#eval (5, 9).1

``9`
#eval (5, 9).2
```

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

### Lean 4: Implicit lambda example with pure

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

Illustrates implicit lambda introduction in Lean 4. When the expected type is a function awaiting implicit arguments, Lean automatically introduces lambdas. This example shows `pure`'s behavior with `ReaderT`.

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

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

### Lean 4 Calculational Proof with Mixed Relations

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

An example of a calculational proof in Lean 4 that combines different relations (equality and inequality) to prove a final goal. This shows the flexibility of the 'calc' command.

```Lean
variable (a b c d : Nat)
example (h1 : a = b) (h2 : b ≤ c) (h3 : c + 1 < d) : a < d :=
calc a = b := h1
    _ < b + 1 := Nat.lt_succ_self b
    _ ≤ c + 1 := Nat.succ_le_succ h2
    _ < d := h3
```

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

### Define Basic Mixfix Operators

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

Examples of defining prefix, infix, and postfix operators with specific precedence levels and associativity in Lean 4.

```lean
infixl:65 " + " => HAdd.hAdd
infix:50 " = " => Eq
infixr:80 " ^ " => HPow.hPow
prefix:100 "-" => Neg.neg
postfix:max "⁻¹" => Inv.inv
```

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

### Multiple Inheritance Example (Lean 4)

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

Shows how to define a structure using multiple inheritance by extending multiple parent structures. The 'RedGreenPoint' structure inherits from both 'Point' and 'RGBValue', demonstrating how fields from different structures can be combined. An object is then defined using fields from these parent structures.

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

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

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

def p : Point Nat := { x := 10, y := 10, z := 20 }
def rgp : RedGreenPoint Nat := { p with red := 200, green := 40, blue := 0, no_blue := rfl }

example : rgp.x = 10 := rfl
example : rgp.red = 200 := rfl
```

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

### Lean 4: Printing Definitions of Eq.symm and User-Defined foo

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

Illustrates the use of the '#print' command in Lean 4 to display the full definition of theorems and functions. Examples include printing the definition of 'Eq.symm' and a user-defined function 'foo'.

```Lean
-- Printing the definition of Eq.symm
#print Eq.symm

-- Checking the type of a user-defined function 'foo'
#check foo

-- Checking the type of 'foo' with explicit arguments
#check @foo

-- Printing the definition of the user-defined function 'foo'
#print foo
```

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

### Lean 4 Existential Quantifier with Implicit Arguments

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

Illustrates how Lean infers implicit arguments for `Exists.intro` when proving existential statements. The examples show different possible predicates that Lean can infer based on the context, and how `set_option pp.explicit true` reveals these inferred arguments.

```lean
variable (g : Nat → Nat → Nat)

theorem gex1 (hg : g 0 0 = 0) : ∃ x, g x x = x :=
  ⟨0, hg⟩

theorem gex2 (hg : g 0 0 = 0) : ∃ x, g x 0 = x :=
  ⟨0, hg⟩

theorem gex3 (hg : g 0 0 = 0) : ∃ x, g 0 0 = x :=
  ⟨0, hg⟩

theorem gex4 (hg : g 0 0 = 0) : ∃ x, g x x = 0 :=
  ⟨0, hg⟩

set_option pp.explicit true  -- display implicit arguments

#print gex1

#print gex2

#print gex3
```

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

### Implement Propositional Logic Proofs in Lean 4

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

Examples demonstrating formal proofs for distributive laws and classical logic implications. These snippets utilize Lean's 'Iff.intro' and 'Or.elim' to handle logical equivalence and disjunction.

```lean
open Classical

-- Distributivity example
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
  Iff.intro
    (fun h : p ∧ (q ∨ r) =>
      have hp : p := h.left
      Or.elim (h.right)
        (fun hq : q => show (p ∧ q) ∨ (p ∧ r) from Or.inl ⟨hp, hq⟩)
        (fun hr : r => show (p ∧ q) ∨ (p ∧ r) from Or.inr ⟨hp, hr⟩))
    (fun h : (p ∧ q) ∨ (p ∧ r) =>
      Or.elim h
        (fun hpq : p ∧ q =>
          have hp : p := hpq.left
          have hq : q := hpq.right
          show p ∧ (q ∨ r) from ⟨hp, Or.inl hq⟩)
        (fun hpr : p ∧ r =>
          have hp : p := hpr.left
          have hr : r := hpr.right
          show p ∧ (q ∨ r) from ⟨hp, Or.inr hr⟩))

-- Example requiring classical reasoning
example (p q : Prop) : ¬(p ∧ ¬q) → (p → q) :=
  fun h : ¬(p ∧ ¬q) =>
    fun hp : p =>
      show q from Or.elim (em q)
        (fun hq : q => hq)
        (fun hnq : ¬q => absurd (And.intro hp hnq) h)
```

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

### Algebraic Proofs using Calc Mode

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

Demonstrates how to use the 'calc' environment to perform step-by-step algebraic expansions. It shows how to align relations using underscores and how to perform rewrites in reverse using the left arrow operator.

```Lean 4
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]
```

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

### Using the Notation Command

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

Demonstrates the use of the general 'notation' command to define custom syntax, including placeholders with specific precedence and mixfix patterns.

```lean
notation:65 lhs:65 " + " rhs:66 => HAdd.hAdd lhs rhs
notation:65 lhs:65 " ~ " rhs:65 => wobble lhs rhs
notation:max "(" e ")" => e
notation:10 Γ " ⊢ " e " : " τ => Typing Γ e τ
```

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

### Define recursive functions with structural and course-of-values recursion

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

Provides examples of standard recursive definitions and their transformation into 'brecOn' form for efficient evaluation.

```Lean 4
def fib : Nat → Nat | 0 => 1 | 1 => 1 | n+2 => fib (n+1) + fib n

def fib : Nat → Nat := fun x => Nat.brecOn x fun x f => (match (motive := (x : Nat) → Nat.below x → Nat) x with | 0 => fun x => 1 | 1 => fun x => 1 | n.succ.succ => fun x => x.1 + x.2.1) f
```

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

### Lean 4: Introduce Conjunction Proof (And.intro)

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

Demonstrates how to construct a proof for 'p ∧ q' using the 'And.intro' function, given proofs for 'p' and 'q'. This is analogous to the AND-introduction rule in logic. It also shows the equivalent anonymous constructor notation.

```Lean
variable (p q : Prop)
example (hp : p) (hq : q) : p ∧ q := And.intro hp hq

-- Equivalent using anonymous constructor notation
variable (p q : Prop)
variable (hp : p)
variable (hq : q)
⟨hp, hq⟩ : p ∧ q
```

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

### Implementing Division via Well-Founded Recursion

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

An example of implementing the division function on natural numbers using well-founded recursion. It includes the lemma for the decreasing measure and the recursive definition.

```lean
open Nat
theorem div_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x := fun h => sub_lt (Nat.lt_of_lt_of_le h.left h.right) h.left
def div.F (x : Nat) (f : (x₁ : Nat) → x₁ < x → Nat → Nat) (y : Nat) : Nat := if h : 0 < y ∧ y ≤ x then f (x - y) (div_lemma h) y + 1 else zero
noncomputable def div := WellFounded.fix (measure id).wf div.F
#reduce div 8 2
```

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

### Pattern Matching on Product and Option Types (Lean 4)

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

Demonstrates pattern matching with product types (tuples) and `Option` types. The `swap` function exchanges elements of a tuple, `foo` sums elements of a tuple, and `bar` processes an `Option Nat`.

```lean
def swap : α × β → β × α | (a, b) => (b, a)
def foo : Nat × Nat → Nat | (m, n) => m + n
def bar : Option Nat → Nat | some n => n + 1 | none => 0
```

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

### Resolve polymorphic expressions with type annotations

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

Shows how to use explicit type annotations (e : T) to guide the Lean elaborator when dealing with polymorphic values like List.nil or id.

```Lean 4
#check (List.nil)
#check (id)
#check (List.nil : List Nat)
#check (id : Nat → Nat)
```

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

### Convert natural numbers to binary representation

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

An example of a recursive function that converts a natural number to a list of bits. It uses 'decreasing_by sorry' to bypass formal termination proof requirements.

```Lean 4
def natToBin : Nat → List Nat
| 0 => [0]
| 1 => [1]
| n + 2 => natToBin ((n + 2) / 2) ++ [n % 2]
decreasing_by sorry

#eval! natToBin 1234567
```

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

### Nesting and Reopening Namespaces

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

Shows how to create hierarchical namespaces by nesting them and how to reopen existing namespaces to add more definitions later.

```lean
namespace Foo
  def a : Nat := 5
  namespace Bar
    def ffa : Nat := 10
  end Bar
end Foo

#check Foo.Bar.ffa

namespace Foo
  def g : Nat := 0
end Foo
```

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

### Defining and Using Namespaces in Lean 4

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

Demonstrates how to define a namespace, declare functions within it, and access them using both short and fully qualified names. It also shows how the 'open' command brings short names into the current scope.

```lean
namespace Foo
  def a : Nat := 5
  def f (x : Nat) : Nat := x + 7
  def fa : Nat := f a
  def ffa : Nat := f (f a)
end Foo

#check Foo.a
#check Foo.f

open Foo
#check a
#check f
```

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

### Nested Pattern Matching with Existential and Disjunction (Lean 4)

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

Shows nested pattern matching involving existential quantifiers (`∃`) and disjunction (`∨`). This example demonstrates how to destructure complex logical statements.

```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)
```

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

### Equality Reasoning with Projection Notation

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

Shows how to chain equality proofs using standard functions versus the more concise projection notation.

```lean
variable (α : Type) (a b c d : α) (hab : a = b) (hcb : c = b) (hcd : c = d)
-- Standard
example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
-- Projection notation
example : a = d := (hab.trans hcb.symm).trans hcd
```

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

### Lean 4 Equality Type Definition

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

Defines the `Eq` type, representing the equality relation between two elements of type `α`. This is an example of an inductive family indexed by the element itself.

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

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

### Implement fast Fibonacci using 'where' and 'let rec' in Lean 4

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

Demonstrates efficient Fibonacci calculation using an auxiliary loop to avoid exponential complexity. The implementation is shown using both 'where' and 'let rec' syntax.

```Lean 4
def fibFast (n : Nat) : Nat := (loop n).2 where loop : Nat → Nat × Nat | 0 => (0, 1) | n+1 => let p := loop n; (p.2, p.1 + p.2)

def fibFast (n : Nat) : Nat := let rec loop : Nat → Nat × Nat | 0 => (0, 1) | n+1 => let p := loop n; (p.2, p.1 + p.2) in (loop n).2
```

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

### Referencing Context with '‹Nat›' in Lean 4

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

Demonstrates that French quotation marks can refer to any element in the context, not just propositions. This example shows referencing the 'Nat' type itself, though its practical use for data is noted as odd.

```lean
example (n : Nat) : Nat := ‹Nat›
```

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

### Lean 4 Proof with 'simp' Tactic

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

Demonstrates the use of the 'simp' tactic in Lean 4 to prove a theorem, which applies given identities repeatedly and automatically. This often results in the most concise proof.

```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 simp [h1, h2, h3, Nat.add_comm, h4]
```

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

### Define Higher-Order Functions in Lean 4

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

Demonstrates how to define higher-order functions in Lean 4, where functions themselves are passed as parameters. This includes examples of function composition with named function parameters and passing types as parameters.

```Lean
fun g f x => g (f x) : (String → Bool) → (Nat → String) → Nat → Bool
#check fun (g : String → Bool) (f : Nat → String) (x : Nat) => g (f x)

fun α β γ g f x => g (f x) : (α β γ : Type) → (β → γ) → (α → β) → α → γ
#check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)
```

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

### Lean 4 Calculational Proof Syntax

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

Demonstrates the basic syntax for a calculational proof in Lean 4, using the 'calc' keyword followed by a series of expressions and proofs. It highlights the required indentation and the use of '_' for alignment.

```Lean
calc
  <expr>_0  'op_1'  <expr>_1  ':='  <proof>_1
  '_'       'op_2'  <expr>_2  ':='  <proof>_2
  ...
  '_'       'op_n'  <expr>_n  ':='  <proof>_n
```

```Lean
calc <expr>_0
    '_' 'op_1' <expr>_1 ':=' <proof>_1
    '_' 'op_2' <expr>_2 ':=' <proof>_2
    ...
    '_' 'op_n' <expr>_n ':=' <proof>_n
```

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

### Inspect Product Type Operations in Lean

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

Demonstrates the use of #check to view constructors, projections, and recursion principles for the Prod type.

```lean
#check @Prod.mk
#check @Prod.fst
#check @Prod.snd
#check @Prod.rec
```

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

### Lean 4 Comment Syntax

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

Illustrates Lean 4's comment syntax, including block comments delimited by `/-` and `-/`, and line comments starting with `--`. This is essential for code readability and organization.

```Lean
/- Any text between `/-` and `-/` constitutes a comment block that is ignored by Lean. -/
-- Similarly, two dashes `--` indicate that the rest of the line contains a comment that is also ignored.
-- Comment blocks can be nested.
```

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

### Lean 4: Introduction to Exists.intro

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

Introduces the `Exists.intro` constructor for existential quantification in Lean 4. It takes a value `w` of type `α` and a proof `p w` that `p` holds for `w`, returning `∃ x, p x`.

```lean
@Exists.intro : ∀ {α : Sort u_1} {p : α → Prop} (w : α), p w → Exists p
```

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

### Lean 4 Vector Type Definition

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

Defines the `Vect` type, representing vectors of elements of type `α` with a specific length `n`. This is an example of an inductive family where the length `n` is an index.

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

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

### Lean 4: Proof of `zero_add` using `simp` tactic

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

Demonstrates a proof for the `zero_add` theorem in Lean 4, which states that adding zero to any natural number `n` results in `n`. This proof utilizes the `simp` tactic with the `add` definition and the `zero_add` theorem itself for simplification.

```Lean
open Nat
def add : Nat → Nat → Nat |
  m, zero => m
  | m, succ n => succ (add m n)

theorem zero_add : ∀ n, add zero n = n
  | zero => rfl
  | succ n => congrArg succ (zero_add n)

-- Alternative proof using simp
-- theorem zero_add' : ∀ n, add zero n = n
--   | zero =>⊢ add zero zero = zero by⊢ add zero zero = zero simp [add]
--   | succ n =>
--     n:Nat
--     ⊢ add zero n.succ = n.succ by
--     n:Nat
--     ⊢ add zero n.succ = n.succ simp [add, zero_add]
```

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

### Substitution and Congruence

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

Illustrates how to use substitution (Eq.subst or the ▸ macro) and congruence rules (congrArg, congrFun, congr) to manipulate terms.

```lean
example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2

variable (f g : α → Nat) (h₁ : a = b) (h₂ : f = g)
example : f a = f b := congrArg f h₁
example : f a = g a := congrFun h₂ a
example : f a = g b := congr h₂ h₁
```

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

### Common Existential Quantifier Identities (Lean 4)

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

Presents common logical identities involving the existential quantifier (∃) and universal quantifier (∀). Some examples require classical reasoning, indicated by the use of 'sorry' or explicit 'open Classical'.

```Lean
open Classical

variable (α : Type)
variable (p q : α → Prop)
variable (r : Prop)

-- Requires classical reasoning
example : (∃ x : α, r) → r :=
  sorry

-- Requires classical reasoning
example (a : α) : r → (∃ x : α, r) :=
  sorry

-- Requires classical reasoning
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
  sorry

-- Requires classical reasoning
example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
  sorry

example : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) :=
  sorry

example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
  sorry

example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) :=
  sorry

example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
  sorry

example : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
  sorry

-- Requires an element 'a' of type α
example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
  sorry

-- Requires an element 'a' of type α
example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
  sorry
```

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

### Lean4: `step` function using `ite` and decidable propositions

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

Example of defining a function `step` using `ite`. The condition `x < a ∨ x > b` is automatically inferred to be decidable by the Lean elaborator.

```lean
def step (a b x : Nat) : Nat := if x < a ∨ x > b then 0 else 1
```

```lean
def step : Nat → Nat → Nat → Nat := 
fun a b x =>
  @ite Nat (Or (@LT.lt Nat instLTNat x a) (@GT.gt Nat instLTNat x b))
    (@instDecidableOr (@LT.lt Nat instLTNat x a) (@GT.gt Nat instLTNat x b) (Nat.decLt x a) (Nat.decLt b x))
    (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
```

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

### Use local recursive declarations in tactic mode

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

Shows how to use 'let rec' within a proof by induction to define auxiliary lemmas or recursive proof steps.

```Lean
theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
  let rec aux (n : Nat) (as : List α) : (replicate.loop a n as).length = n + as.length := by
    match n with
    | 0 => simp [replicate.loop]
    | n+1 => simp +arith [replicate.loop, aux n]
  exact aux n []
```

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

### Understanding Lean's Type Universe Hierarchy

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

Explains and demonstrates the infinite hierarchy of types in Lean 4, starting from `Type` (an alias for `Type 0`) up to `Type 5` and beyond. It shows how each `Type n` is an element of `Type (n+1)`.

```lean
Type : Type 1
#check Type

Type 1 : Type 2
#check Type 1

Type 2 : Type 3
#check Type 2

Type 3 : Type 4
#check Type 3

Type 4 : Type 5
#check Type 4

Type : Type 1
#check Type

Type : Type 1
#check Type 0
```

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

### Lean 4: Proof involving `absurd` and Negation

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

Provides an example of a proof using `absurd` and negation in Lean 4. This demonstrates how to construct a proof for a more complex implication by leveraging the `absurd` function to handle contradictions.

```lean
variable (p q r : Prop)

example (hnp : ¬p) (hq : q) (hqp : q → p) : r := absurd (hqp hq) hnp
```

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

### Lean 4 'open' with Specific Identifiers

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

Shows how to use the 'open' command to create aliases for only specific identifiers within a namespace, rather than all of them.

```Lean
open Nat (succ zero gcd)

-- Aliases created for Nat.zero and Nat.gcd:
#check zero
#eval gcd 15 6
```

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

### Left Inverse Function Definition in Lean 4

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

Defines a left inverse function `linv` for an injective function `f` when the domain `α` is inhabited, using classical logic and dependent if-then-else expressions. This example showcases the application of `choose` and the `Classical` instance.

```Lean
open Classical
noncomputable def linv [Inhabited α] (f : α → β) : β → α := fun b : β => if ex : (∃ a : α, f a = b) then choose ex else default
```

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

### Rewrite under binders in conversion mode

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

Shows how to use 'intro' within conversion mode to enter function abstractions and rewrite sub-expressions that are otherwise inaccessible to standard tactics.

```Lean 4
example : (fun x : Nat => 0 + x) = (fun x => x) := by
  conv =>
    lhs
    intro x
    rw [Nat.zero_add]
```

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

### Lean 4 'open' with 'renaming' Clause

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

Demonstrates how to use the 'renaming' clause with the 'open' command to create aliases with different names for specific identifiers within a namespace.

```Lean
open Nat renaming mul → times, add → plus

-- Aliases created with renamed identifiers:
#eval plus (times 2 2) 3
```

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

### Reordering Constructor Cases with 'case' Tactic (Lean 4)

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

This example shows how the 'case' tactic can be used to prove goals for constructors in an order different from their declaration. The tactic intelligently matches the specified constructor to the corresponding goal.

```Lean 4
inductive Foo where | bar1 : Nat → Nat → Foo | bar2 : Nat → Nat → Nat → Foo

def silly (x : Foo) : Nat :=
by
  cases x
  case bar2 c d e =>
    -- Prove the Foo.bar2 case first
    exact e
  case bar1 a b =>
    -- Prove the Foo.bar1 case second
    exact b

```

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

### Implement tail function using auxiliary recursors

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

Demonstrates the manual implementation of a tail function for Vect using casesOn and Nat.noConfusion to handle unreachable cases. This highlights the boilerplate required without the equation compiler.

```Lean
def tailAux (v : Vect α m) : m = n + 1 → Vect α n := 
  Vect.casesOn (motive := fun x _ => x = n + 1 → Vect α n) v 
    (fun h : 0 = n + 1 => Nat.noConfusion h) 
    (fun (a : α) (m : Nat) (as : Vect α m) => fun (h : m + 1 = n + 1) => Nat.noConfusion h (fun h1 : m = n => h1 ▸ as))

def tail (v : Vect α (n+1)) : Vect α n := tailAux v rfl
```

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

### Heterogeneous Polymorphic Multiplication with Output Parameters (Nat) in Lean 4

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

Defines a heterogeneous polymorphic multiplication (`HMul`) where the result type is an output parameter. This example shows scalar multiplication for natural numbers and arrays of natural numbers.

```lean
namespace Ex

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hMul : α → β → γ

export HMul (hMul)

instance : HMul Nat Nat Nat where
  hMul := Nat.mul

instance : HMul Nat (Array Nat) (Array Nat) where
  hMul a bs := bs.map (fun b => hMul a b)

#eval hMul 4 3

#eval hMul 4 #[2, 3, 4]

end Ex
```

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

### Prove Existential from Negated Universal (Lean 4)

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

Demonstrates how to constructively prove the existence of an element satisfying a property 'p x' given the negation of the universal statement '¬∀ x, ¬ p x'. This utilizes the 'Contradiction' tactic and requires the 'Classical' module.

```Lean
open Classical

variable (p : α → Prop)

example (h : ¬ ∀ x, ¬ p x) : ∃ x, p x :=
  byContradiction (fun h1 : ¬ ∃ x, p x =>
    have h2 : ∀ x, ¬ p x := fun x => fun h3 : p x =>
      have h4 : ∃ x, p x := ⟨x, h3⟩
      show False from h1 h4
    show False from h h2
  )
```

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

### Lean 4: Local Definitions with 'let'

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

Demonstrates the use of the 'let' keyword to introduce local definitions in Lean 4. 'let a := t1; t2' is definitionally equal to replacing 'a' in 't2' with 't1'. This allows for syntactic abbreviation.

```lean
let y := 2 + 2;
y * y : Nat
```

```lean
def twice_double (x : Nat) : Nat := let y := x + x; y * y
```

```lean
let y := 2 + 2;
let z := y + y;
z * z : Nat
```

```lean
def t (x : Nat) : Nat := let y := x + x
y * y
```

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

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

### Constructing Data with 'cases' Tactic (Lean 4)

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

The 'cases' tactic can be used not only for proving propositions but also for constructing data. This example shows how to define a function that returns different values based on the constructor of an input inductive type.

```Lean 4
def f (n : Nat) : Nat :=
by
  cases n
  | zero =>
    -- Value for the 'zero' case
    exact 3
  | succ _ =>
    -- Value for the 'succ' case
    exact 7

example : f 0 = 3 := rfl
example : f 5 = 7 := rfl

```

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

### Define Multi-Parameter Functions in Lean 4

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

Illustrates the definition of functions with multiple parameters in Lean 4 using lambda abstraction. It demonstrates how to handle conditional logic within functions and shows how Lean infers parameter types when not explicitly annotated.

```Lean
fun x y => if not y then x + 1 else x + 2 : Nat → Bool → Nat
#check fun x : Nat => fun y : Bool => if not y then x + 1 else x + 2

fun x y => if not y then x + 1 else x + 2 : Nat → Bool → Nat
#check fun (x : Nat) (y : Bool) => if not y then x + 1 else x + 2

fun x y => if not y then x + 1 else x + 2 : Nat → Bool → Nat
#check fun x y => if not y then x + 1 else x + 2
```

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

### Define Structure Object with Named Fields (Lean 4)

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

Demonstrates defining a structure object using named fields, allowing for flexible order and explicit type annotation. The structure 'Point' with fields 'x' and 'y' is used as an example. The suffix ': structure-type' can be omitted if the type is inferable.

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

#check { x := 10, y := 20 : Point Nat }
#check { y := 20, x := 10 : Point _ }
#check ({ x := 10, y := 20 } : Point Nat)

example : Point Nat := { y := 20, x := 10 }
```