Mathematics in Lean

https://leanprover-community.github.io/mathematics_in_lean/
Admin
Mathematics in Lean is a comprehensive resource that teaches how to formalize various mathematical...
Tokens:138,090
Snippets:1,507
Trust Score:8.3
Update:4 months ago
Show doc for...
Tokens:
Raw
### Hello World Example

Source: https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html

A simple example demonstrating the `#eval` command in Lean.

```Lean
#eval "Hello, World!"

```

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

### Preorder Examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

Examples demonstrating irreflexivity and transitivity of the strict order in a preorder in Lean.

```Lean
variable {α : Type*} [Preorder α]
variable (a b c : α)

example : ¬a < a := by
  rw [lt_iff_le_not_ge]
  sorry

example : a < b → b < c → a < c := by
  simp only [lt_iff_le_not_ge]
  sorry
```

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

### Ordered ring arithmetic examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Examples of reasoning about arithmetic in ordered rings.

```Lean
example (h : a ≤ b) : 0 ≤ b - a := by
  sorry

example (h: 0 ≤ b - a) : a ≤ b := by
  sorry

example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c := by
  sorry
```

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

### Example of using FnUb predicate

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

An example demonstrating the use of the FnUb predicate and the 'add_le_add' tactic.

```Lean
example (hfa : FnUb f a) (hgb : FnUb g b) : FnUb (fun x ↦ f x + g x) (a + b) := by
  intro x
  dsimp
  apply add_le_add
  apply hfa
  apply hgb
```

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

### Example with DiaOneClass and tracing

Source: https://leanprover-community.github.io/mathematics_in_lean/C08_Hierarchies.html

An example demonstrating how to use `DiaOneClass₁` and enabling tracing to observe instance synthesis.

```Lean
set_option trace.Meta.synthInstance true in
example {α : Type} [DiaOneClass₁ α] (a b : α) : Prop := a ⋄ b = 𝟙

```

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

### Absolute Value and Divisibility Examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

Examples showing how to use `abs_lt` and `Nat.dvd_gcd_iff` to rewrite expressions in Lean.

```Lean
example (x : ℝ) : |x + 3| < 5 → -8 < x ∧ x < 2 := by
  rw [abs_lt]
  intro h
  constructor <;> linarith

example : 3 ∣ Nat.gcd 6 15 := by
  rw [Nat.dvd_gcd_iff]
  constructor <;> norm_num
```

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

### Conjunction and Iff Example

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

Example demonstrating the use of conjunction and iff in Lean, with a placeholder for a proof.

```Lean
theorem aux {x y : ℝ} (h : x ^ 2 + y ^ 2 = 0) : x = 0 :=
  have h' : x ^ 2 = 0 := by sorry
  eq_zero_of_pow_eq_zero h'

example (x y : ℝ) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 :=
  sorry
```

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

### Basic example with Monoid₁

Source: https://leanprover-community.github.io/mathematics_in_lean/C08_Hierarchies.html

An example of a proof using the `Monoid₁` type class and `⋄` notation.

```Lean
example {M : Type} [Monoid₁ M] {a b c : M} (hba : b ⋄ a = 𝟙) (hac : a ⋄ c = 𝟙) : b = c := by
  rw [← one_dia c, ← hba, dia_assoc, hac, dia_one b]
```

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

### Finset Sum and Product Examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html

Examples demonstrating the use of `Finset.sum` and `Finset.prod` with `Finset.range n` and their equivalence to standard summation and product notation.

```Lean
variable {α : Type*}
(s : Finset ℕ)
(f : ℕ → ℕ)
(n : ℕ)

#check Finset.sum s f
#check Finset.prod s f

open BigOperators
open Finset

example : s.sum f = ∑ x ∈ s, f x :=
  rfl

example : s.prod f = ∏ x ∈ s, f x :=
  rfl

example : (range n).sum f = ∑ x ∈ range n, f x :=
  rfl

example : (range n).prod f = ∏ x ∈ range n, f x :=
  rfl
```

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

