### Prove Inequality with Induction from a Starting Point (Lean)

Source: https://hrmacbeth.github.io/math2001/06_Induction

Demonstrates how to prove an inequality (3^n >= 2^n + 5) for natural numbers n >= 2 using induction starting from n=2 in Lean. It shows the setup for base case and inductive step using the `induction_from_starting_point` tactic.

```Lean
example {n : ℕ} (hn : 2 ≤ n) : (3:ℤ) ^ n ≥ 2 ^ n + 5 := by
  induction_from_starting_point n, hn with k hk IH
  · -- base case
    numbers
  · -- inductive step
    calc (3:ℤ) ^ (k + 1) = 2 * 3 ^ k + 3 ^ k := by ring
      _ ≥ 2 * (2 ^ k + 5) + 3 ^ k := by rel [IH]
      _ = 2 ^ (k + 1) + 5 + (5 + 3 ^ k) := by ring
      _ ≥ 2 ^ (k + 1) + 5 := by extra
```

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

### Example Proof: Equation Manipulation with Addition/Subtraction (Lean)

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

Shows how to solve an equation by combining addition/subtraction operations with existing hypotheses. This example is useful for problems where simple rearrangement is required.

```lean
example {w : ℚ} (h1 : 3 * w + 1 = 4) : w = 1 :=
  sorry

```

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

### Example Proof: Simple Equation Manipulation (Lean)

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

Demonstrates a basic proof in Lean by manipulating a hypothesis to derive a conclusion. This example involves creating one side of a hypothesis using existing terms and known equations.

```lean
example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 :=
  sorry

```

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

### Example Proof: Polynomial Identity (Lean)

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

Demonstrates a proof involving higher-degree polynomial terms. This example utilizes a polynomial identity, verified by expansion and simplification, to establish the desired result.

```lean
example {z : ℝ} (h1 : z ^ 2 - 2 = 0) : z ^ 4 - z ^ 3 - z ^ 2 + 2 * z + 1 = 3 :=
  sorry

```

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

### Example Proof: Simpler System of Simultaneous Equations (Lean)

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

Presents another example of solving simultaneous equations by forming a linear combination of the given hypotheses. This proof aims to isolate and find the value of 'u'.

```lean
example {u v : ℚ} (h1 : u + 2 * v = 4) (h2 : u - 2 * v = 6) : u = 5 :=
  sorry

```

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

### Example Proof: Higher Degree Equation (Lean)

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

Illustrates proving an equation involving terms of degree greater than one. This example demonstrates algebraic manipulation, substitution, and simplification to reach the final result.

```lean
example {a b : ℚ} (h1 : a - 3 = 2 * b) : a ^ 2 - a + 3 = 4 * b ^ 2 + 10 * b + 9 :=
  sorry

```

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

### Prove n! is Even for n >= 2 in Lean

Source: https://hrmacbeth.github.io/math2001/06_Induction

Demonstrates a Lean example for proving that n! is even for all natural numbers n where n is greater than or equal to 2. The proof suggests using induction starting from n=2.

```Lean
example {n : ℕ} (hn : 2 ≤ n) : Nat.Even (n !) := by
  sorry
```

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

### Example Proof: Complex System of Equations (Lean)

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

Shows how to solve a more complex system of simultaneous equations by taking varying multiples of hypotheses. This example involves canceling one variable and then solving for the other.

```lean
example {x y : ℝ} (h1 : x + y = 4) (h2 : 5 * x - 3 * y = 4) : x = 2 :=
  sorry

```

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

### Lean Induction Proof Setup

Source: https://hrmacbeth.github.io/math2001/06_Induction

Demonstrates how to set up an induction proof in Lean using the `simple_induction` tactic. It shows the goal state before and after applying the tactic, highlighting the separation into base and inductive cases.

```lean
example (n : ℕ) : 2 ^ n ≥ n + 1 := by
  simple_induction n with k IH
  · -- base case
    numbers
  · -- inductive step
    calc 2 ^ (k + 1) = 2 * 2 ^ k := by ring
      _ ≥ 2 * (k + 1) := by rel [IH]
      _ = (k + 1 + 1) + k := by ring
      _ ≥ k + 1 + 1 := by extra
```

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

### Example Proof: Algebra I Style Equation (Lean)

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

Illustrates solving a classic Algebra I-style equation using proof by calculation. It demonstrates how to derive the solution by 'creating' one side of the hypothesis through algebraic steps.

```lean
example {x : ℤ} (h1 : 2 * x + 3 = x) : x = -3 :=
  sorry

```

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

