-- 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.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''
this : (g.squashGCF (n' + 1)).s.get? m'' = g.s.get? m''
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)

Tactic:
simp [contsAux, succ_m''th_contsAux_eq, m''th_contsAux_eq, this]

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

Tactic:
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)

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''
this : (g.squashGCF (n' + 1)).s.get? m'' = g.s.get? m''
⊢ 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
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)

Tactic:
have m'_lt_n : m'' + 1 < n' + 1 := 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
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)