### Ring Tactic Examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Examples demonstrating the use of the `ring` tactic to prove identities in commutative rings.

```Lean
example : c * b * a = b * (a * c) := by
  ring

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
  ring

example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  ring

example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp, hyp']
  ring
```

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

### Partial Order Example

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

Example showing the equivalence between `<` and `≤ ∧ a ≠ b` in a partial order in Lean.

```Lean
variable {α : Type*} [PartialOrder α]
variable (a b : α)

example : a < b ↔ a ≤ b ∧ a ≠ b := by
  rw [lt_iff_le_not_ge]
  sorry
```

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

### Bounded quantifiers examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C04_Sets_and_Functions.html

Examples demonstrating the usage of bounded quantifiers like `∀ x ∈ s, ...` and `∃ x ∈ s, ...`.

```Lean
variable (s t : Set ℕ)

example (h₀ : ∀ x ∈ s, ¬Even x) (h₁ : ∀ x ∈ s, Prime x) : ∀ x ∈ s, ¬Even x ∧ Prime x := by
  intro x xs
  constructor
  · apply h₀ x xs
  apply h₁ x xs

example (h : ∃ x ∈ s, ¬Even x ∧ Prime x) : ∃ x ∈ s, Prime x := by
  rcases h with ⟨x, xs, _, prime_x⟩
  use x, xs
```

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

### Field Simplification Example

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

An example demonstrating the use of field_simp and ring tactics for simplifying expressions with denominators.

```Lean
example (x y : ℝ) (h : x - y ≠ 0) : (x ^ 2 - y ^ 2) / (x - y) = x + y := by
  field_simp [h]
  ring
```

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

### Example demonstrating custom SMul instance for ℤ

Source: https://leanprover-community.github.io/mathematics_in_lean/C08_Hierarchies.html

This example verifies that the custom `SMul` instance for `ℕ` and `ℤ` (defined as `mySMul`) is used, showing that scalar multiplication behaves as expected with the integer multiplication.

```Lean
example (n : ℕ) (m : ℤ) : SMul.smul (self := mySMul) n m = n * m := rfl
```

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

### Commutative ring example

Source: https://leanprover-community.github.io/mathematics_in_lean/C09_Groups_and_Rings.html

An example demonstrating the `ring` tactic for proving an identity in a commutative ring.

```Lean
example {R : Type*} [CommRing R] (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring
```

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

### Invertible Matrix Proof Example

Source: https://leanprover-community.github.io/mathematics_in_lean/C10_Linear_Algebra.html

An example of proving matrix inversion properties using the `Invertible` type class and `simp` tactic.

```Lean
example : !![(1 : ℝ), 2; 3, 4]⁻¹ * !![(1 : ℝ), 2; 3, 4] = 1 := by
  have : Invertible !![(1 : ℝ), 2; 3, 4] := by
    apply Matrix.invertibleOfIsUnitDet
    norm_num
  simp


```

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

### Examples of InjOn and range

Source: https://leanprover-community.github.io/mathematics_in_lean/C04_Sets_and_Functions.html

Examples demonstrating the use of `InjOn` and `range` with specific functions and sets.

```Lean
open Set Real

example : InjOn log { x | x > 0 } := by
  intro x xpos y ypos e
  calc
    x = exp (log x) := by rw [exp_log xpos]
    _ = exp (log y) := by rw [e]
    _ = y := by rw [exp_log ypos]


example : range exp = { y | y > 0 } := by
  ext y; constructor
  · rintro ⟨x, rfl⟩
    apply exp_pos
  intro ypos
  use log y
  rw [exp_log ypos]
```

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

### Declaring variables outside an example

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Shows how to declare variables once outside an example or theorem, which Lean includes automatically.

```Lean
variable (a b c d e f : ℝ)

example (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h', ← mul_assoc, h, mul_assoc]

```

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

### Example using One₁

Source: https://leanprover-community.github.io/mathematics_in_lean/C08_Hierarchies.html