### Lean Proof for Simple Integer Equality

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

A basic Lean proof example demonstrating the calculation of an integer's value based on given hypotheses. The `sorry` placeholder indicates where the proof steps should be filled in.

```Lean
example {a b : ℤ} (h1 : a = 2 * b + 5) (h2 : b = 3) : a = 11 :=
  sorry

```

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

### Apply push_neg Tactic in Lean (Multiple Examples)

Source: https://hrmacbeth.github.io/math2001/05_Logic

Demonstrates the use of the `#push_neg` tactic in Lean to negate various quantified statements. These examples are for practice and checking work.

```Lean
#push_neg ¬(∀ n : ℕ, n > 0 → ∃ k l : ℕ, k < n ∧ l < n ∧ k ≠ l)
#push_neg ¬(∀ m : ℤ, m ≠ 2 → ∃ n : ℤ, n ^ 2 = m)
#push_neg ¬(∃ x : ℝ, ∀ y : ℝ, ∃ m : ℤ, x < y * m ∧ y * m < m)
#push_neg ¬(∃ x : ℝ, ∀ q : ℝ, q > x → ∃ m : ℕ, q ^ m > x)
```

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

### Lean Proof: Implication Introduction

Source: https://hrmacbeth.github.io/math2001/05_Logic

Shows how to prove an implication in Lean using the 'intro' and 'left' tactics. This example demonstrates proving P implies (P or not Q).

```Lean
example (P Q : Prop) : P → (P ∨ ¬ Q) := by
  intro hP
  left
  apply hP
```

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

### Example Proof: System of Simultaneous Equations (Lean)

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

Demonstrates solving a system of simultaneous equations by combining hypotheses. This method avoids explicit variable elimination steps, presenting a direct calculation to find the value of 'x'.

```lean
example {x y : ℤ} (h1 : 2 * x - y = 4) (h2 : y - x + 1 = 2) : x = 5 :=
  sorry

```

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

### Set up Induction for 'Sufficiently Large' Numbers (Lean)

Source: https://hrmacbeth.github.io/math2001/06_Induction

Outlines the structure for proving a property (2^n >= n^2) that holds for all sufficiently large natural numbers using Lean. It uses `dsimp` and `use` to establish the starting point for the induction.

```Lean
example : forall_sufficiently_large n : ℕ, 2 ^ n ≥ n ^ 2 := by
  dsimp
  use 4
  intro n hn
  induction_from_starting_point n, hn with k hk IH
  · -- base case
    sorry
  · -- inductive step
    sorry
```

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

### Prove or Disprove Set Equality (Lean)

Source: https://hrmacbeth.github.io/math2001/09_Sets

Illustrates proving or disproving the equality of two sets using Lean. Includes examples with conditions on elements and modular arithmetic.

```lean
example : {n : ℤ | Even n} = {a : ℤ | a ≡ 6 [ZMOD 2]} := by
  sorry

example : {n : ℤ | Even n} ≠ {a : ℤ | a ≡ 6 [ZMOD 2]} := by
  sorry
```

```lean
example : {t : ℝ | t ^ 2 - 5 * t + 4 = 0} = {4} := by
  sorry

example : {t : ℝ | t ^ 2 - 5 * t + 4 = 0} ≠ {4} := by
  sorry
```

```lean
example : {k : ℤ | 8 ∣ 6 * k} = {l : ℤ | 8 ∣ l} := by
  sorry

example : {k : ℤ | 8 ∣ 6 * k} ≠ {l : ℤ | 8 ∣ l} := by
  sorry
```

```lean
example : {k : ℤ | 7 ∣ 9 * k} = {l : ℤ | 7 ∣ l} := by
  sorry

example : {k : ℤ | 7 ∣ 9 * k} ≠ {l : ℤ | 7 ∣ l} := by
  sorry
```

```lean
example : {1, 2, 3} = {1, 2} := by
  sorry

example : {1, 2, 3} ≠ {1, 2} := by
  sorry
```

```lean
example : {x : ℝ | x ^ 2 + 3 * x + 2 = 0} = {-1, -2} := by
  sorry
```

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

### Propositional Logic Proofs in Lean

Source: https://hrmacbeth.github.io/math2001/05_Logic

Provides examples of proving basic propositional logic statements in Lean. These exercises cover conjunction, disjunction, implication, negation, and biconditional logical connectives.

