-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem contsAux_eq_contsAux_squashGCF_of_le {m : ℕ} :
    m ≤ n → contsAux g m = (squashGCF g n).contsAux m :=
  Nat.strong_induction_on m
    (by
      clear m
      intro m IH m_le_n
      rcases m with - | m'
      · rfl
      · rcases n with - | n'
        · exact (m'.not_succ_le_zero m_le_n).elim
        -- 1 ≰ 0
        · rcases m' with - | m''
          · rfl
          · -- get some inequalities to instantiate the IH for m'' and m'' + 1
            have m'_lt_n : m'' + 1 < n' + 1 := m_le_n
            have succ_m''th_contsAux_eq := IH (m'' + 1) (lt_add_one (m'' + 1)) m'_lt_n.le
            have : m'' < m'' + 2 := lt_add_of_pos_right m'' zero_lt_two
            have m''th_contsAux_eq := IH m'' this (le_trans this.le m_le_n)
            have : (squashGCF g (n' + 1)).s.get? m'' = g.s.get? m'' :=
              squashGCF_nth_of_lt (Nat.succ_lt_succ_iff.mp m'_lt_n)
            simp [contsAux, succ_m''th_contsAux_eq, m''th_contsAux_eq, this])

Proof state:
case succ.succ.zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' : ℕ
IH : ∀ m < 0 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : 0 + 1 ≤ n' + 1
⊢ g.contsAux (0 + 1) = (g.squashGCF (n' + 1)).contsAux (0 + 1)

Tactic:
rfl

Result:
no goals

Proof state:
case zero
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
IH : ∀ m < 0, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
m_le_n : 0 ≤ n
⊢ g.contsAux 0 = (g.squashGCF n).contsAux 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_contsAux_eq : g.contsAux (m'' + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1)
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)

Tactic:
have : m'' < m'' + 2 := lt_add_of_pos_right m'' zero_lt_two

Result:
case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_contsAux_eq : g.contsAux (m'' + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1)
this : m'' < m'' + 2
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)

Proof state:
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m : ℕ
⊢ ∀ (n_1 : ℕ),
    (∀ m < n_1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m) →
      n_1 ≤ n → g.contsAux n_1 = (g.squashGCF n).contsAux n_1

Tactic:
clear m

Result:
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
⊢ ∀ (n_1 : ℕ),
    (∀ m < n_1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m) →
      n_1 ≤ n → g.contsAux n_1 = (g.squashGCF n).contsAux n_1

Proof state:
case succ
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ m < m' + 1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
m_le_n : m' + 1 ≤ n
⊢ g.contsAux (m' + 1) = (g.squashGCF n).contsAux (m' + 1)

Tactic:
rcases n with - | n'

Result:
case succ.zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ m < m' + 1, m ≤ 0 → g.contsAux m = (g.squashGCF 0).contsAux m
m_le_n : m' + 1 ≤ 0
⊢ g.contsAux (m' + 1) = (g.squashGCF 0).contsAux (m' + 1)

case succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
m' n' : ℕ
IH : ∀ m < m' + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m' + 1 ≤ n' + 1
⊢ g.contsAux (m' + 1) = (g.squashGCF (n' + 1)).contsAux (m' + 1)

Proof state:
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m : ℕ
IH : ∀ m_1 < m, m_1 ≤ n → g.contsAux m_1 = (g.squashGCF n).contsAux m_1
m_le_n : m ≤ n
⊢ g.contsAux m = (g.squashGCF n).contsAux m

Tactic:
rcases m with - | m'

Result:
case zero
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
IH : ∀ m < 0, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
m_le_n : 0 ≤ n
⊢ g.contsAux 0 = (g.squashGCF n).contsAux 0

case succ
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ m < m' + 1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
m_le_n : m' + 1 ≤ n
⊢ g.contsAux (m' + 1) = (g.squashGCF n).contsAux (m' + 1)

Proof state:
case succ.zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ m < m' + 1, m ≤ 0 → g.contsAux m = (g.squashGCF 0).contsAux m
m_le_n : m' + 1 ≤ 0
⊢ g.contsAux (m' + 1) = (g.squashGCF 0).contsAux (m' + 1)

Tactic:
exact (m'.not_succ_le_zero m_le_n).elim

Result:
no goals

Proof state:
case succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
m' n' : ℕ
IH : ∀ m < m' + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m' + 1 ≤ n' + 1
⊢ g.contsAux (m' + 1) = (g.squashGCF (n' + 1)).contsAux (m' + 1)

Tactic:
rcases m' with - | m''

Result:
case succ.succ.zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' : ℕ
IH : ∀ m < 0 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : 0 + 1 ≤ n' + 1
⊢ g.contsAux (0 + 1) = (g.squashGCF (n' + 1)).contsAux (0 + 1)

case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)

Proof state:
case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
m'_lt_n : m'' + 1 < n' + 1
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)

Tactic:
have succ_m''th_contsAux_eq := IH (m'' + 1) (lt_add_one (m'' + 1)) m'_lt_n.le

Result:
case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_contsAux_eq : g.contsAux (m'' + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1)
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)

Proof state:
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
⊢ ∀ (n_1 : ℕ),
    (∀ m < n_1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m) →
      n_1 ≤ n → g.contsAux n_1 = (g.squashGCF n).contsAux n_1

Tactic:
intro m IH m_le_n

Result:
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m : ℕ
IH : ∀ m_1 < m, m_1 ≤ n → g.contsAux m_1 = (g.squashGCF n).contsAux m_1
m_le_n : m ≤ n
⊢ g.contsAux m = (g.squashGCF n).contsAux m

Proof state:
case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_contsAux_eq : g.contsAux (m'' + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1)
this : m'' < m'' + 2
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)

Tactic:
have m''th_contsAux_eq := IH m'' this (le_trans this.le m_le_n)

Result:
case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_contsAux_eq : g.contsAux (m'' + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1)
this : m'' < m'' + 2
m''th_contsAux_eq : g.contsAux m'' = (g.squashGCF (n' + 1)).contsAux m''
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)