Demonstrates a basic example where `One₁ α` is used to provide the `one` element.

```Lean
example (α : Type) [One₁ α] : α := One₁.one
```

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

### Monoid and AddCommMonoid examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C09_Groups_and_Rings.html

Examples demonstrating the properties of Monoids and Additive Commutative Monoids in Lean.

```Lean
example {M : Type*} [Monoid M] (x : M) : x * 1 = x := mul_one x

example {M : Type*} [AddCommMonoid M] (x y : M) : x + y = y + x := add_comm x y
```

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

### Absorption laws for lattices

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Examples of proving the absorption laws for lattices.

```Lean
theorem absorb1 : x ⊓ (x ⊔ y) = x := by
  sorry

theorem absorb2 : x ⊔ x ⊓ y = x := by
  sorry
```

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

### Composition of Tendsto₁

Source: https://leanprover-community.github.io/mathematics_in_lean/C11_Topology.html

An example demonstrating the composition of Tendsto₁.

```Lean
example {X Y Z : Type*} {F : Filter X} {G : Filter Y} {H : Filter Z} {f : X → Y} {g : Y → Z}
    (hf : Tendsto₁ f F G) (hg : Tendsto₁ g G H) : Tendsto₁ (g ∘ f) F H :=
  sorry
```

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

### Surjective Function Example 1

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

An example defining and proving surjectivity for a function, using intro and use tactics.

```Lean
example {c : ℝ} : Surjective fun x ↦ x + c := by
  intro x
  use x - c
  dsimp; ring
```

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

### Checking a lemma about the product of filters and limits.

Source: https://leanprover-community.github.io/mathematics_in_lean/C11_Topology.html

This example checks the lemma `le_inf_iff` and provides an example of how to express the convergence of a function to a pair of points in terms of the convergence of its components.

```Lean
#check le_inf_iff

example (f : ℕ → ℝ × ℝ) (x₀ y₀ : ℝ) :
    Tendsto f atTop (𝓝 (x₀, y₀)) ↔
      Tendsto (Prod.fst ∘ f) atTop (𝓝 x₀) ∧ Tendsto (Prod.snd ∘ f) atTop (𝓝 y₀) := 
  sorry

```

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

### Examples of FnLb and FnUb

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

These examples demonstrate the usage of FnLb and FnUb predicates for functions operating on real numbers.

```Lean
example (hfa : FnLb f a) (hgb : FnLb g b) : FnLb (fun x ↦ f x + g x) (a + b) :=
  sorry

example (nnf : FnLb f 0) (nng : FnLb g 0) : FnLb (fun x ↦ f x * g x) 0 :=
  sorry

example (hfa : FnUb f a) (hgb : FnUb g b) (nng : FnLb g 0) (nna : 0 ≤ a) :
    FnUb (fun x ↦ f x * g x) (a * b) :=
  sorry
```

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

### Bounded Union Example

Source: https://leanprover-community.github.io/mathematics_in_lean/C04_Sets_and_Functions.html

An example related to bounded union, suggesting `apply eq_univ_of_forall` and `Nat.exists_infinite_primes`.

```Lean
example : (⋃ p ∈ primes, { x | x ≤ p }) = univ := by
  sorry

```

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

### Lattice associativity and commutativity examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Examples of proving associativity for join (⊔) and infimum (⊓) operations in a lattice.

```Lean
example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) := by
  sorry
```

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

### Elementary Integration Examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C13_Integration_and_Measure_Theory.html

Examples of integrating elementary functions on finite intervals in ℝ, including the integral of x and 1/x.

```Lean
open MeasureTheory

open Interval
-- this introduces the notation `[[a, b]]` for the segment from `min a b` to `max a b`

example (a b : ℝ) : (∫ x in a..b, x) = (b ^ 2 - a ^ 2) / 2 :=
  integral_id

example {a b : ℝ} (h : (0 : ℝ) ∉ [[a, b]]) : (∫ x in a..b, 1 / x) = Real.log (b / a) :=
  integral_one_div h
```

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

