awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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) = Option.some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = Option.some gp_succ_n
some : ∀ (m : ℕ), (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

Tactic:
ext1 m
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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) = Option.some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = Option.some gp_succ_n
m : ℕ
some : ∀ (m_eq_n : m = n), (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
some₁ : ∀ (m_ne_n : ¬m = n), (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
rcases Decidable.em (m = n) with m_eq_n | m_ne_n

Premises used: Decidable.em, Eq
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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_eq_n : m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
simp [*, squashSeq]

Premises used: GenContFract.squashSeq
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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) = Option.some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = Option.some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
some : ∀ (s_succ_mth_eq : s.get? (m + 1) = none), (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
some₁ :
  ∀ (val : Pair K) (s_succ_mth_eq : s.get? (m + 1) = Option.some val),
    (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
cases s_succ_mth_eq : s.get? (m + 1)

Premises used: HAdd.hAdd, OfNat.ofNat, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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

Tactic:
simp only [*, squashSeq, Stream'.Seq.get?_tail, Stream'.Seq.get?_zipWith,
          Option.map₂_none_right]

Premises used: Stream'.Seq.get?_tail, Stream'.Seq.get?_zipWith, GenContFract.squashSeq, Option.map₂_none_right
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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:
simp [*, squashSeq]

Premises used: GenContFract.squashSeq
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
cases :
  ∀ (x : Option (Pair K)) (s_succ_succ_nth_eq : s.get? (n + 2) = x), (squashSeq s (n + 1)).tail = squashSeq s.tail n
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

Tactic:
cases s_succ_succ_nth_eq : s.get? (n + 2) with
  | none =>
    cases s_succ_nth_eq : s.get? (n + 1) <;>
      simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq]
  | some gp_succ_succ_n =>
    obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.get? (n + 1) = some gp_succ_n :=
      s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq
    -- apply extensionality with `m` and continue by cases `m = n`.
    ext1 m
    rcases Decidable.em (m = n) with m_eq_n | m_ne_n
    · simp [*, squashSeq]
    · cases s_succ_mth_eq : s.get? (m + 1)
      · simp only [*, squashSeq, Stream'.Seq.get?_tail, Stream'.Seq.get?_zipWith,
          Option.map₂_none_right]
      · simp [*, squashSeq]

Premises used: Stream'.Seq.get?_tail, Stream'.Seq.get?_zipWith, GenContFract.squashSeq, Option.some, Option.map₂_none_right, Option.none, HAdd.hAdd, OfNat.ofNat, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
s_succ_nth_eq : s.get? (n + 1) = Option.none
none : convs'Aux s (n + 2) = convs'Aux s (n + 1)
none₁ none₂ : convs'Aux s (n + 1) = convs'Aux s (n + 1)
⊢ convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)

Tactic:
rw [squashSeq_eq_self_of_terminated s_succ_nth_eq,
      convs'Aux_stable_step_of_terminated s_succ_nth_eq]

Premises used: GenContFract.convs'Aux_stable_step_of_terminated, GenContFract.squashSeq_eq_self_of_terminated
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (HAdd.hAdd (α := ℕ) 0 1) = some gp_succ_n
⊢ ∃ (gp_head : Pair K), s.head = some gp_head

Tactic:
s.ge_stable zero_le_one s_succ_nth_eq

Premises used: Stream'.Seq.ge_stable, Stream'.Seq.head, zero_le_one
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (HAdd.hAdd (α := ℕ) 0 1) = Option.some gp_succ_n
some :
  ∀ (gp_head : Pair K) (s_head_eq : s.head = Option.some gp_head),
    convs'Aux s (HAdd.hAdd (α := ℕ) 0 2) = convs'Aux (squashSeq s 0) (HAdd.hAdd (α := ℕ) 0 1)
⊢ convs'Aux s (HAdd.hAdd (α := ℕ) 0 2) = convs'Aux (squashSeq s 0) (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable zero_le_one s_succ_nth_eq

Premises used: Stream'.Seq.ge_stable, Stream'.Seq.head, zero_le_one
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (HAdd.hAdd (α := ℕ) 0 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ (squashSeq s 0).head = some { a := gp_head.a, b := gp_head.b + gp_succ_n.a / gp_succ_n.b }

Tactic:
have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
        squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (HAdd.hAdd (α := ℕ) 0 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : (squashSeq s 0).head = some { a := gp_head.a, b := gp_head.b + gp_succ_n.a / gp_succ_n.b }
⊢ convs'Aux s (HAdd.hAdd (α := ℕ) 0 2) = convs'Aux (squashSeq s 0) (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp_all [convs'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]

Premises used: Stream'.Seq.get?_tail, GenContFract.convs'Aux, Stream'.Seq.head
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (m + 1) = some gp_succ_n),
    convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
⊢ ∃ (gp_head : Pair K), s.head = some gp_head

Tactic:
s.ge_stable (m + 2).zero_le s_succ_nth_eq

Premises used: Nat.zero_le, Stream'.Seq.ge_stable, Stream'.Seq.head, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (m + 1) = Option.some gp_succ_n),
    convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = Option.some gp_succ_n
some :
  ∀ (gp_head : Pair K) (s_head_eq : s.head = Option.some gp_head),
    convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)

Tactic:
obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable (m + 2).zero_le s_succ_nth_eq

Premises used: Nat.zero_le, Stream'.Seq.ge_stable, Stream'.Seq.head, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (m + 1) = some gp_succ_n),
    convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)

Tactic:
simpa only [convs'Aux, s_head_eq]

Premises used: GenContFract.convs'Aux
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (m + 1) = Option.some gp_succ_n),
    convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = Option.some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = Option.some gp_head
some : gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)

Tactic:
suffices
        gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
          convs'Aux (squashSeq s (m + 1)) (m + 2)
        by simpa only [convs'Aux, s_head_eq]
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (m + 1) = some gp_succ_n),
    convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ (squashSeq s (m + 1)).head = some gp_head

Tactic:
have : (squashSeq s (m + 1)).head = some gp_head :=
        (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (m + 1) = some gp_succ_n),
    convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : (squashSeq s (m + 1)).head = some gp_head
⊢ gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)