```Lean
example {P Q : Prop} (h : P ∧ Q) : P ∨ Q := by
  sorry

example {P Q R : Prop} (h1 : P → Q) (h2 : P → R) (h3 : P) : Q ∧ R := by
  sorry

example (P : Prop) : ¬(P ∧ ¬ P) := by
  sorry

example {P Q : Prop} (h1 : P ↔ ¬ Q) (h2 : Q) : ¬ P := by
  sorry

example {P Q : Prop} (h1 : P ∨ Q) (h2 : Q → P) : P := by
  sorry

example {P Q : Prop} (h1 : P ↔ Q) : (P ∧ R) ↔ (Q ∧ R) := by
  sorry

example (P : Prop) : (P ∧ P) ↔ P := by
  sorry

example (P Q : Prop) : (P ∨ Q) ↔ (Q ∨ P) := by
  sorry

example (P Q : Prop) : ¬(P ∨ Q) ↔ (¬P ∧ ¬Q) := by
  sorry
```

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

### Prove Set Inclusion for Finite Sets in Lean

Source: https://hrmacbeth.github.io/math2001/09_Sets

Shows how to prove that a finite set is a subset of another set defined by a property. This example uses Lean's `dsimp`, `Set.subset_def`, `intro`, `obtain`, and `addarith` tactics.

```Lean
example : {1, 3, 6} ⊆ {t : ℚ | t < 10} := by
  dsimp [Set.subset_def]
  intro t ht
  obtain h1 | h3 | h6 := ht
  · addarith [h1]
  · addarith [h3]
  · addarith [h6]
```

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

### Prove p=-11 given p+4q=1 and q-1=2

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

This Lean exercise involves proving an integer equality. Starting with `p + 4*q = 1` and `q - 1 = 2`, the proof demonstrates that `p` must be -11. This showcases basic arithmetic and substitution for integers.

```lean
example {p q : ℤ} (h1 : p + 4 * q = 1) (h2 : q - 1 = 2) : p = -11 :=
  sorry

```

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

### Prove Inequality (n+1)! >= 2^n in Lean

Source: https://hrmacbeth.github.io/math2001/06_Induction

Demonstrates a Lean example for proving the inequality (n+1)! >= 2^n for all natural numbers n. The proof is structured using induction.

```Lean
example (n : ℕ) : (n + 1)! ≥ 2 ^ n := by
  sorry
```

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

### Prove 2^n >= n^3 for Large n (Lean)

Source: https://hrmacbeth.github.io/math2001/06_Induction

A Lean proof setup using `dsimp` to handle the 'sufficiently large' condition for proving 2^n >= n^3.

```Lean
example : forall_sufficiently_large n : ℕ, 2 ^ n ≥ n ^ 3 := by
  dsimp
  sorry
```

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

### First-Order Logic Proofs in Lean

Source: https://hrmacbeth.github.io/math2001/05_Logic

Demonstrates proving first-order logic statements in Lean. These examples involve quantifiers over types and predicates, including implications between quantified statements and changing the order of quantifiers.

```Lean
example {P Q : α → Prop} (h1 : ∀ x, P x → Q x) (h2 : ∀ x, P x) : ∀ x, Q x := by
  sorry

example {P Q : α → Prop} (h : ∀ x, P x ↔ Q x) : (∃ x, P x) ↔ (∃ x, Q x) := by
  sorry

example (P : α → β → Prop) : (∃ x y, P x y) ↔ ∃ y x, P x y := by
  sorry

example (P : α → β → Prop) : (∀ x y, P x y) ↔ ∀ y x, P x y := by
  sorry

example (P : α → Prop) (Q : Prop) : ((∃ x, P x) ∧ Q) ↔ ∃ x, (P x ∧ Q) := by
  sorry
```

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

### Prove P(a,1) = a+1 using Induction in Lean

Source: https://hrmacbeth.github.io/math2001/06_Induction

This Lean code presents an example for proving that P(a,1) equals a+1 for all natural numbers a, using simple induction. The proof is marked with `sorry`, signifying that the actual inductive proof needs to be implemented.

```Lean
example (a : ℕ) : pascal a 1 = a + 1 := by
  sorry
```

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

### Prove Divisibility of n! by d in Lean

Source: https://hrmacbeth.github.io/math2001/06_Induction

Provides a Lean example for proving that any natural number d, where 1 <= d <= n, is a factor of n!. The proof utilizes induction on n and handles different cases for d.

```Lean
example (n : ℕ) : ∀ d, 1 ≤ d → d ≤ n → d ∣ n ! := by
  simple_induction n with k IH
  · -- base case
    intro k hk1 hk
    interval_cases k
  · -- inductive step
    intro d hk1 hk
    obtain hk | hk : d = k + 1 ∨ d < k + 1 := eq_or_lt_of_le hk
    · -- case 1: `d = k + 1`
      sorry
    · -- case 2: `d < k + 1`
      sorry
```

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