### Local Inverse Theorem examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C12_Differential_Calculus.html

Examples demonstrating the local inverse function obtained from strict differentiability and its properties.

```Lean
section LocalInverse
variable [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E}

example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) : F → E :=
  HasStrictFDerivAt.localInverse f f' a hf

example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    ∀ᶠ x in 𝓝 a, hf.localInverse f f' a (f x) = x :=
  hf.eventually_left_inverse

example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    ∀ᶠ x in 𝓝 (f a), f (hf.localInverse f f' a x) = x :=
  hf.eventually_right_inverse

example {f : E → F} {f' : E ≃L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf) (f'.symm : F →L[𝕜] E) (f a) :=
  HasStrictFDerivAt.to_localInverse hf

end LocalInverse
```

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

### Quotient group structure and projection

Source: https://leanprover-community.github.io/mathematics_in_lean/C09_Groups_and_Rings.html

Examples demonstrating how to obtain the group structure on a quotient group G ⧸ H when H is a normal subgroup, and how to get the quotient map as a group morphism.

```Lean
noncomputable section QuotientGroup

example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : Group (G ⧸ H) := inferInstance

example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : G →* G ⧸ H :=
  QuotientGroup.mk' H
```

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

### Monotonicity examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

Examples demonstrating the concept of monotonicity for functions in Lean.

```Lean
example {c : ℝ} (mf : Monotone f) (nnc : 0 ≤ c) : Monotone fun x ↦ c * f x :=
  sorry

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f (g x) :=
  sorry
```

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

### Constructing proofs (proof terms)

Source: https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html

Shows how to construct proofs as expressions of a proposition's type, using `rfl` for reflexivity and `sorry` as a placeholder.

```Lean
theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

#check hard

```

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

### Using `eq_zero_or_eq_zero_of_mul_eq_zero`

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

Examples demonstrating the use of the `eq_zero_or_eq_zero_of_mul_eq_zero` theorem to prove statements about real numbers.

```Lean
example {x : ℝ} (h : x ^ 2 = 1) : x = 1 ∨ x = -1 :=
by
  sorry

example {x y : ℝ} (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y :=
by
  sorry
```

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

### Using `apply?` to find relevant theorems

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Demonstrates how to use the `apply?` tactic to find and apply relevant theorems from the library. The example shows applying `sq_nonneg`.

```Lean
example : 0 ≤ a ^ 2 := by
  -- apply?
  exact sq_nonneg a

```

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

### Existential Quantifier Example 1

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

An example demonstrating the use of the existential quantifier.

```Lean
example (divab : a ∣ b) (divac : a ∣ c) : a ∣ b + c := by
  sorry
```

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

### Group identity example

Source: https://leanprover-community.github.io/mathematics_in_lean/C09_Groups_and_Rings.html

An example of a basic group identity in Lean.

```Lean
example {G : Type*} [Group G] (x : G) : x * x⁻¹ = 1 := mul_inv_cancel x
```

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

### Using the intro tactic

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

Demonstrates using the 'intro' tactic to introduce universally quantified variables and hypotheses.

```Lean
theorem my_lemma3 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε epos ele1 xlt ylt
  sorry
```

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

### Using `apply` and `exact` tactics

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Shows different ways to use the `apply` and `exact` tactics to prove a goal, including using dots for focusing goals and providing proof terms directly.

```Lean
example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans
  · apply h₀
  · apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans h₀
  apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z :=
  le_trans h₀ h₁

example (x : ℝ) : x ≤ x := by
  apply le_refl

example (x : ℝ) : x ≤ x :=
  le_refl x
```

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

### Basic rewrite example

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Demonstrates the use of the `rw` tactic with `mul_comm` and `mul_assoc` to prove an equality.

```Lean
example (a b c : ℝ) : a * b * c = b * (a * c) := by
  rw [mul_comm a b]
  rw [mul_assoc b a c]

```

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

### Proof of min commutativity using apply and le_min

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

