Theorem: AnalysisI.Ch2.euclidean_algorithm (Lean4Analysis/Ch2.lean)

State before:
n q : ℕ
⊢ Positive q → Euclid n q
Tactic:
intro (_ : Positive q)
State after:
n q : ℕ
x✝ : Positive q
⊢ Euclid n q

State before:
n q : ℕ
x✝ : Positive q
⊢ Euclid n q
Tactic:
have : 0 < q := Natural.lt_zero_pos.mp ‹Positive q›
State after:
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid n q

State before:
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid n q
Tactic:
apply Natural.ind_on (motive := λ n => Euclid n q) n
State after:
case zero
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid 0 q

case step
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ ∀ (m : ℕ), Euclid m q → Euclid (step m) q

State before:
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid 0 q
Tactic:
case zero =>
  show Euclid 0 q
  let m := 0
  let r := 0
  have r_bounded : r < q := ‹0 < q›
  have n_divided : 0 ≃ m * q + r := calc
    0         ≃ _ := Rel.symm Natural.zero_mul
    0 * q     ≃ _ := Rel.symm Natural.add_zero
    0 * q + 0 ≃ _ := Rel.refl
    m * q + r ≃ _ := Rel.refl
  exact Euclid.intro m r r_bounded n_divided
State after:
no goals

State before:
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid 0 q
Tactic:
let m := 0
State after:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
⊢ Euclid 0 q

State before:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
⊢ Euclid 0 q
Tactic:
let r := 0
State after:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
⊢ Euclid 0 q

State before:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
⊢ Euclid 0 q
Tactic:
have r_bounded : r < q := ‹0 < q›
State after:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
r_bounded : r < q
⊢ Euclid 0 q

State before:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
r_bounded : r < q
⊢ Euclid 0 q
Tactic:
have n_divided : 0 ≃ m * q + r := calc
  0         ≃ _ := Rel.symm Natural.zero_mul
  0 * q     ≃ _ := Rel.symm Natural.add_zero
  0 * q + 0 ≃ _ := Rel.refl
  m * q + r ≃ _ := Rel.refl
State after:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
r_bounded : r < q
n_divided : 0 ≃ m * q + r
⊢ Euclid 0 q

State before:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
r_bounded : r < q
n_divided : 0 ≃ m * q + r
⊢ Euclid 0 q
Tactic:
exact Euclid.intro m r r_bounded n_divided
State after:
no goals

State before:
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ ∀ (m : ℕ), Euclid m q → Euclid (step m) q
Tactic:
intro n (ih : Euclid n q)
State after:
n✝ q : ℕ
x✝ : Positive q
this : 0 < q
n : ℕ
ih : Euclid n q
⊢ Euclid (step n) q

State before:
n✝ q : ℕ
x✝ : Positive q
this : 0 < q
n : ℕ
ih : Euclid n q
⊢ Euclid (step n) q
Tactic:
have ⟨m', r', (_ : r' < q), (_ : n ≃ m' * q + r')⟩ := ih
State after:
n✝ q : ℕ
x✝ : Positive q
this : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
⊢ Euclid (step n) q

State before:
n✝ q : ℕ
x✝ : Positive q
this : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
⊢ Euclid (step n) q
Tactic:
have : step r' ≤ q := Natural.lt_step_le.mp ‹r' < q›
State after:
n✝ q : ℕ
x✝ : Positive q
this✝ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this : step r' ≤ q
⊢ Euclid (step n) q

State before:
n✝ q : ℕ
x✝ : Positive q
this✝ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this : step r' ≤ q
⊢ Euclid (step n) q
Tactic:
have : step r' < q ∨ step r' ≃ q := Natural.le_split ‹step r' ≤ q›
State after:
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ Euclid (step n) q

State before:
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ Euclid (step n) q
Tactic:
apply Or.elim ‹step r' < q ∨ step r' ≃ q›
State after:
case left
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ step r' < q → Euclid (step n) q

case right
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ step r' ≃ q → Euclid (step n) q

State before:
case left
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ step r' < q → Euclid (step n) q
Tactic:
intro (_ : step r' < q)
State after:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
⊢ Euclid (step n) q

State before:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
⊢ Euclid (step n) q
Tactic:
let m := m'
State after:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
⊢ Euclid (step n) q

State before:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
⊢ Euclid (step n) q
Tactic:
let r := step r'
State after:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
⊢ Euclid (step n) q

State before:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
⊢ Euclid (step n) q
Tactic:
have : r < q := ‹step r' < q›
State after:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝² : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝¹ : step r' ≤ q
this✝ : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
this : r < q
⊢ Euclid (step n) q

State before:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝² : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝¹ : step r' ≤ q
this✝ : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
this : r < q
⊢ Euclid (step n) q
Tactic:
have : step n ≃ m * q + r := calc
  step n             ≃ _ := AA.subst₁ ‹n ≃ m' * q + r'›
  step (m' * q + r') ≃ _ := Rel.symm Natural.add_step
  m' * q + step r'   ≃ _ := Rel.refl
  m * q + r          ≃ _ := Rel.refl
State after:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝³ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝² : step r' ≤ q
this✝¹ : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
this✝ : r < q
this : step n ≃ m * q + r
⊢ Euclid (step n) q

State before:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝³ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝² : step r' ≤ q
this✝¹ : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
this✝ : r < q
this : step n ≃ m * q + r
⊢ Euclid (step n) q
Tactic:
exact ⟨m, r, ‹r < q›, ‹step n ≃ m * q + r›⟩
State after:
no goals

State before:
case right
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ step r' ≃ q → Euclid (step n) q
Tactic:
intro (_ : step r' ≃ q)
State after:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
⊢ Euclid (step n) q

State before:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
⊢ Euclid (step n) q
Tactic:
let m := step m'
State after:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
⊢ Euclid (step n) q

State before:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
⊢ Euclid (step n) q
Tactic:
let r := 0
State after:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
⊢ Euclid (step n) q

State before:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
⊢ Euclid (step n) q
Tactic:
have : r < q := ‹0 < q›
State after:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝² : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝¹ : step r' ≤ q
this✝ : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
this : r < q
⊢ Euclid (step n) q

State before:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝² : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝¹ : step r' ≤ q
this✝ : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
this : r < q
⊢ Euclid (step n) q
Tactic:
have : step n ≃ m * q + r := calc
  step n             ≃ _ := AA.subst₁ ‹n ≃ m' * q + r'›
  step (m' * q + r') ≃ _ := Rel.symm Natural.add_step
  m' * q + step r'   ≃ _ := AA.substR ‹step r' ≃ q›
  m' * q + q         ≃ _ := Rel.symm Natural.step_mul
  step m' * q        ≃ _ := Rel.symm Natural.add_zero
  step m' * q + 0    ≃ _ := Rel.refl
  m * q + r          ≃ _ := Rel.refl
State after:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝³ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝² : step r' ≤ q
this✝¹ : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
this✝ : r < q
this : step n ≃ m * q + r
⊢ Euclid (step n) q

State before:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝³ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝² : step r' ≤ q
this✝¹ : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
this✝ : r < q
this : step n ≃ m * q + r
⊢ Euclid (step n) q
Tactic:
exact ⟨m, r, ‹r < q›, ‹step n ≃ m * q + r›⟩
State after:
no goals