### Solve Quadratic Equation in Lean

Source: https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure

Demonstrates solving a quadratic equation in Lean, showing how to use a lemma for 'or' conditions and handle case divisions. It starts with the given equation and derives the solution using Lean's proof language.

```Lean
example {x : ℝ} (hx : x ^ 2 - 3 * x + 2 = 0) : x = 1 ∨ x = 2 := by
  have h1 := 
    calc
    (x - 1) * (x - 2) = x ^ 2 - 3 * x + 2 := by ring
    _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  sorry
```

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

### Prove integer divisibility in Lean

Source: https://hrmacbeth.github.io/math2001/03_Parity_and_Divisibility

Illustrates how to represent and prove divisibility for integers (ℤ) in Lean. This example uses a `sorry` placeholder, indicating that the proof logic needs to be filled in, but sets up the structure for proving that -2 divides 6.

```Lean
example : (-2 : ℤ) ∣ 6 := by
  sorry
```

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

### Prove Inequality (n+1)! <= (n+1)^n in Lean

Source: https://hrmacbeth.github.io/math2001/06_Induction

Provides a Lean example to prove the inequality (n+1)! <= (n+1)^n for all natural numbers n. This is compared to Example 6.2.6.

```Lean
example (n : ℕ) : (n + 1) ! ≤ (n + 1) ^ n := by
  sorry
```

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

### Lean Proof with Calculation Tactics

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

Demonstrates a Lean proof using calculation tactics like `ring` and `rw`. It shows how to fill in `sorry` placeholders with appropriate justifications. Errors in tactics or mathematics will result in red underlines.

```Lean
example {r s : ℝ} (h1 : s = 3) (h2 : r + 2 * s = -1) : r = -7 :=
  calc
    r = r + 2 * s - 2 * s := by sorry
    _ = -1 - 2 * s := by sorry
    _ = -1 - 2 * 3 := by sorry
    _ = -7 := by sorry

```

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

### Prove 5t ≠ 18 for any integer t in Lean

Source: https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure

This Lean example proves that for any integer t, the expression 5t is never equal to 18. The proof is expected to use a lemma similar to those in Example 2.3.2.

```Lean
example {t : ℤ} : 5 * t ≠ 18 := by
  sorry
```

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

### Prove a=b or a=2b for real a, b where a^2+2b^2=3ab in Lean

Source: https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure

This Lean example proves that if real numbers a and b satisfy a^2 + 2b^2 = 3ab, then either a equals b or a equals 2b. The solution likely involves a lemma from a previous example.

```Lean
example {a b : ℝ} (hab : a ^ 2 + 2 * b ^ 2 = 3 * a * b) : a = b ∨ a = 2 * b := by
  sorry
```

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

### Prove Inequality for Sequence 'd' in Lean

Source: https://hrmacbeth.github.io/math2001/06_Induction

Proves by two-step induction from a starting point (n>=4) that for the sequence 'd', dn is greater than or equal to 4^n for all sufficiently large natural numbers n. This proof uses Lean's `two_step_induction_from_starting_point` tactic and demonstrates how to handle base cases and inductive steps for proofs not starting at n=0.

```lean
example : forall_sufficiently_large n : ℕ, d n ≥ 4 ^ n := by
  dsimp
  use 4
  intro n hn
  two_step_induction_from_starting_point n, hn with k hk IH1 IH2
  · calc d 4 = 267 := by rfl
      _ ≥ 4 ^ 4 := by numbers
  · calc d 5 = 1096 := by rfl
      _ ≥ 4 ^ 5 := by numbers
  calc d (k + 2) = 3 * d (k + 1) + 5 * d k := by rw [d]
    _ ≥ 3 * 4 ^ (k + 1) + 5 * 4 ^ k := by rel [IH1, IH2]
    _ = 16 * 4 ^ k + 4 ^ k := by ring
    _ ≥ 16 * 4 ^ k := by extra
    _ = 4 ^ (k + 2) := by ring
```

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

### Lean Proof for Modular Arithmetic Step-by-Step

Source: https://hrmacbeth.github.io/math2001/03_Parity_and_Divisibility

Illustrates solving modular arithmetic problems in Lean using a step-by-step approach with the `calc` command and the `rel` tactic. It shows how to substitute congruences and simplify expressions.