This example demonstrates a proof that `min a b` is equal to `min b a` using the `apply` and `le_min` tactics, along with `show` to structure the proof.

```Lean
example : min a b = min b a := by
  apply le_antisymm
  · show min a b ≤ min b a
    apply le_min
    · apply min_le_right
    apply min_le_left
  · show min b a ≤ min a b
    apply le_min
    · apply min_le_right
    apply min_le_left
```

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

### Negation Monotonicity Example

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

Example demonstrating how to prove that negation is not a nondecreasing function in Lean.

```Lean
theorem not_monotone_iff {f : ℝ → ℝ} : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by
  rw [Monotone]
  push_neg
  rfl

example : ¬Monotone fun x : ℝ ↦ -x := by
  sorry
```

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

### Example of using `apply?`

Source: https://leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html

Illustrates how to use the `apply?` tactic to find a suitable theorem for proving equality when one side is a product and a non-zero factor is known.

```Lean
example (a b c : Nat) (h : a * b = a * c) (h' : a ≠ 0) : b = c :=
  -- apply? suggests the following:
  (mul_right_inj' h').mp h
```

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

### Checking expressions and their types

Source: https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html

Demonstrates the use of the `#check` command to inspect the types of expressions and the definition of a simple function.

```Lean
#check 2 + 2

def f (x : ℕ) :=
  x + 3

#check f

```

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

### Distributivity implication examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Examples showing that one distributivity law implies the other in a lattice.

```Lean
variable {α : Type*}
[Lattice α]
variable (a b c : α)

example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) := by
  sorry

example (h : ∀ x y z : α, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c := by
  sorry
```

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

### Accessing polynomial coefficients

Source: https://leanprover-community.github.io/mathematics_in_lean/C09_Groups_and_Rings.html

Examples showing how to access coefficients of a polynomial using Polynomial.coeff.

```Lean
example {R : Type*} [CommRing R] (r:R) : (C r).coeff 0 = r := by simp
```

```Lean
example {R : Type*} [CommRing R] : (X ^ 2 + 2 * X + C 3 : R[X]).coeff 1 = 2 := by simp
```

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

### Finsupp.linearCombination_apply_of_mem_supported

Source: https://leanprover-community.github.io/mathematics_in_lean/C10_Linear_Algebra.html

This example demonstrates the application of Finsupp.linearCombination, showing that it is equivalent to a sum over a finite set containing the support of the coefficients.

```Lean
example (c : ι →₀ K) (f : ι → V) (s : Finset ι) (h : c.support ⊆ s) :
    Finsupp.linearCombination K f c = ∑ i ∈ s, c i • f i :=
  Finsupp.linearCombination_apply_of_mem_supported K h
```

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

### Proof involving `ring` and `calc` tactics

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

An example demonstrating the use of the `ring` tactic and the `calc` command for proving an inequality, highlighting the use of spaces around binary operations and the preference for `≤` over `≥`.

```Lean
example : 2*a*b ≤ a^2 + b^2 := by
  have h : 0 ≤ a^2 - 2*a*b + b^2
  calc
    a^2 - 2*a*b + b^2 = (a - b)^2 := by ring
    _ ≥ 0 := by apply pow_two_nonneg

  calc
    2*a*b = 2*a*b + 0 := by ring
    _ ≤ 2*a*b + (a^2 - 2*a*b + b^2) := add_le_add (le_refl _) h
    _ = a^2 + b^2 := by ring

```

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

### Automated tactic proof using simplification

Source: https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html

Demonstrates using Lean's simplifier with specific rules to automatically prove the parity theorem.

```Lean
example : ∀ m n : Nat, Even n → Even (m * n) := by
  intros; simp [*, parity_simps]

```

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

### Modulo operation example

Source: https://leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html

A simple Lean example demonstrating the modulo operation.

```Lean
example : 27 % 4 = 3 := by norm_num
```

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

### Nth_rw Tactic Example

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

An example showing how to use `nth_rw` to replace a specific occurrence of an expression.

