mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some.inr
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
·

Goal state after:
case some.inr
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some.inr.none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
s_succ_mth_eq : s.get? (m + 1) = none
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

pp: case some.inr.some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
val✝ : Pair K
s_succ_mth_eq : s.get? (m + 1) = some val✝
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
·

Goal state after:
case some.inr.none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
s_succ_mth_eq : s.get? (m + 1) = none
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some.inr.some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
val✝ : Pair K
s_succ_mth_eq : s.get? (m + 1) = some val✝
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
·

Goal state after:
case some.inr.some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
val✝ : Pair K
s_succ_mth_eq : s.get? (m + 1) = some val✝
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.some.inl
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_zero : fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

pp: case succ.some.inr
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
·

Goal state after:
case succ.some.inl
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_zero : fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: case inl
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
⊢ |v - (of v).convs n| < ε

pp: case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ |v - (of v).convs n| < ε

Tactic:
·

Goal state after:
case inl
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
⊢ |v - (of v).convs n| < ε
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.some.inr
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
·

Goal state after:
case succ.some.inr
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: 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

pp: 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:
·

Goal state after:
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
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: 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:
·

Goal state after:
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)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: 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)

pp: 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:
·

Goal state after:
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)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: 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:
·

Goal state after:
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)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: 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)

pp: 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:
·

Goal state after:
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)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: 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:
·

Goal state after:
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)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case inl
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
terminatedAt_n : g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

pp: case inr
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

Tactic:
·

Goal state after:
case inl
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
terminatedAt_n : g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case inr
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

Tactic:
·

Goal state after:
case inr
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ |v - (of v).convs n| < ε

Tactic:
·

Goal state after:
case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ |v - (of v).convs n| < ε
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case none
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
stream_nth_eq : IntFractPair.stream q n = none
⊢ ∃ n, IntFractPair.stream q n = none

pp: case some
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
⊢ ∃ n, IntFractPair.stream q n = none

Tactic:
·

Goal state after:
case none
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
stream_nth_eq : IntFractPair.stream q n = none
⊢ ∃ n, IntFractPair.stream q n = none
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case some
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
⊢ ∃ n, IntFractPair.stream q n = none

Tactic:
·

Goal state after:
case some
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
⊢ ∃ n, IntFractPair.stream q n = none
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing 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.convs (n + 1) = g'.convs' n

pp: case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing 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
⊢ g.convs (n + 1) = g'.convs' n

Tactic:
·

Goal state after:
case succ.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing 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.convs (n + 1) = g'.convs' n
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing 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
⊢ g.convs (n + 1) = g'.convs' n

Tactic:
·

Goal state after:
case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing 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
⊢ g.convs (n + 1) = g'.convs' n
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case refl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing 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

pp: case step
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing 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:
·

Goal state after:
case refl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing 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
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case zero
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
IH : ∀ m < 0, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : 0 ≤ 1 ∨ ¬(of v).TerminatedAt (0 - 2)
⊢ ↑(fib 0) ≤ ((of v).contsAux 0).b

pp: case succ.zero
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
IH : ∀ m < 0 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : 0 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (0 + 1 - 2)
⊢ ↑(fib (0 + 1)) ≤ ((of v).contsAux (0 + 1)).b

pp: case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
·

Goal state after:
case zero
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
IH : ∀ m < 0, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : 0 ≤ 1 ∨ ¬(of v).TerminatedAt (0 - 2)
⊢ ↑(fib 0) ≤ ((of v).contsAux 0).b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ.zero
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
IH : ∀ m < 0 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : 0 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (0 + 1 - 2)
⊢ ↑(fib (0 + 1)) ≤ ((of v).contsAux (0 + 1)).b

pp: case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
·

Goal state after:
case succ.zero
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
IH : ∀ m < 0 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : 0 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (0 + 1 - 2)
⊢ ↑(fib (0 + 1)) ≤ ((of v).contsAux (0 + 1)).b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
·

Goal state after:
case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case step
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing 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:
·

Goal state after:
case step
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing 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
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ.inl
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
terminated : g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

pp: case succ.inr
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
not_terminated : ¬g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
·

Goal state after:
case succ.inl
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
terminated : g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b