```Lean
example {a b : ℤ} (ha : a ≡ 4 [ZMOD 5]) (hb : b ≡ 3 [ZMOD 5]) :
    a * b + b ^ 3 + 3 ≡ 2 [ZMOD 5] := 
  calc
    a * b + b ^ 3 + 3 ≡ 4 * b + b ^ 3 + 3 [ZMOD 5] := by rel [ha]
    _ ≡ 4 * 3 + 3 ^ 3 + 3 [ZMOD 5] := by rel [hb]
    _ = 2 + 5 * 8 := by numbers
    _ ≡ 2 [ZMOD 5] := by extra
```

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

### Example: Existence of a remainder r such that a ≡ r (mod b) (Lean)

Source: https://hrmacbeth.github.io/math2001/06_Induction

This Lean example demonstrates the existence of an integer 'r' such that 0 ≤ r < b and a ≡ r (mod b), given that b is positive. It utilizes the previously proven theorems about fmod (non-negativity and being less than the divisor) and the fundamental identity fmod(a,b) + b*fdiv(a,b) = a.

```lean
example (a b : ℤ) (h : 0 < b) : ∃ r : ℤ, 0 ≤ r ∧ r < b ∧ a ≡ r [ZMOD b] := by
  use fmod a b
  constructor
  · apply fmod_nonneg_of_pos a h
  constructor
  · apply fmod_lt_of_pos a h
  · use fdiv a b
    have Hab : fmod a b + b * fdiv a b = a := fmod_add_fdiv a b
    addarith [Hab]
```

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

### Prove n! is Strictly Positive in Lean

Source: https://hrmacbeth.github.io/math2001/06_Induction

Provides a Lean example for proving that n! is strictly positive for all natural numbers n.

```Lean
example (n : ℕ) : 0 < n ! := by
  sorry
```

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

### Prove Formula for Sequence c_n in Lean

Source: https://hrmacbeth.github.io/math2001/06_Induction

Provides a Lean example to prove the explicit formula c_n = 2 * 3^n + 5 for the recursively defined sequence c_n.

```Lean
example (n : ℕ) : c n = 2 * 3 ^ n + 5 := by
  sorry
```

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

### Prove p=-1 given p-2q=1 and q=-1

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

This Lean snippet proves a statement about rational numbers. Given `p - 2*q = 1` and `q = -1`, it demonstrates that `p` equals -1. This showcases algebraic manipulation with rational numbers in Lean.

```lean
example {p q : ℚ} (h1 : p - 2 * q = 1) (h2 : q = -1) : p = -1 :=
  sorry

```

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

### Prove 2^n >= n^2 + 4 for Large n (Lean)

Source: https://hrmacbeth.github.io/math2001/06_Induction

A Lean proof setup using `dsimp` to handle the 'sufficiently large' condition for proving 2^n >= n^2 + 4.

```Lean
example : forall_sufficiently_large n : ℕ, 2 ^ n ≥ n ^ 2 + 4 := by
  dsimp
  sorry
```

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

### Prove u=1/4 given 4u+v=3 and v=2

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

This Lean snippet demonstrates proving a result about rational numbers. Given `4*u + v = 3` and `v = 2`, the code shows that `u` equals 1/4. It involves algebraic manipulation within the Lean environment.

```lean
example {u v : ℚ} (h1 : 4 * u + v = 3) (h2 : v = 2) : u = 1 / 4 :=
  sorry

```

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

### Prove 3^n >= 2^n + 100 for Large n (Lean)

Source: https://hrmacbeth.github.io/math2001/06_Induction

A Lean proof setup using `dsimp` to handle the 'sufficiently large' condition for proving 3^n >= 2^n + 100.

```Lean
example : forall_sufficiently_large n : ℕ, (3:ℤ) ^ n ≥ 2 ^ n + 100 := by
  dsimp
  sorry
```

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

### Lean Example: Proving (a+b)^2 = 20

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

This Lean code snippet defines a problem involving rational numbers 'a' and 'b' with given hypotheses about their difference and product. It then states the goal to prove that the square of their sum equals 20. The proof is constructed using a 'calc' block, employing 'ring' for algebraic manipulation and 'rw' to rewrite using the provided hypotheses.

```Lean
example {a b : ℚ} (h1 : a - b = 4) (h2 : a * b = 1) : (a + b) ^ 2 = 20 :=
  calc
    (a + b) ^ 2 = (a - b) ^ 2 + 4 * (a * b) := by ring
    _ = 4 ^ 2 + 4 * 1 := by rw [h1, h2]
    _ = 20 := by ring

```

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

### Lean Proof by Cases with Intermediate 'or' Hypothesis