```Lean
example (a b c : ℕ) (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := by
  nth_rw 2 [h]
  rw [add_mul]
```

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

### Using `linarith` with additional inequalities

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Demonstrates how `linarith` can use additional inequalities passed as arguments.

```Lean
example (h : 2 * a ≤ 3 * b) (h' : 1 ≤ a) (h'' : d = 2) : d + a ≤ 5 * b := by
  linarith

example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a + exp b ≤ 3 * a + exp c := by
  linarith [exp_le_exp.mpr h']
```

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

### Inductively Defined Type Example

Source: https://leanprover-community.github.io/mathematics_in_lean/C06_Discrete_Mathematics.html

An example demonstrating an inductively defined type and its evaluation.

```Lean
A.subst n C).eval v = A.eval (fun m => if m = n then C.eval v else v m) := sorry
```

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

### Surjectivity Hypothesis Example

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

An example showing how to use a surjectivity hypothesis by applying it to a value, and using rcases.

```Lean
example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, f x ^ 2 = 4 := by
  rcases h 2 with ⟨x, hx⟩
  use x
  rw [hx]
  norm_num
```

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

### Lagrange's Theorem and Sylow's First Theorem

Source: https://leanprover-community.github.io/mathematics_in_lean/C09_Groups_and_Rings.html

Examples demonstrating Lagrange's theorem and Sylow's first theorem using Mathlib.

```Lean
open scoped Classical


example {G : Type*} [Group G] (G' : Subgroup G) : Nat.card G' ∣ Nat.card G := 
  ⟨G'.index, mul_comm G'.index _ ▸ G'.index_mul_card.symm⟩

open Subgroup

example {G : Type*} [Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact p.Prime] 
    (hdvd : p ^ n ∣ Nat.card G) : ∃ K : Subgroup G, Nat.card K = p ^ n := 
  Sylow.exists_subgroup_card_pow_prime p hdvd
```

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

### Surjective Function Example 2

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

An example to prove surjectivity for a function involving multiplication, using a hypothesis.

```Lean
example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
  sorry
```

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

### Proving function equality with `ext`

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

Demonstrates the use of the `ext` tactic to prove that two functions are equal by showing they return the same value for all arguments. This example proves that (x + y)^2 is equal to x^2 + 2xy + y^2.

```Lean
example : (fun x y : ℝ ↦ (x + y) ^ 2) = fun x y : ℝ ↦ x ^ 2 + 2 * x * y + y ^ 2 := by
  ext
  ring
```

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

### Checking library theorems `le_refl` and `le_trans`

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Demonstrates how to use `#check` to inspect the type signature of library theorems.

```Lean
#check (le_refl : ∀ a : ℝ, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
```

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

### Example: Unit element in a submonoid

Source: https://leanprover-community.github.io/mathematics_in_lean/C08_Hierarchies.html

An example demonstrating that the unit element `1` belongs to any submonoid `N`.

```Lean
example [Monoid M] (N : Submonoid₁ M) : 1 ∈ N := N.one_mem
```

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

### Using `linarith` for linear arithmetic goals

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Shows how the `linarith` tactic can solve goals involving linear arithmetic, simplifying proofs that might otherwise require `apply?`.

```Lean
example : 2*a*b ≤ a^2 + b^2 := by
  have h : 0 ≤ a^2 - 2*a*b + b^2
  calc
    a^2 - 2*a*b + b^2 = (a - b)^2 := by ring
    _ ≥ 0 := by apply pow_two_nonneg
  linarith

```

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

### Using the calc command for proof

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

Demonstrates using the 'calc' command to structure a proof with intermediate steps.

```Lean
theorem my_lemma4 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε epos ele1 xlt ylt
  calc
    |x * y| = |x| * |y| := sorry
    _ ≤ |x| * ε := sorry
    _ < 1 * ε := sorry
    _ = ε := sorry
```

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

### MonoidHom and AddMonoidHom examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C09_Groups_and_Rings.html

