-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem convs_eq_convs' [LinearOrderedField K]
    (s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) :
    g.convs n = g.convs' n

Proof state:
K : Type u_1
inst✝ : LinearOrderedField K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
this : g.convs (n + 1) = g'.convs n
gp' : Pair K
m : ℕ
m_lt_n : m < n
s_mth_eq' : g'.s.get? m = some gp'
⊢ 0 < gp'.a ∧ 0 < gp'.b

Tactic:
rcases m_lt_n with n | succ_m_lt_n

Result:
case refl
K : Type u_1
inst✝ : LinearOrderedField K
g : GenContFract K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      g.convs m.succ = g.convs' m.succ
s_pos : ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ + 1 → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF m.succ
not_terminatedAt_n : ¬g.TerminatedAt m.succ
this : g.convs (m.succ + 1) = g'.convs m.succ
s_mth_eq' : g'.s.get? m = some gp'
⊢ 0 < gp'.a ∧ 0 < gp'.b

case step
K : Type u_1
inst✝ : LinearOrderedField K
g : GenContFract K
gp' : Pair K
m m✝ : ℕ
succ_m_lt_n : m.succ.le m✝
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < m✝.succ → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      g.convs m✝.succ = g.convs' m✝.succ
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < m✝.succ + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF m✝.succ
not_terminatedAt_n : ¬g.TerminatedAt m✝.succ
this : g.convs (m✝.succ + 1) = g'.convs m✝.succ
s_mth_eq' : g'.s.get? m = some gp'
⊢ 0 < gp'.a ∧ 0 < gp'.b

Proof state:
case refl
K : Type u_1
inst✝ : LinearOrderedField K
g : GenContFract K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      g.convs m.succ = g.convs' m.succ
s_pos : ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ + 1 → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF m.succ
not_terminatedAt_n : ¬g.TerminatedAt m.succ
this : g.convs (m.succ + 1) = g'.convs m.succ
s_mth_eq' : g'.s.get? m = some gp'
⊢ 0 < gp'.a ∧ 0 < gp'.b

Tactic:
obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m :=
  Option.ne_none_iff_exists'.mp not_terminatedAt_n

Result:
case refl.intro
K : Type u_1
inst✝ : LinearOrderedField K
g : GenContFract K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      g.convs m.succ = g.convs' m.succ
s_pos : ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ + 1 → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF m.succ
not_terminatedAt_n : ¬g.TerminatedAt m.succ
this : g.convs (m.succ + 1) = g'.convs m.succ
s_mth_eq' : g'.s.get? m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : g.s.get? (m + 1) = some gp_succ_m
⊢ 0 < gp'.a ∧ 0 < gp'.b

Proof state:
K : Type u_1
inst✝ : LinearOrderedField K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
this : g.convs (n + 1) = g'.convs n
⊢ g.convs (n + 1) = g'.convs' n

Tactic:
rwa [← IH]

Result:
K : Type u_1
inst✝ : LinearOrderedField K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
this : g.convs (n + 1) = g'.convs n
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → g'.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b

Proof state:
case succ
K : Type u_1
inst✝ : LinearOrderedField K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
⊢ g.convs (n + 1) = g.convs' (n + 1)

Tactic:
suffices g.convs (n + 1) = g'.convs' n by
  rwa [succ_nth_conv'_eq_squashGCF_nth_conv']

Result:
case succ
K : Type u_1
inst✝ : LinearOrderedField K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
⊢ g.convs (n + 1) = g'.convs' n

Proof state:
case succ.inr
K : Type u_1
inst✝ : LinearOrderedField K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
this : ∀ ⦃b : K⦄, g.partDens.get? n = some b → b ≠ 0
⊢ g.convs (n + 1) = g'.convs n

Tactic:
exact succ_nth_conv_eq_squashGCF_nth_conv @this

Result:
no goals

Proof state:
case refl.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
g : GenContFract K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      g.convs m.succ = g.convs' m.succ
s_pos : ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ + 1 → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF m.succ
not_terminatedAt_n : ¬g.TerminatedAt m.succ
this✝ : g.convs (m.succ + 1) = g'.convs m.succ
s_mth_eq' : g'.s.get? m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : g.s.get? (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : g.s.get? m = some gp_m
m_lt_n : m < m.succ
this : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b
⊢ 0 < gp_succ_m.a / gp_succ_m.b

Tactic:
exact div_pos this.left this.right

Result:
no goals