Source: https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure

Illustrates setting up an intermediate 'or' statement as a hypothesis in Lean using the 'have' keyword and then applying proof by cases with 'obtain'. The example proves n^2 ≠ 2 by considering cases n ≤ 1 and 2 ≤ n.

```Lean
example {n : ℕ} : n ^ 2 ≠ 2 := by
  have hn := le_or_succ_le n 1
  obtain hn | hn := hn
  apply ne_of_lt
  calc
    n ^ 2 ≤ 1 ^ 2 := by rel [hn]
    _ < 2 := by numbers
  sorry

```

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

### Prove Bijective Function (Lean)

Source: https://hrmacbeth.github.io/math2001/08_Functions

This example attempts to prove that a function is bijective over the real numbers in Lean. Currently, it uses a `sorry` placeholder, indicating that the proof is not yet implemented.

```Lean
example : Bijective (fun ((m, n) : ℝ × ℝ) ↦ (m + n, m - n)) := by
  sorry
```

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

### Prove s+t=3 or s+t=5 for rational s, t where s = 3-t in Lean

Source: https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure

This Lean example proves that for rational numbers s and t, if s = 3 - t, then either s + t = 3 or s + t = 5. The proof uses the given relationship between s and t.

```Lean
example {s t : ℚ} (h : s = 3 - t) : s + t = 3 ∨ s + t = 5 := by
  sorry
```

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

### Lean Tactic: intro

Source: https://hrmacbeth.github.io/math2001/Index_of_Tactics

The `intro` tactic introduces universally quantified variables (∀), the antecedent of an implication (→), or assumes the positive version of a negated goal (¬) for proof by contradiction.

```Lean
intro
```

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

### Proof with Intermediate Steps and Calculations - Lean

Source: https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure

An example showcasing a proof structure with multiple intermediate steps defined using 'have' and a final calculational proof. It requires filling in 'sorry' placeholders to complete the proof, encouraging prediction of infoview states.

```Lean
example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 := by
  have h3 : r ≤ 3 + s := by sorry -- justify with one tactic
  have h4 : r ≤ 3 - s := by sorry -- justify with one tactic
  calc
    r = (r + r) / 2 := by sorry -- justify with one tactic
    _ ≤ (3 - s + (3 + s)) / 2 := by sorry -- justify with one tactic
    _ = 3 := by sorry -- justify with one tactic

```

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

### Prove Non-Existence of Integer Satisfying Inequality in Lean

Source: https://hrmacbeth.github.io/math2001/05_Logic

Shows that it is not true that there exists an integer a such that for all integers n, 2a^3 ≥ na + 7. The proof is expected to start with negation-normalizing tactics.

```Lean
example : ¬ ∃ a : ℤ, ∀ n : ℤ, 2 * a ^ 3 ≥ n * a + 7 := by
  sorry
```

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

### Prove x=-1 given y+1=3 and x+2y=3

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

This Lean proof demonstrates solving a system of two linear equations with two rational variables. It uses the given conditions `y + 1 = 3` and `x + 2*y = 3` to prove that `x` equals -1.

```lean
example {x y : ℚ} (h1 : y + 1 = 3) (h2 : x + 2 * y = 3) : x = -1 :=
  sorry

```

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

### Limitations of addarith Tactic in Lean

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

Illustrates a scenario where the `addarith` tactic in Lean is insufficient for proof. This example involves a deduction requiring division (if 3w+1=4, then w=1), which `addarith` cannot verify. Such proofs still require explicit calculation.

```lean
example {w : ℚ} (h1 : 3 * w + 1 = 4) : w = 1 := sorry
```

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

### Lean: Intermediate Fact for 'And' Goal Proof

Source: https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure

This Lean snippet illustrates a common proof strategy where an intermediate fact (e.g., solving for 'b' first) is established before using the `constructor` tactic. This intermediate fact can then be used to simplify the proofs of both parts of the final 'and' goal, making the overall proof more concise.

```Lean
example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 ∧ b = 1 := by
  have hb : b = 1 := by addarith [h2]
  constructor
  · calc
      a = 4 + 5 * b := by addarith [h1]
      _ = 4 + 5 * 1 := by rw [hb]
      _ = 9 := by ring
  · apply hb
```

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

### Prove Existence of Real Number Satisfying Inequality in Lean

Source: https://hrmacbeth.github.io/math2001/04_Proofs_with_Structure_II

Demonstrates proving an existential quantification in Lean. It shows how to introduce a variable and prove a property for it, specifically finding a real number 'b' such that b <= x^2 - 2x for all real numbers 'x'.

