awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
fst : IntFractPair K
snd : Stream'.Seq (IntFractPair K)
aux_seq_eq : IntFractPair.seq1 v = (fst, snd)
⊢ (of v).h = (↑(fst, snd).1.b : K)

Tactic:
simp [of, aux_seq_eq]

Premises used: GenContFract.of
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
⊢ (of v).h = (↑⌊v⌋ : K)

Tactic:
simp [of_h_eq_intFractPair_seq1_fst_b, IntFractPair.of]

Premises used: GenContFract.IntFractPair.of, GenContFract.of_h_eq_intFractPair_seq1_fst_b
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
⊢ (IntFractPair.seq1 v).2.get? n = IntFractPair.stream v (n + 1)

Tactic:
rfl

Premises used: GenContFract.IntFractPair.stream, Stream'.get, Stream'.tail, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
⊢ (of v).TerminatedAt n ↔ (IntFractPair.seq1 v).2.TerminatedAt n

Tactic:
Option.map_eq_none_iff

Premises used: Stream'.Seq.TerminatedAt, GenContFract.IntFractPair.stream, Stream'.get, Stream'.map, Option.map_eq_none_iff, Stream'.tail, GenContFract.TerminatedAt, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
rw : (IntFractPair.seq1 v).2.TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none
rw₁ : (IntFractPair.seq1 v).2.get? n = none ↔ IntFractPair.stream v (n + 1) = none
rw₂ rw₃ : IntFractPair.stream v (n + 1) = none ↔ IntFractPair.stream v (n + 1) = none
⊢ (of v).TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none

Tactic:
rw [of_terminatedAt_iff_intFractPair_seq1_terminatedAt, Stream'.Seq.TerminatedAt,
    IntFractPair.get?_seq1_eq_succ_get?_stream]

