-- 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
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
this✝ : 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
ot : g'.s.get? m = some { a := gp_m.a, b := gp_m.b + gp_succ_m.a / gp_succ_m.b }
this : gp' = { a := gp_m.a, b := gp_m.b + gp_succ_m.a / gp_succ_m.b }
⊢ 0 < gp'.a ∧ 0 < gp'.b

Tactic:
rwa [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
⊢ 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b

Tactic:
refine ⟨(s_pos (Nat.lt.step m_lt_n) mth_s_eq).left, ?_⟩

Result:
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
⊢ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b

Proof state:
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
this : 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
ot : g'.s.get? m = some { a := gp_m.a, b := gp_m.b + gp_succ_m.a / gp_succ_m.b }
⊢ gp' = { a := gp_m.a, b := gp_m.b + gp_succ_m.a / gp_succ_m.b }

Tactic:
simp_all only [Option.some.injEq]

Result:
no goals

Proof state:
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

Tactic:
refine s_pos (Nat.lt.step <| Nat.lt.step succ_m_lt_n) ?_

Result:
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'
⊢ g.s.get? m = some gp'

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
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
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:
exact s_pos (Nat.lt.step m_lt_n) s_mth_eq

Result:
no goals

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

Tactic:
simp

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
⊢ 0 < gp_succ_m.a / gp_succ_m.b

Tactic:
have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq

Result:
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