awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ i < n + 1

Tactic:
rw [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
i : ℕ
hi : i < n + 1
⊢ ∃ (gp : Pair K), (↑s : GenContFract K).s.get? i = some gp

Tactic:
Option.ne_none_iff_exists'.1 <| mt (terminated_stable <| Nat.le_of_succ_le_succ hi) ‹_›

Premises used: Option.ne_none_iff_exists', mt, Nat.le_of_succ_le_succ, Iff.mp, GenContFract.terminated_stable
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
i : ℕ
hi : i < n + 1
obtain :
  ∀ (gp : Pair K) (s_ith_eq : (↑s : GenContFract K).s.get? i = some gp),
    -((↑s : GenContFract K).partNums.get? i).getD 0 = -1
⊢ -((↑s : GenContFract K).partNums.get? i).getD 0 = -1

Tactic:
obtain ⟨gp, s_ith_eq⟩ : ∃ gp, (↑s : GenContFract K).s.get? i = some gp :=
      Option.ne_none_iff_exists'.1 <| mt (terminated_stable <| Nat.le_of_succ_le_succ hi) ‹_›

Premises used: GenContFract.s, Option.ne_none_iff_exists', mt, Nat.le_of_succ_le_succ, Iff.mp, GenContFract.terminated_stable, Subtype.val, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
i : ℕ
hi : i < n + 1
gp : Pair K
s_ith_eq : (↑s : GenContFract K).s.get? i = some gp
rw : -(some gp.a).getD 0 = -1
rw₁ : Eq.{u_1 + 1} (α := K) (-Option.getD (some 1) 0) (-1)
rw₂ rw₃ : Eq.{u_1 + 1} (α := K) (-1) (-1)
⊢ -((↑s : GenContFract K).partNums.get? i).getD 0 = -1

Tactic:
rw [partNum_eq_s_a s_ith_eq, s.property i gp.a <| partNum_eq_s_a s_ith_eq, Option.getD_some]

Premises used: GenContFract.Pair.a, Option.getD_some, GenContFract.partNum_eq_s_a, Subtype.property
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
rw : HPow.hPow (α := K) (-1) (Finset.range (n + 1)).card = HPow.hPow (α := K) (-1) (n + 1)
rw₁ rw₂ : HPow.hPow (α := K) (-1) (n + 1) = HPow.hPow (α := K) (-1) (n + 1)
⊢ ∏ i ∈ Finset.range (n + 1), -1 = HPow.hPow (α := K) (-1) (n + 1)

Tactic:
rw [Finset.prod_const, Finset.card_range]

Premises used: Finset.card_range, Finset.prod_const
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.TerminatedAt m

Tactic:
g.s.terminated_stable n_le_m terminatedAt_n

Premises used: GenContFract.s, Stream'.Seq.terminated_stable, GenContFract.TerminatedAt
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
terminatedAt_n : g.TerminatedAt n
⊢ g.s.get? n = none

Tactic:
rw [terminatedAt_iff_s_none] at terminatedAt_n

Premises used: GenContFract.terminatedAt_iff_s_none
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
terminatedAt_n : g.s.get? n = none
⊢ g.contsAux (n + 2) = g.contsAux (n + 1)

Tactic:
simp only [contsAux, terminatedAt_n]

Premises used: GenContFract.contsAux
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
⊢ g.contsAux m = g.contsAux (n + 1)

Tactic:
Nat.le_induction rfl (fun k hnk hk => ?_) _ n_lt_m

Premises used: Nat.le_induction
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
refine : ∀ (k : ℕ) (hnk : n.succ ≤ k) (hk : g.contsAux k = g.contsAux (n + 1)), g.contsAux (k + 1) = g.contsAux (n + 1)
⊢ g.contsAux m = g.contsAux (n + 1)

Tactic:
refine Nat.le_induction rfl (fun k hnk hk => ?_) _ n_lt_m
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ k
hk : g.contsAux k = g.contsAux (n + 1)
rcases :
  ∀ (k : ℕ) (hnk : n.succ ≤ n + k + 1) (hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)),
    g.contsAux (n + k + 1 + 1) = g.contsAux (n + 1)
⊢ g.contsAux (k + 1) = g.contsAux (n + 1)

Tactic:
rcases Nat.exists_eq_add_of_lt hnk with ⟨k, rfl⟩

Premises used: Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ n + k + 1
hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)
⊢ g.contsAux (n + k + 1 + 1) = g.contsAux (n + 1)

Tactic:
(contsAux_stable_step_of_terminated ?_).trans hk

Premises used: Eq.trans, GenContFract.contsAux_stable_step_of_terminated
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ n + k + 1
hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)
refine : g.TerminatedAt (n + k)
⊢ g.contsAux (n + k + 1 + 1) = g.contsAux (n + 1)