Premises used: Stream'.Seq.TerminatedAt, GenContFract.IntFractPair.get?_seq1_eq_succ_get?_stream, GenContFract.of_terminatedAt_iff_intFractPair_seq1_terminatedAt
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq :
  Stream'.Seq.get?
      (s
        (match (motive := Stream'.Seq1 (IntFractPair K) → GenContFract K)
          (IntFractPair.of v,
            Stream'.Seq.tail
              (Subtype.mk (p := fun (f : Stream' (Option (IntFractPair K))) ↦ f.IsSeq) (IntFractPair.stream v) ⋯)) with
        | (h, s) =>
          { h := (↑h.b : K), s := Stream'.Seq.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }) s }))
      n =
    some gp_n
⊢ ∃ (ifp : IntFractPair K), IntFractPair.stream v (n + 1) = some ifp ∧ { a := 1, b := (↑ifp.b : K) } = gp_n

Tactic:
simpa [Stream'.Seq.get?_tail, Stream'.Seq.map_get?] using s_nth_eq

Premises used: Stream'.Seq.get?_tail, Stream'.Seq.map_get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq : (of v).s.get? n = some gp_n
obtain :
  ∀ (ifp : IntFractPair K) (stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp)
    (gp_n_eq : { a := 1, b := (↑ifp.b : K) } = gp_n),
    ∃ (ifp : IntFractPair K), IntFractPair.stream v (n + 1) = some ifp ∧ (↑ifp.b : K) = gp_n.b
⊢ ∃ (ifp : IntFractPair K), IntFractPair.stream v (n + 1) = some ifp ∧ (↑ifp.b : K) = gp_n.b

Tactic:
obtain ⟨ifp, stream_succ_nth_eq, gp_n_eq⟩ :
    ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ Pair.mk 1 (ifp.b : K) = gp_n := by
    unfold of IntFractPair.seq1 at s_nth_eq
    simpa [Stream'.Seq.get?_tail, Stream'.Seq.map_get?] using s_nth_eq

Premises used: GenContFract.IntFractPair.stream, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq : (of v).s.get? n = some gp_n
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
gp_n_eq : { a := 1, b := (↑ifp.b : K) } = gp_n
refl :
  ∀ (s_nth_eq : (of v).s.get? n = some { a := 1, b := (↑ifp.b : K) }),
    ∃ (ifp_1 : IntFractPair K),
      IntFractPair.stream v (n + 1) = some ifp_1 ∧
        Eq.{u_1 + 1} (α := K) (↑ifp_1.b : K) (Pair.b { a := 1, b := (↑ifp.b : K) })
⊢ ∃ (ifp : IntFractPair K), IntFractPair.stream v (n + 1) = some ifp ∧ (↑ifp.b : K) = gp_n.b

Tactic:
cases gp_n_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
s_nth_eq : (of v).s.get? n = some { a := 1, b := (↑ifp.b : K) }
⊢ ∃ (ifp_1 : IntFractPair K),
    IntFractPair.stream v (n + 1) = some ifp_1 ∧
      Eq.{u_1 + 1} (α := K) (↑ifp_1.b : K) (Pair.b { a := 1, b := (↑ifp.b : K) })

Tactic:
simp_all only [Option.some.injEq, exists_eq_left']

Premises used: Option.some.injEq, exists_eq_left'
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ Eq.{u_1 + 1} (α := Option (Pair K))
    (Stream'.Seq.get?
      (s
        (match (motive := Stream'.Seq1 (IntFractPair K) → GenContFract K)
          (IntFractPair.of v,
            Stream'.Seq.tail
              (Subtype.mk (p := fun (f : Stream' (Option (IntFractPair K))) ↦ f.IsSeq) (IntFractPair.stream v) ⋯)) with
        | (h, s) =>
          { h := (↑h.b : K), s := Stream'.Seq.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }) s }))
      n)
    (some { a := 1, b := (↑ifp_succ_n.b : K) })

Tactic:
simp [Stream'.Seq.map_tail, Stream'.Seq.get?_tail, Stream'.Seq.map_get?, stream_succ_nth_eq]

Premises used: Stream'.Seq.get?_tail, Stream'.Seq.map_tail, Stream'.Seq.map_get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
nth_fr_ne_zero : ifp_n.fr ≠ 0
⊢ (of v).s.get? n = some { a := 1, b := (↑(IntFractPair.of ifp_n.fr⁻¹).b : K) }

Tactic:
get?_of_eq_some_of_succ_get?_intFractPair_stream <|
    IntFractPair.stream_succ_of_some stream_nth_eq nth_fr_ne_zero

Premises used: GenContFract.get?_of_eq_some_of_succ_get?_intFractPair_stream, GenContFract.IntFractPair.stream_succ_of_some
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
simp :
  Eq (α := Option (Pair K))
    (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }) ((IntFractPair.stream v).tail.get 0))
    ((IntFractPair.stream v 1).bind (some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }))
⊢ Eq (α := Option (Pair K))
    (Stream'.Seq.get?
      (s
        (match (motive := Stream'.Seq1 (IntFractPair K) → GenContFract K)
          (IntFractPair.of v,
            Stream'.Seq.tail
              (Subtype.mk (p := fun (f : Stream' (Option (IntFractPair K))) ↦ f.IsSeq) (IntFractPair.stream v) ⋯)) with
        | (h, s) =>
          { h := (↑h.b : K), s := Stream'.Seq.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }) s }))
      0)
    ((IntFractPair.stream v 1).bind (some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }))

Tactic:
simp only [Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.get?, Stream'.map]

Premises used: Stream'.Seq.map, Stream'.Seq.tail, Stream'.map, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
rw :
  Eq (α := Option (Pair K))
    (match (motive := Option (IntFractPair K) → Option (Pair K)) IntFractPair.stream v (Nat.succ 0) with
      | some x => some { a := 1, b := (↑x.b : K) }
      | none => none :
      Option (Pair K))
    ((IntFractPair.stream v 1).bind (some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }) : Option (Pair K))
⊢ Eq (α := Option (Pair K))
    (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }) ((IntFractPair.stream v).tail.get 0))
    ((IntFractPair.stream v 1).bind (some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }))

Tactic:
rw [← Stream'.get_succ, Stream'.get, Option.map.eq_def]

Premises used: Stream'.get_succ, Option.map.eq_def, Stream'.get
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h_1 :
  ∀ (opt : Option (IntFractPair K)) (x : IntFractPair K),
    IntFractPair.stream v (Nat.succ 0) = some x →
      Eq (α := Option (Pair K)) (some { a := 1, b := (↑x.b : K) })
        ((IntFractPair.stream v 1).bind (some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }))
h_2 :
  ∀ (opt : Option (IntFractPair K)),
    IntFractPair.stream v (Nat.succ 0) = none →
      Eq (α := Option (Pair K)) none
        ((IntFractPair.stream v 1).bind (some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }))
⊢ Eq (α := Option (Pair K))
    (match (motive := Option (IntFractPair K) → Option (Pair K)) IntFractPair.stream v (Nat.succ 0) with
      | some x => some { a := 1, b := (↑x.b : K) }
      | none => none :
      Option (Pair K))
    ((IntFractPair.stream v 1).bind (some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }) : Option (Pair K))

Tactic:
split
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
opt : Option (IntFractPair K)
x : IntFractPair K
heq : IntFractPair.stream v (Nat.succ 0) = some x
⊢ Eq (α := Option (Pair K)) (some { a := 1, b := (↑x.b : K) })
    ((IntFractPair.stream v 1).bind (some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }))

Tactic:
simp_all only [Option.bind_some, Option.bind_none, Function.comp_apply]

Premises used: Option.bind_some, Option.bind_none, Function.comp_apply
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
opt : Option (IntFractPair K)
heq : IntFractPair.stream v (Nat.succ 0) = none
⊢ Eq (α := Option (Pair K)) none
    ((IntFractPair.stream v 1).bind (some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }))

Tactic:
simp_all only [Option.bind_some, Option.bind_none, Function.comp_apply]

Premises used: Option.bind_some, Option.bind_none, Function.comp_apply
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : fract v ≠ 0
rw :
  Eq (α := Option (Pair K))
    ((some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }) (IntFractPair.of (IntFractPair.of v).fr⁻¹))
    (some { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) })
⊢ (of v).s.get? 0 = some { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) }

Tactic:
rw [of_s_head_aux, stream_succ_of_some (stream_zero v) h, Option.bind]

Premises used: Option.bind, GenContFract.of_s_head_aux, GenContFract.IntFractPair.stream_zero, GenContFract.IntFractPair.stream_succ_of_some
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : fract v ≠ 0
⊢ Eq (α := Option (Pair K))
    ((some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }) (IntFractPair.of (IntFractPair.of v).fr⁻¹))
    (some { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) })

Tactic:
rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
inst_3 : IsStrictOrderedRing K
a : ℤ
zero :
  Eq.{u_1 + 1} (α := Option (Pair K))
    (Option.bind (α := IntFractPair K) (IntFractPair.stream (↑a : K) 1)
      (some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }))
    none
zero₁ :
  Eq.{u_1 + 1} (α := Option (Pair K))
    (Option.bind (α := IntFractPair K) none (some ∘ fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) })) none
zero₂ zero₃ : Eq.{u_1 + 1} (α := Option (Pair K)) none none
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) 0) none

Tactic:
rw [of_s_head_aux, stream_succ_of_int, Option.bind]

Premises used: Option.bind, GenContFract.IntFractPair.stream_succ_of_int, GenContFract.of_s_head_aux
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
inst_3 : IsStrictOrderedRing K
a : ℤ
n : ℕ
ih : Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) n) none
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) (n + 1)) none