```lean
example : ∃ b : ℝ, ∀ x : ℝ, b ≤ x ^ 2 - 2 * x := by
  use -1
  intro x
  calc
    -1 ≤ -1 + (x - 1) ^ 2 := by extra
    _ = x ^ 2 - 2 * x := by ring
```

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

### Prove Fibonacci Sequence F_n <= 2^n using Strong Induction in Lean

Source: https://hrmacbeth.github.io/math2001/06_Induction

Proves the inequality F_n <= 2^n for all natural numbers n using strong induction in Lean. This example illustrates the application of strong induction.

```Lean
theorem F_bound (n : ℕ) : F n ≤ 2 ^ n := by
  match n with
  | 0 =>
      calc F 0 = 1 := by rw [F]
        _ ≤ 2 ^ 0 := by numbers
  | 1 =>
      calc F 1 = 1 := by rw [F]
        _ ≤ 2 ^ 1 := by numbers
  | k + 2  =>
      have IH1 := F_bound k -- first inductive hypothesis
      have IH2 := F_bound (k + 1) -- second inductive hypothesis
      calc F (k + 2) = F (k + 1) + F k := by rw [F]
        _ ≤ 2 ^ (k + 1) + 2 ^ k := by rel [IH1, IH2]
        _ ≤ 2 ^ (k + 1) + 2 ^ k + 2 ^ k := by extra
        _ = 2 ^ (k + 2) := by ring

```

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

### Prove c=-3 given 4c+1=3c-2

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

This Lean exercise proves a simple linear equation for a rational number `c`. Given the equation `4*c + 1 = 3*c - 2`, the proof shows that `c` must be -3. This demonstrates basic algebraic solving within Lean.

```lean
example {c : ℚ} (h1 : 4 * c + 1 = 3 * c - 2) : c = -3 :=
  sorry

```

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

### Lean Proof for Solving Linear Equation

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

This Lean code snippet shows how to prove a simple linear equation in integers. It involves manipulating the equation using a hypothesis to reach the desired result, with a `sorry` placeholder for the proof steps.

```Lean
example {x : ℤ} (h1 : x + 4 = 2) : x = -2 :=
  sorry

```

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

### Define Recursive Sequence y_n and Prove Formula in Lean

Source: https://hrmacbeth.github.io/math2001/06_Induction

Defines a recursive sequence y_n with y0=2 and y(n+1)=(y_n)^2. It includes a Lean example to prove that y_n = 2^(2^n) for all natural numbers n.

```Lean
def y : ℕ → ℕ
  | 0 => 2
  | n + 1 => (y n) ^ 2

example (n : ℕ) : y n = 2 ^ (2 ^ n) := by
  sorry
```

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

### Prove Infinitely Many Primes in Lean

Source: https://hrmacbeth.github.io/math2001/07_Number_Theory

This Lean code proves the theorem that there are infinitely many prime numbers. It uses previously defined lemmas and examples like `factorial_pos`, `exists_prime_factor`, `Nat.not_dvd_of_exists_lt_and_lt`, and `dvd_factorial`.

```lean
example (N : ℕ) : ∃ p ≥ N, Prime p := by
  have hN0 : 0 < N ! := by apply factorial_pos
  have hN2 : 2 ≤ N ! + 1 := by addarith [hN0]
  -- `N! + 1` has a prime factor, `p`
  obtain ⟨p, hp, hpN⟩ : ∃ p : ℕ, Prime p ∧ p ∣ N ! + 1 := exists_prime_factor hN2
  have hp2 : 2 ≤ p
  · obtain ⟨hp', hp''⟩ := hp
    apply hp'
  obtain ⟨k, hk⟩ := hpN
  match k with
  | 0 => -- if `k` is zero, contradiction
    have k_contra :=
    calc 0 < N ! + 1 := by extra
      _ = p * 0 := hk
      _ = 0 := by ring
    numbers at k_contra
  | l + 1 => -- so `k = l + 1` for some `l`
    -- the key fact: `p` is not a factor of `N!`
    have key : ¬ p ∣ (N !)
    · apply Nat.not_dvd_of_exists_lt_and_lt (N !)
      use l
      constructor
      · have := 
        calc p * l + p = p * (l + 1) := by ring
          _ = N ! + 1 := by rw [hk]
          _ < N ! + p := by addarith [hp2]
        addarith [this]
      · calc N ! < N ! + 1 := by extra
          _ = p * (l + 1) := by rw [hk]
    -- so `p` is a prime number greater than or equal to `N`, as we sought
    use p
    constructor
    · obtain h_le | h_gt : p ≤ N ∨ N < p := le_or_lt p N
      · have : p ∣ (N !)
        · apply dvd_factorial
          · extra
          · addarith [h_le]
        contradiction
      · addarith [h_gt]
    · apply hp
```

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