Tactic:
refine (contsAux_stable_step_of_terminated ?_).trans hk

Premises used: Eq.trans, GenContFract.contsAux_stable_step_of_terminated
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ n + k + 1
hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)
⊢ g.TerminatedAt (n + k)

Tactic:
terminated_stable (Nat.le_add_right _ _) terminatedAt_n

Premises used: Nat.le_add_right, GenContFract.terminated_stable
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ n + k + 1
hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)
⊢ g.TerminatedAt (n + k)

Tactic:
exact terminated_stable (Nat.le_add_right _ _) terminatedAt_n

Premises used: Nat.le_add_right, GenContFract.terminated_stable
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
⊢ s.get? n = none

Tactic:
change s.get? n = none at terminatedAt_n

Premises used: Option.none, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? 0 = none
⊢ convs'Aux s (HAdd.hAdd (α := ℕ) 0 1) = convs'Aux s 0

Tactic:
simp only [convs'Aux, terminatedAt_n, Stream'.Seq.head]

Premises used: GenContFract.convs'Aux, Stream'.Seq.head
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n_1 : ℕ
inst : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
s_head_eq : s.head = none
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
simp only [convs'Aux, s_head_eq]

Premises used: GenContFract.convs'Aux
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n_1 : ℕ
inst : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ s.tail.TerminatedAt n

Tactic:
simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]

Premises used: Stream'.Seq.get?_tail, Stream'.Seq.TerminatedAt
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n_1 : ℕ
inst : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ s.tail.TerminatedAt n

Tactic:
have : s.tail.TerminatedAt n := by
        simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n_1 : ℕ
inst : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : s.tail.TerminatedAt n
⊢ convs'Aux s.tail (n + 1) = convs'Aux s.tail n