Tactic:
(of (a : K)).s.prop ih

Premises used: GenContFract.s, Int.cast, GenContFract.of, Subtype.prop, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
inst_3 : IsStrictOrderedRing K
a : ℤ
n : ℕ
ih : Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) n) none
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) (n + 1)) none

Tactic:
exact (of (a : K)).s.prop ih

Premises used: GenContFract.s, Int.cast, GenContFract.of, Subtype.prop
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
inst_3 : IsStrictOrderedRing K
a : ℤ
n : ℕ
zero : Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) 0) none
succ :
  ∀ (n : ℕ) (ih : Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) n) none),
    Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) (n + 1)) none
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) n) none

Tactic:
induction n with
    | zero => rw [of_s_head_aux, stream_succ_of_int, Option.bind]
    | succ n ih => exact (of (a : K)).s.prop ih

Premises used: Option.bind, GenContFract.IntFractPair.stream_succ_of_int, GenContFract.of_s_head_aux, Int.succ
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
inl : ∀ (h : fract v = 0), (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
inr : ∀ (h : fract v ≠ 0), (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
rcases eq_or_ne (fract v) 0 with h | h

Premises used: Int.fract, eq_or_ne, GenContFract.h, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v = 0
⊢ ∃ (a : ℤ), v = (↑a : K)

Tactic:
⟨⌊v⌋, eq_of_sub_eq_zero h⟩

Premises used: Int.floor, eq_of_sub_eq_zero, Exists.intro
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v = 0
inl :
  ∀ (a : ℤ) (h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0),
    Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) (n + 1))
      (Stream'.Seq.get? (s (of (fract (↑a : K))⁻¹)) n)
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩

Premises used: rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
inst_3 : IsStrictOrderedRing K
n : ℕ
a : ℤ
h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0
inl : Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) (n + 1)) (Stream'.Seq.get? (s (of 0⁻¹)) n)
inl₁ : Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) (n + 1)) (Stream'.Seq.get? (s (of 0)) n)
inl₂ : Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? Stream'.Seq.nil (n + 1)) (Stream'.Seq.get? (s (of 0)) n)
inl₃ :
  Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? Stream'.Seq.nil (n + 1)) (Stream'.Seq.get? (s (of (↑0 : K))) n)
inl₄ :
  Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? Stream'.Seq.nil (n + 1)) (Stream'.Seq.get? Stream'.Seq.nil n)