Examples showcasing the behavior of Monoid Homomorphisms and Additive Monoid Homomorphisms.

```Lean
example {M N : Type*} [Monoid M] [Monoid N] (x y : M) (f : M →* N) : f (x * y) = f x * f y :=
  f.map_mul x y

example {M N : Type*} [AddMonoid M] [AddMonoid N] (f : M →+ N) : f 0 = 0 :=
  f.map_zero
```

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

### Checking mathematical statements (Prop type)

Source: https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html

Illustrates checking the type of a mathematical statement, which is `Prop`, and defining a theorem.

```Lean
#check 2 + 2 = 4

def FermatLastTheorem :=
  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

#check FermatLastTheorem

```

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

### Matrix Equality and Multiplication Examples

Source: https://leanprover-community.github.io/mathematics_in_lean/C10_Linear_Algebra.html

Demonstrates the difference between point-wise multiplication and matrix multiplication for functions and matrices in Lean.

```Lean
section

example : (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) = !![1, 1; 1, 1] := by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

example : (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) * (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) = !![1, 1; 1, 1] := by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

example : !![1, 1; 1, 1] * !![1, 1; 1, 1] = !![2, 2; 2, 2] := by
  norm_num

```
```

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

### Calc proof with sorry tactics

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Shows how to outline a calc proof using 'sorry' tactics for justification.

```Lean
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
  calc
    (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
      sorry
    _ = a * a + (b * a + a * b) + b * b := by
      sorry
    _ = a * a + 2 * (a * b) + b * b := by
      sorry

```

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

### Example of flip operation

Source: https://leanprover-community.github.io/mathematics_in_lean/C06_Discrete_Mathematics.html

An example demonstrating the effect of the 'flip' operation on a specific binary tree.

```Lean
example: flip  (node (node empty (node empty empty)) (node empty empty)) = node (node empty empty) (node (node empty empty) empty) := sorry
```

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

### Structured proof using calc

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Demonstrates a structured proof using the 'calc' keyword.

```Lean
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
  calc
    (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
      rw [mul_add, add_mul, add_mul]
    _ = a * a + (b * a + a * b) + b * b := by
      rw [← add_assoc, add_assoc (a * a)]
    _ = a * a + 2 * (a * b) + b * b := by
      rw [mul_comm b a, ← two_mul]

```

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

### Example: Direct image of a submonoid

Source: https://leanprover-community.github.io/mathematics_in_lean/C08_Hierarchies.html

An example showing how to take the direct image of a submonoid `N` under a map `f`.

```Lean
example [Monoid M] (N : Submonoid₁ M) (α : Type) (f : M → α) := f '' N
```

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

### Exercises on additive inverses

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Exercises to prove properties related to additive inverses and equality.

```Lean
theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
  sorry

theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := by
  sorry

theorem neg_zero : (-0 : R) = 0 := by
  apply neg_eq_of_add_eq_zero
  rw [add_zero]

theorem neg_neg (a : R) : - -a = a := by
  sorry
```

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

### Complex divisibility example

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

A more complex example involving sums and powers, requiring the user to find appropriate theorems.

```Lean
example (h : x ∣ w) : x ∣ y * (x * z) + x ^ 2 + w ^ 2 := by
  sorry
end

```

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

### Replicating Rows and Columns

Source: https://leanprover-community.github.io/mathematics_in_lean/C10_Linear_Algebra.html

Demonstrates generating matrices with identical rows or columns using `Matrix.replicateRow` and `Matrix.replicateCol`.

```Lean
#eval replicateRow (Fin 1) ![1, 2] -- !![1, 2]

#eval replicateCol (Fin 1) ![1, 2] -- !![1; 2]


```

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

### Monotone predicate example

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

This example demonstrates how to express the property of a function being monotone using Lean's type system.

```Lean
example (f : ℝ → ℝ) (h : Monotone f) : ∀ {a b}, a ≤ b → f a ≤ f b :=
  @h
```

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

### Using `rw` with implicit arguments

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Shows how `rw` can be used with implicit arguments, where Lean tries to match patterns automatically.

```Lean
example (a b c : ℝ) : a * b * c = b * c * a := by
  rw [mul_assoc]
  rw [mul_comm]

```

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

### Example: Element coercion from submonoid

Source: https://leanprover-community.github.io/mathematics_in_lean/C08_Hierarchies.html

An example illustrating the coercion of an element `x` from a submonoid `N` to an element of `M` that belongs to `N`.

```Lean
example [Monoid M] (N : Submonoid₁ M) (x : N) : (x : M) ∈ N := x.property
```

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

### Commutative semiring example

Source: https://leanprover-community.github.io/mathematics_in_lean/C09_Groups_and_Rings.html

An example showing the `ring` tactic applied to a commutative semiring, specifically natural numbers.

```Lean
example (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring
```

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

### Divisibility by a multiple

Source: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Shows how to prove that `x` divides `y * x * z` using `dvd_mul_of_dvd_left` and `dvd_mul_left`.

```Lean
example : x ∣ y * x * z := by
  apply dvd_mul_of_dvd_left
  apply dvd_mul_left

```

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

### Example of Continuous Function

Source: https://leanprover-community.github.io/mathematics_in_lean/C08_Hierarchies.html

An example demonstrating the use of a predicate for continuous functions, showing `Continuous (id : ℝ → ℝ)`.

```Lean
example : Continuous (id : ℝ → ℝ) := continuous_id
```

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

### Mapping and comapping subgroups

Source: https://leanprover-community.github.io/mathematics_in_lean/C09_Groups_and_Rings.html

Examples showing how to map a subgroup using a group morphism (f) and how to comap a subgroup.

```Lean
example {G H : Type*} [Group G] [Group H] (G' : Subgroup G) (f : G →* H) : Subgroup H :=
  Subgroup.map f G'

example {G H : Type*} [Group G] [Group H] (H' : Subgroup H) (f : G →* H) : Subgroup G :=
  Subgroup.comap f H'
```

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

### Example: Intersection of submonoids

Source: https://leanprover-community.github.io/mathematics_in_lean/C08_Hierarchies.html

An example showing that the intersection of two submonoids `N` and `P` is also a submonoid, represented by the infimum operator `⊓`.

```Lean
example [Monoid M] (N P : Submonoid₁ M) : Submonoid₁ M := N ⊓ P
```

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

### Group isomorphism example

Source: https://leanprover-community.github.io/mathematics_in_lean/C09_Groups_and_Rings.html

An example demonstrating the composition of group isomorphisms, showing that composing a map with its inverse yields the identity isomorphism.

```Lean
example {G H : Type*} [Group G] [Group H] (f : G ≃* H) : 
    f.trans f.symm = MulEquiv.refl G :=
  f.self_trans_symm
```

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

### Proof of Monotone for sum of functions (proof term style)

Source: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html

This example demonstrates the same proof as above but using a proof term style, which is often more concise for short proofs.

```Lean
example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x :=
  fun _a _b aleb ↦ add_le_add (mf aleb) (mg aleb)
```

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

### Irrational Roots Example

Source: https://leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html

An example demonstrating properties of irrational roots using Lean's number theory functions.

```Lean
example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m ^ k = r * n ^ k) {p : ℕ} :
    k ∣ r.factorization p := by
  rcases r with _ | r
  · simp
  have npow_nz : n ^ k ≠ 0 := fun npowz ↦ nnz (eq_zero_of_pow_eq_zero npowz)
  have eq1 : (m ^ k).factorization p = k * m.factorization p := by
    sorry
  have eq2 : ((r + 1) * n ^ k).factorization p =
      k * n.factorization p + (r + 1).factorization p := by
    sorry
  have : r.succ.factorization p = k * m.factorization p - k * n.factorization p := by
    rw [← eq1, pow_eq, eq2, add_comm, Nat.add_sub_cancel]
  rw [this]
  sorry
```
Tokens:
Raw