### Lean: Handle 'And' Goal with Constructor Tactic

Source: https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure

This snippet demonstrates using the `constructor` tactic in Lean to address a goal that is an 'and' statement. The `constructor` tactic splits the single goal into two simpler goals, one for each part of the conjunction. This is shown in the context of solving a system of equations.

```Lean
example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 ∧ b = 1 := by
  constructor
  · calc
      a = 4 + 5 * b := by addarith [h1]
      _ = -6 + 5 * (b + 2) := by ring
      _ = -6 + 5 * 3 := by rw [h2]
      _ = 9 := by ring
  · addarith [h2]
```

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

### Lean Proof for Integer Properties

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

A Lean code snippet for proving a property involving integers. It uses a `calc` block with `sorry` placeholders for justifications. This example highlights the sensitivity of Lean to order of operations and requires precise mathematical reasoning.

```Lean
example {a b m n : ℤ} (h1 : a * m + b * n = 1) (h2 : b ^ 2 = 2 * a ^ 2) :
    (2 * a * n + b * m) ^ 2 = 2 :=
  calc
    (2 * a * n + b * m) ^ 2
      = 2 * (a * m + b * n) ^ 2 + (m ^ 2 - 2 * n ^ 2) * (b ^ 2 - 2 * a ^ 2) := by sorry
    _ = 2 * 1 ^ 2 + (m ^ 2 - 2 * n ^ 2) * (2 * a ^ 2 - 2 * a ^ 2) := by sorry
    _ = 2 := by sorry

```

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

### Prove a=2 given a+2b=4 and a-b=1

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

This Lean exercise proves a statement about real numbers. Given `a + 2*b = 4` and `a - b = 1`, it demonstrates that `a` equals 2. This involves solving a system of two linear equations.

```lean
example {a b : ℝ} (h1 : a + 2 * b = 4) (h2 : a - b = 1) : a = 2 :=
  sorry

```

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

### Lean: Prove Empty Set is Subset of Any Set

Source: https://hrmacbeth.github.io/math2001/09_Sets

Demonstrates proving that the empty set is a subset of any set `U` of integers in Lean. It uses `dsimp`, `Set.subset_def`, `intro`, and `exhaust` tactics.

```Lean
example (U : Set ℤ) : ∅ ⊆ U := by
  dsimp [Set.subset_def]
  intro x
  exhaust
```

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

### Define Inverse Function v for u(x)=5x+1 (Lean)

Source: https://hrmacbeth.github.io/math2001/08_Functions

Defines a function 'u' and its noncomputable inverse 'v'. It includes an example asserting that 'v' is the inverse of 'u', demonstrating inverse function definitions in Lean.

```Lean
def u (x : ℝ) : ℝ := 5 * x + 1

noncomputable def v (x : ℝ) : ℝ := sorry

example : Inverse u v := by
  sorry

```

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

### Prove 2x ≠ 3 for any integer x in Lean

Source: https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure

This Lean code proves that for any integer x, 2x can never be equal to 3. This is a basic number theory proof likely using a lemma from Example 2.3.2.

```Lean
example {x : ℤ} : 2 * x ≠ 3 := by
  sorry
```

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

### Prove y=2 given x+3=5 and 2x-yx=0

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

This Lean exercise proves a statement about real numbers `x` and `y`. Given `x + 3 = 5` and `2*x - y*x = 0`, the code shows that `y` equals 2. This involves solving for variables in a system of equations.

```lean
example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 :=
  sorry

```

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

### Prove Inequality with Integers using Lean Calc

Source: https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation

This Lean code demonstrates a proof by calculation for an inequality involving integers. It uses tactics like `ring` for algebraic manipulation, `rel` for substituting inequalities, and `numbers` for numeric facts. The proof constructs a chain of inequalities to show that y > 3, given initial conditions on x and y.

```Lean
example {x y : ℤ} (hx : x + 3 ≤ 2) (hy : y + 2 * x ≥ 3) : y > 3 :=
  calc
    y = y + 2 * x - 2 * x := by ring
    _ ≥ 3 - 2 * x := by rel [hy]
    _ = 9 - 2 * (x + 3) := by ring
    _ ≥ 9 - 2 * 2 := by rel [hx]
    _ > 3 := by numbers

```