Tactic:
simp_all [convs'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]

Premises used: GenContFract.convs'Aux, GenContFract.squashSeq_succ_n_tail_eq_squashSeq_tail_n
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = Option.some gp_succ_n
some :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K)
    (s_succ_nth_eq : s.get? (HAdd.hAdd (α := ℕ) 0 1) = Option.some gp_succ_n),
    convs'Aux s (HAdd.hAdd (α := ℕ) 0 2) = convs'Aux (squashSeq s 0) (HAdd.hAdd (α := ℕ) 0 1)
some₁ :
  ∀ (m : ℕ)
    (IH :
      ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (m + 1) = Option.some gp_succ_n),
        convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1))
    {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (m + 1 + 1) = Option.some gp_succ_n),
    convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)
⊢ convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)

Tactic:
induction n generalizing s gp_succ_n with
    | zero =>
      obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable zero_le_one s_succ_nth_eq
      have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
        squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
      simp_all [convs'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
    | succ m IH =>
      obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable (m + 2).zero_le s_succ_nth_eq
      suffices
        gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
          convs'Aux (squashSeq s (m + 1)) (m + 2)
        by simpa only [convs'Aux, s_head_eq]
      have : (squashSeq s (m + 1)).head = some gp_head :=
        (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
      simp_all [convs'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]

Premises used: Stream'.Seq.get?_tail, GenContFract.convs'Aux, Stream'.Seq.head, GenContFract.squashSeq_succ_n_tail_eq_squashSeq_tail_n
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
cases :
  ∀ (x : Option (Pair K)) (s_succ_nth_eq : s.get? (n + 1) = x), convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)
⊢ convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)

Tactic:
cases s_succ_nth_eq : s.get? <| n + 1 with
  | none =>
    rw [squashSeq_eq_self_of_terminated s_succ_nth_eq,
      convs'Aux_stable_step_of_terminated s_succ_nth_eq]
  | some gp_succ_n =>
    induction n generalizing s gp_succ_n with
    | zero =>
      obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable zero_le_one s_succ_nth_eq
      have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
        squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
      simp_all [convs'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
    | succ m IH =>
      obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable (m + 2).zero_le s_succ_nth_eq
      suffices
        gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
          convs'Aux (squashSeq s (m + 1)) (m + 2)
        by simpa only [convs'Aux, s_head_eq]
      have : (squashSeq s (m + 1)).head = some gp_head :=
        (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
      simp_all [convs'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]

Premises used: Stream'.Seq.get?_tail, GenContFract.convs'Aux, Option.some, Stream'.Seq.head, GenContFract.squashSeq_succ_n_tail_eq_squashSeq_tail_n, Option.none, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
terminatedAt_n : g.TerminatedAt 0
⊢ g.s.get? 0 = none

Tactic:
change g.s.get? 0 = none at terminatedAt_n

Premises used: GenContFract.s, Option.none, OfNat.ofNat, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
terminatedAt_n : g.s.get? 0 = none
⊢ g.squashGCF 0 = g

Tactic:
simp only [squashGCF, terminatedAt_n]

Premises used: GenContFract.squashGCF
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
n : ℕ
terminatedAt_n : g.TerminatedAt (n + 1)
succ :
  ∀ (h : K) (s : Stream'.Seq (Pair K)) (terminatedAt_n : { h := h, s := s : GenContFract K }.TerminatedAt (n + 1)),
    { h := h, s := s : GenContFract K }.squashGCF (n + 1) = { h := h, s := s }
⊢ g.squashGCF (n + 1) = g

Tactic:
cases g
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
n : ℕ
h : K
s : Stream'.Seq (Pair K)
terminatedAt_n : { h := h, s := s : GenContFract K }.TerminatedAt (n + 1)
succ : squashSeq s n = s
⊢ { h := h, s := s : GenContFract K }.squashGCF (n + 1) = { h := h, s := s }

Tactic:
simp only [squashGCF, mk.injEq, true_and]

Premises used: GenContFract.mk.injEq, GenContFract.squashGCF, true_and
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
n : ℕ
h : K
s : Stream'.Seq (Pair K)
terminatedAt_n : { h := h, s := s : GenContFract K }.TerminatedAt (n + 1)
⊢ squashSeq s n = s

Tactic:
squashSeq_eq_self_of_terminated terminatedAt_n

Premises used: GenContFract.squashSeq_eq_self_of_terminated
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : DivisionRing K
n : ℕ
h : K
s : Stream'.Seq (Pair K)
terminatedAt_n : { h := h, s := s : GenContFract K }.TerminatedAt (n + 1)
⊢ squashSeq s n = s

Tactic:
exact squashSeq_eq_self_of_terminated terminatedAt_n

Premises used: GenContFract.squashSeq_eq_self_of_terminated
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : DivisionRing K
terminatedAt_n : g.TerminatedAt n
zero : ∀ (terminatedAt_n : g.TerminatedAt 0), g.squashGCF 0 = g
succ : ∀ (n : ℕ) (terminatedAt_n : g.TerminatedAt (n + 1)), g.squashGCF (n + 1) = g
⊢ g.squashGCF n = g

Tactic:
cases n with
  | zero =>
    change g.s.get? 0 = none at terminatedAt_n
    simp only [squashGCF, terminatedAt_n]
  | succ =>
    cases g
    simp only [squashGCF, mk.injEq, true_and]
    exact squashSeq_eq_self_of_terminated terminatedAt_n

Premises used: GenContFract.s, GenContFract.mk.injEq, Option.none, GenContFract.squashGCF, OfNat.ofNat, true_and, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : DivisionRing K
m : ℕ
m_lt_n : m < n
⊢ (g.squashGCF (n + 1)).s.get? m = g.s.get? m

Tactic:
simp only [squashGCF, squashSeq_nth_of_lt m_lt_n]

Premises used: GenContFract.squashSeq_nth_of_lt, GenContFract.squashGCF
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
zero : ∀ (g_s_head_eq : g.s.get? 0 = none), g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0
zero₁ :
  ∀ (val : Pair K) (g_s_head_eq : g.s.get? 0 = some val), g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0
⊢ g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0

Tactic:
cases g_s_head_eq : g.s.get? 0

Premises used: GenContFract.s, OfNat.ofNat, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
g_s_head_eq : g.s.get? 0 = none
⊢ g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0

Tactic:
simp [g_s_head_eq, squashGCF, convs', convs'Aux, Stream'.Seq.head]

Premises used: GenContFract.convs'Aux, GenContFract.convs', Stream'.Seq.head, GenContFract.squashGCF
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
val : Pair K
g_s_head_eq : g.s.get? 0 = some val
⊢ g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0

Tactic:
simp [g_s_head_eq, squashGCF, convs', convs'Aux, Stream'.Seq.head]

Premises used: GenContFract.convs'Aux, GenContFract.convs', Stream'.Seq.head, GenContFract.squashGCF
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
n : ℕ
⊢ g.convs' (n + 1 + 1) = (g.squashGCF (n + 1)).convs' (n + 1)

Tactic:
simp only [succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq, convs',
      squashGCF]

Premises used: GenContFract.convs', GenContFract.succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq, GenContFract.squashGCF
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : DivisionRing K
zero : g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0
succ : ∀ (n : ℕ), g.convs' (n + 1 + 1) = (g.squashGCF (n + 1)).convs' (n + 1)
⊢ g.convs' (n + 1) = (g.squashGCF n).convs' n

Tactic:
cases n with
  | zero =>
    cases g_s_head_eq : g.s.get? 0 <;>
      simp [g_s_head_eq, squashGCF, convs', convs'Aux, Stream'.Seq.head]
  | succ =>
    simp only [succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq, convs',
      squashGCF]

Premises used: GenContFract.s, GenContFract.convs'Aux, GenContFract.convs', Stream'.Seq.head, GenContFract.succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq, GenContFract.squashGCF, OfNat.ofNat, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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
zero :
  ∀ (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
succ :
  ∀ (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)
⊢ g.contsAux m = (g.squashGCF n).contsAux m

Tactic:
rcases m with - | m'
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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
succ :
  ∀ (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)
succ₁ :
  ∀ (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)
⊢ g.contsAux (m' + 1) = (g.squashGCF n).contsAux (m' + 1)

Tactic:
rcases n with - | n'
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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:
(m'.not_succ_le_zero m_le_n).elim

Premises used: False.elim, Nat.not_succ_le_zero
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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

Premises used: False.elim, Nat.not_succ_le_zero
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
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
succ :
  ∀ (IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m)
    (m_le_n : HAdd.hAdd (α := ℕ) 0 1 ≤ n' + 1),
    g.contsAux (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF (n' + 1)).contsAux (HAdd.hAdd (α := ℕ) 0 1)
succ₁ :
  ∀ (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)
⊢ g.contsAux (m' + 1) = (g.squashGCF (n' + 1)).contsAux (m' + 1)

Tactic:
rcases m' with - | m''
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
n' : ℕ
IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : HAdd.hAdd (α := ℕ) 0 1 ≤ n' + 1
⊢ g.contsAux (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF (n' + 1)).contsAux (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
rfl