Tactic:
have := IH this
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n_1 : ℕ
inst : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this_1 : s.tail.TerminatedAt n
this : convs'Aux s.tail (n + 1) = convs'Aux s.tail n
⊢ (match (motive := Option (Pair K) → K) s.tail.head with
    | none => 0
    | some gp => gp.a / (gp.b + convs'Aux s.tail.tail n)) =
    convs'Aux s.tail n

Tactic:
rw [convs'Aux] at this

Premises used: GenContFract.convs'Aux
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n_1 : ℕ
inst : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this_1 : s.tail.TerminatedAt n
this :
  (match (motive := Option (Pair K) → K) s.tail.head with
    | none => 0
    | some gp => gp.a / (gp.b + convs'Aux s.tail.tail n)) =
    convs'Aux s.tail n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
simp [this, convs'Aux, s_head_eq]

Premises used: GenContFract.convs'Aux
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n_1 : ℕ
inst : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
succ : ∀ (x : Option (Pair K)) (s_head_eq : s.head = x), convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
cases s_head_eq : s.head with
    | none => simp only [convs'Aux, s_head_eq]
    | some gp_head =>
      have : s.tail.TerminatedAt n := by
        simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]
      have := IH this
      rw [convs'Aux] at this
      simp [this, convs'Aux, s_head_eq]

Premises used: GenContFract.convs'Aux, Option.some, Stream'.Seq.head, Option.none
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? n = none
zero :
  ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? 0 = none), convs'Aux s (HAdd.hAdd (α := ℕ) 0 1) = convs'Aux s 0
succ :
  ∀ (n : ℕ) (IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n)
    {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? (n + 1) = none), convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
⊢ convs'Aux s (n + 1) = convs'Aux s n

Tactic:
induction n generalizing s with
  | zero => simp only [convs'Aux, terminatedAt_n, Stream'.Seq.head]
  | succ n IH =>
    cases s_head_eq : s.head with
    | none => simp only [convs'Aux, s_head_eq]
    | some gp_head =>
      have : s.tail.TerminatedAt n := by
        simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]
      have := IH this
      rw [convs'Aux] at this
      simp [this, convs'Aux, s_head_eq]

Premises used: GenContFract.convs'Aux, Option.some, Stream'.Seq.head, Option.none
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n m : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s n = convs'Aux s n

Tactic:
rfl
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n m : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
m_1 : ℕ
n_le_m : n.le m_1
IH : convs'Aux s m_1 = convs'Aux s n
⊢ convs'Aux s m_1.succ = convs'Aux s n

Tactic:
(convs'Aux_stable_step_of_terminated (?_)).trans IH

Premises used: GenContFract.convs'Aux_stable_step_of_terminated, Eq.trans
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n m : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
m_1 : ℕ
n_le_m : n.le m_1
IH : convs'Aux s m_1 = convs'Aux s n
step : s.TerminatedAt m_1
⊢ convs'Aux s m_1.succ = convs'Aux s n

Tactic:
refine (convs'Aux_stable_step_of_terminated (?_)).trans IH

Premises used: GenContFract.convs'Aux_stable_step_of_terminated, Eq.trans
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n m : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
m_1 : ℕ
n_le_m : n.le m_1
IH : convs'Aux s m_1 = convs'Aux s n
⊢ s.TerminatedAt m_1

Tactic:
s.terminated_stable n_le_m terminatedAt_n

Premises used: Stream'.Seq.terminated_stable
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n m : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
m_1 : ℕ
n_le_m : n.le m_1
IH : convs'Aux s m_1 = convs'Aux s n
⊢ s.TerminatedAt m_1

Tactic:
exact s.terminated_stable n_le_m terminatedAt_n

Premises used: Stream'.Seq.terminated_stable
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
n m : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
n_le_m : n ≤ m
terminatedAt_n : s.TerminatedAt n
refl : convs'Aux s n = convs'Aux s n
step : ∀ {m : ℕ} (n_le_m : n.le m) (IH : convs'Aux s m = convs'Aux s n), convs'Aux s m.succ = convs'Aux s n
⊢ convs'Aux s m = convs'Aux s n

Tactic:
induction n_le_m with
  | refl => rfl
  | step n_le_m IH =>
    refine (convs'Aux_stable_step_of_terminated (?_)).trans IH
    exact s.terminated_stable n_le_m terminatedAt_n

Premises used: Stream'.Seq.terminated_stable, refl
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.conts m = g.conts n

Tactic:
simp only [nth_cont_eq_succ_nth_contAux,
    contsAux_stable_of_terminated (Nat.pred_le_iff.mp n_le_m) terminatedAt_n]

Premises used: Nat.pred_le_iff, GenContFract.nth_cont_eq_succ_nth_contAux, GenContFract.contsAux_stable_of_terminated, Iff.mp
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.nums m = g.nums n

Tactic:
simp only [num_eq_conts_a, conts_stable_of_terminated n_le_m terminatedAt_n]

Premises used: GenContFract.num_eq_conts_a, GenContFract.conts_stable_of_terminated
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.dens m = g.dens n

Tactic:
simp only [den_eq_conts_b, conts_stable_of_terminated n_le_m terminatedAt_n]

Premises used: GenContFract.conts_stable_of_terminated, GenContFract.den_eq_conts_b
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.convs m = g.convs n

Tactic:
simp only [convs, dens_stable_of_terminated n_le_m terminatedAt_n,
    nums_stable_of_terminated n_le_m terminatedAt_n]

Premises used: GenContFract.nums_stable_of_terminated, GenContFract.convs, GenContFract.dens_stable_of_terminated
-- Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.convs' m = g.convs' n

Tactic:
simp only [convs', convs'Aux_stable_of_terminated n_le_m terminatedAt_n]

Premises used: GenContFract.convs', GenContFract.convs'Aux_stable_of_terminated
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.s.TerminatedAt n

Tactic:
rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.s.get? n = none

Tactic:
rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
none :
  ∀ (s_nth_eq : g.s.get? n = Option.none),
    g.partNums.get? n = Option.none ↔ Eq.{u_1 + 1} (α := Option (Pair α)) Option.none Option.none
some :
  ∀ (val : Pair α) (s_nth_eq : g.s.get? n = Option.some val),
    g.partNums.get? n = Option.none ↔ Option.some val = Option.none
⊢ g.partNums.get? n = Option.none ↔ g.s.get? n = Option.none

Tactic:
cases s_nth_eq : g.s.get? n

Premises used: GenContFract.s, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
s_nth_eq : g.s.get? n = none
⊢ g.partNums.get? n = none ↔ Eq.{u_1 + 1} (α := Option (Pair α)) none none

Tactic:
simp [partNums, s_nth_eq]

Premises used: GenContFract.partNums
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
val : Pair α
s_nth_eq : g.s.get? n = some val
⊢ g.partNums.get? n = none ↔ some val = none

Tactic:
simp [partNums, s_nth_eq]

Premises used: GenContFract.partNums
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
rw : g.s.get? n = none ↔ g.partNums.get? n = none
rw₁ rw₂ : g.s.get? n = none ↔ g.s.get? n = none
⊢ g.TerminatedAt n ↔ g.partNums.get? n = none

Tactic:
rw [terminatedAt_iff_s_none, partNum_none_iff_s_none]

Premises used: GenContFract.partNum_none_iff_s_none, GenContFract.terminatedAt_iff_s_none
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
none :
  ∀ (s_nth_eq : g.s.get? n = Option.none),
    g.partDens.get? n = Option.none ↔ Eq.{u_1 + 1} (α := Option (Pair α)) Option.none Option.none
some :
  ∀ (val : Pair α) (s_nth_eq : g.s.get? n = Option.some val),
    g.partDens.get? n = Option.none ↔ Option.some val = Option.none
⊢ g.partDens.get? n = Option.none ↔ g.s.get? n = Option.none

Tactic:
cases s_nth_eq : g.s.get? n

Premises used: GenContFract.s, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
s_nth_eq : g.s.get? n = none
⊢ g.partDens.get? n = none ↔ Eq.{u_1 + 1} (α := Option (Pair α)) none none

Tactic:
simp [partDens, s_nth_eq]

Premises used: GenContFract.partDens
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
val : Pair α
s_nth_eq : g.s.get? n = some val
⊢ g.partDens.get? n = none ↔ some val = none

Tactic:
simp [partDens, s_nth_eq]

Premises used: GenContFract.partDens
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
rw : g.s.get? n = none ↔ g.partDens.get? n = none
rw₁ rw₂ : g.s.get? n = none ↔ g.s.get? n = none
⊢ g.TerminatedAt n ↔ g.partDens.get? n = none

Tactic:
rw [terminatedAt_iff_s_none, partDen_none_iff_s_none]

Premises used: GenContFract.terminatedAt_iff_s_none, GenContFract.partDen_none_iff_s_none
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
gp : Pair α
s_nth_eq : g.s.get? n = some gp
⊢ g.partNums.get? n = some gp.a

Tactic:
simp [partNums, s_nth_eq]

Premises used: GenContFract.partNums
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
gp : Pair α
s_nth_eq : g.s.get? n = some gp
⊢ g.partDens.get? n = some gp.b

Tactic:
simp [partDens, s_nth_eq]

Premises used: GenContFract.partDens
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
a : α
nth_partNum_eq : g.partNums.get? n = some a
⊢ ∃ (gp : Pair α), g.s.get? n = some gp ∧ gp.a = a

Tactic:
simpa [partNums, Stream'.Seq.map_get?] using nth_partNum_eq

Premises used: GenContFract.partNums, Stream'.Seq.map_get?
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
b : α
nth_partDen_eq : g.partDens.get? n = some b
⊢ ∃ (gp : Pair α), g.s.get? n = some gp ∧ gp.b = b

Tactic:
simpa [partDens, Stream'.Seq.map_get?] using nth_partDen_eq

Premises used: Stream'.Seq.map_get?, GenContFract.partDens
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
⊢ g.conts n = g.contsAux (n + 1)

Tactic:
rfl

Premises used: GenContFract.conts, Stream'.get, Stream'.tail, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
⊢ g.nums n = (g.conts n).a

Tactic:
rfl

Premises used: GenContFract.nums, Stream'.get, Stream'.map, Stream'.tail, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
⊢ g.dens n = (g.conts n).b

Tactic:
rfl

Premises used: GenContFract.dens, Stream'.get, Stream'.map, Stream'.tail, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
⊢ g.convs n = g.nums n / g.dens n

Tactic:
rfl

Premises used: GenContFract.convs, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
⊢ g.convs n = (g.conts n).a / (g.conts n).b

Tactic:
rfl

Premises used: GenContFract.convs, GenContFract.dens, GenContFract.nums, Stream'.get, Stream'.map, Stream'.tail, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
A : K
nth_num_eq : g.nums n = A
⊢ ∃ (conts : Pair K), g.conts n = conts ∧ conts.a = A

Tactic:
simpa
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
B : K
nth_denom_eq : g.dens n = B
⊢ ∃ (conts : Pair K), g.conts n = conts ∧ conts.b = B

Tactic:
simpa
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
⊢ g.contsAux 0 = { a := 1, b := 0 }

Tactic:
rfl

Premises used: GenContFract.contsAux, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
⊢ g.contsAux 1 = { a := g.h, b := 1 }

Tactic:
rfl

Premises used: GenContFract.contsAux, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
⊢ g.conts 0 = { a := g.h, b := 1 }

Tactic:
rfl

Premises used: GenContFract.contsAux, GenContFract.conts, Stream'.get, Stream'.tail, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
⊢ g.nums 0 = g.h

Tactic:
rfl

Premises used: GenContFract.nums, Stream'.map, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
⊢ g.dens 0 = 1

Tactic:
rfl

Premises used: GenContFract.dens, Stream'.map, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
⊢ g.convs 0 = g.h

Tactic:
simp [conv_eq_num_div_den, num_eq_conts_a, den_eq_conts_b, div_one]

Premises used: GenContFract.num_eq_conts_a, GenContFract.den_eq_conts_b, GenContFract.conv_eq_num_div_den, div_one