inl₅ : Eq.{u_1 + 1} (α := Option (Pair K)) none (Stream'.Seq.get? Stream'.Seq.nil n)
inl₆ inl₇ : Eq.{u_1 + 1} (α := Option (Pair K)) none none
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) (n + 1))
    (Stream'.Seq.get? (s (of (fract (↑a : K))⁻¹)) n)

Tactic:
rw [fract_intCast, inv_zero, of_s_of_int, ← cast_zero, of_s_of_int,
      Stream'.Seq.get?_nil, Stream'.Seq.get?_nil]

Premises used: Int.cast_zero, inv_zero, Stream'.Seq.get?_nil, Int.fract_intCast, GenContFract.of_s_of_int
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
inr : ∀ (h₁ : (of (fract v)⁻¹).s.get? n = none), (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
inr₁ : ∀ (h₁ : (of (fract v)⁻¹).s.get? n ≠ none), (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
rcases eq_or_ne ((of (fract v)⁻¹).s.get? n) none with h₁ | h₁

Premises used: GenContFract.s, Int.fract, GenContFract.of, Option.none, Inv.inv, eq_or_ne, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n = none
inr : (of v).s.get? (n + 1) = none
inr₁ : (of v).TerminatedAt (n + 1)
inr₂ : IntFractPair.stream v (n + 1 + 1) = none
inr₃ : IntFractPair.stream (fract v)⁻¹ (n + 1) = none
inr₄ : (of (fract v)⁻¹).TerminatedAt n
inr₅ inr₆ inr₇ inr₈ : (of (fract v)⁻¹).s.get? n = none
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
rwa [h₁, ← terminatedAt_iff_s_none,
      of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, stream_succ h, ←
      of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, terminatedAt_iff_s_none]

Premises used: GenContFract.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, GenContFract.terminatedAt_iff_s_none, GenContFract.IntFractPair.stream_succ
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
inr : ∀ (p : Pair K) (hp : (of (fract v)⁻¹).s.get? n = some p), (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp h₁

Premises used: Option.ne_none_iff_exists', Iff.mp
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
inr :
  ∀ (p' : IntFractPair K) (hp'₁ : IntFractPair.stream (fract v)⁻¹ (n + 1) = some p'),
    (↑p'.b : K) = p.b → (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
obtain ⟨p', hp'₁, _⟩ := exists_succ_get?_stream_of_gcf_of_get?_eq_some hp

Premises used: GenContFract.IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream (fract v)⁻¹ (n + 1) = some p'
right : (↑p'.b : K) = p.b
⊢ (of (fract v)⁻¹).s.get? n = some { a := 1, b := (↑p'.b : K) }

Tactic:
have Hp := get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream (fract v)⁻¹ (n + 1) = some p'
right : (↑p'.b : K) = p.b
Hp : (of (fract v)⁻¹).s.get? n = some { a := 1, b := (↑p'.b : K) }
⊢ IntFractPair.stream v (n + 1 + 1) = some p'

Tactic:
rw [← stream_succ h] at hp'₁

Premises used: GenContFract.IntFractPair.stream_succ
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream (fract v)⁻¹ (n + 1) = some p'
right : (↑p'.b : K) = p.b
Hp : (of (fract v)⁻¹).s.get? n = some { a := 1, b := (↑p'.b : K) }
hp'₂ : IntFractPair.stream v (n + 1 + 1) = some p'
⊢ (↑p'.b : K) = p.b

Tactic:
rw [← stream_succ h] at hp'₁

Premises used: GenContFract.IntFractPair.stream_succ
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream (fract v)⁻¹ (n + 1) = some p'
right_1 : (↑p'.b : K) = p.b
Hp : (of (fract v)⁻¹).s.get? n = some { a := 1, b := (↑p'.b : K) }
hp'₂ : IntFractPair.stream v (n + 1 + 1) = some p'
right : (↑p'.b : K) = p.b
⊢ (of (fract v)⁻¹).s.get? n = some { a := 1, b := (↑p'.b : K) }

Tactic:
rw [← stream_succ h] at hp'₁

Premises used: GenContFract.IntFractPair.stream_succ
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream v (n + 1 + 1) = some p'
right : (↑p'.b : K) = p.b
Hp : (of (fract v)⁻¹).s.get? n = some { a := 1, b := (↑p'.b : K) }
inr : (of v).s.get? (n + 1) = some { a := 1, b := (↑p'.b : K) }
inr₁ inr₂ : Eq.{u_1 + 1} (α := Option (Pair K)) (some { a := 1, b := (↑p'.b : K) }) (some { a := 1, b := (↑p'.b : K) })
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
rw [Hp, get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁]

Premises used: GenContFract.get?_of_eq_some_of_succ_get?_intFractPair_stream
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
⊢ (of v).s.tail = (of (fract v)⁻¹).s

Tactic:
Stream'.Seq.ext fun n => Stream'.Seq.get?_tail (of v).s n ▸ of_s_succ v n

Premises used: GenContFract.s, Stream'.Seq.get?_tail, Stream'.Seq.ext, Eq.rec, GenContFract.of, GenContFract.of_s_succ