awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
succ :
  ∀ (hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none),
    IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have succ₁ : ∀ (hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none),
  IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
Tactic: rcases eq_or_ne (IntFractPair.stream (Int.fract v)⁻¹ n) none with hnone | hsome
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (hypothesis)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have ih₁ : IntFractPair.stream v (n + 1) = none
Tactic: rw [hnone] at ih
Cleared hypotheses: ih, hnone
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = none
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have succ : IntFractPair.stream v (n + 1 + 1) = none
Tactic: rw [succ_nth_stream_eq_none_iff.mpr (Or.inl hnone),
        succ_nth_stream_eq_none_iff.mpr (Or.inl ih)]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = none
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
succ : IntFractPair.stream v (n + 1 + 1) = none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have succ₁ : Eq.{u_1 + 1} (α := Option (IntFractPair K)) none none
Tactic: rw [succ_nth_stream_eq_none_iff.mpr (Or.inl hnone),
        succ_nth_stream_eq_none_iff.mpr (Or.inl ih)]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have succ : ∀ (p : IntFractPair K) (hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p),
  IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
Tactic: obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp hsome
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (hypothesis)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have ih₁ : IntFractPair.stream v (n + 1) = some p
Tactic: rw [hp] at ih
Cleared hypotheses: ih, hp
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have succ : ∀ (hz : p.fr = 0), IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
Tactic: rcases eq_or_ne p.fr 0 with hz | hnz
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
succ : ∀ (hz : p.fr = 0), IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have succ₁ : ∀ (hnz : p.fr ≠ 0), IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
Tactic: rcases eq_or_ne p.fr 0 with hz | hnz
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hz : p.fr = 0
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have succ : IntFractPair.stream v (n + 1 + 1) = none
Tactic: rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hz : p.fr = 0
succ : IntFractPair.stream v (n + 1 + 1) = none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have succ₁ : Eq.{u_1 + 1} (α := Option (IntFractPair K)) none none
Tactic: rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hnz : p.fr ≠ 0
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have succ : IntFractPair.stream v (n + 1 + 1) = some (IntFractPair.of p.fr⁻¹)
Tactic: rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hnz : p.fr ≠ 0
succ : IntFractPair.stream v (n + 1 + 1) = some (IntFractPair.of p.fr⁻¹)
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
have succ₁ : some (IntFractPair.of p.fr⁻¹) = some (IntFractPair.of p.fr⁻¹)
Tactic: rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
⊢ IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
have zero : IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = IntFractPair.stream (Int.fract v)⁻¹ 0
Tactic: induction n with
  | zero =>
    have H : (IntFractPair.of v).fr = Int.fract v := by simp [IntFractPair.of]
    rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H h), H]
  | succ n ih =>
    rcases eq_or_ne (IntFractPair.stream (Int.fract v)⁻¹ n) none with hnone | hsome
    · rw [hnone] at ih
      rw [succ_nth_stream_eq_none_iff.mpr (Or.inl hnone),
        succ_nth_stream_eq_none_iff.mpr (Or.inl ih)]
    · obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp hsome
      rw [hp] at ih
      rcases eq_or_ne p.fr 0 with hz | hnz
      · rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]
      · rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
zero : IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = IntFractPair.stream (Int.fract v)⁻¹ 0
⊢ IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
have succ : ∀ (n : ℕ) (ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n),
  IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
Tactic: induction n with
  | zero =>
    have H : (IntFractPair.of v).fr = Int.fract v := by simp [IntFractPair.of]
    rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H h), H]
  | succ n ih =>
    rcases eq_or_ne (IntFractPair.stream (Int.fract v)⁻¹ n) none with hnone | hsome
    · rw [hnone] at ih
      rw [succ_nth_stream_eq_none_iff.mpr (Or.inl hnone),
        succ_nth_stream_eq_none_iff.mpr (Or.inl ih)]
    · obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp hsome
      rw [hp] at ih
      rcases eq_or_ne p.fr 0 with hz | hnz
      · rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]
      · rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
⊢ (of v).h = (↑(IntFractPair.seq1 v).1.b : K)
have mk : ∀ (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: cases aux_seq_eq : IntFractPair.seq1 v
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
⊢ (of v).TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none
have rw : (IntFractPair.seq1 v).2.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]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ (of v).TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none
have rw₁ : (IntFractPair.seq1 v).2.get? n = none ↔ IntFractPair.stream v (n + 1) = none
Tactic: rw [of_terminatedAt_iff_intFractPair_seq1_terminatedAt, Stream'.Seq.TerminatedAt,
    IntFractPair.get?_seq1_eq_succ_get?_stream]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ (of v).TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none
have rw₂ : IntFractPair.stream v (n + 1) = none ↔ IntFractPair.stream v (n + 1) = none
Tactic: rw [of_terminatedAt_iff_intFractPair_seq1_terminatedAt, Stream'.Seq.TerminatedAt,
    IntFractPair.get?_seq1_eq_succ_get?_stream]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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), IntFractPair.stream v (n + 1) = some ifp ∧ (↑ifp.b : K) = gp_n.b
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ ∃ (ifp : IntFractPair K), IntFractPair.stream v (n + 1) = some ifp ∧ (↑ifp.b : K) = gp_n.b
have 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) })
Tactic: cases gp_n_eq
Cleared hypotheses: gp_n, s_nth_eq, gp_n_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : 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) }))
have 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) }))
Tactic: simp only [Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.get?, Stream'.map]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : 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) }))
have 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))
Tactic: rw [← Stream'.get_succ, Stream'.get, Option.map.eq_def]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : 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))
have 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) }))
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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) }))
⊢ 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))
have 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) }))
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
h : fract v ≠ 0
⊢ (of v).s.get? 0 = some { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) }
have 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) })
Tactic: rw [of_s_head_aux, stream_succ_of_some (stream_zero v) h, Option.bind]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
inst_3 : IsStrictOrderedRing K
a : ℤ
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) 0) none
have 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
Tactic: rw [of_s_head_aux, stream_succ_of_int, Option.bind]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) 0) none
have 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
Tactic: rw [of_s_head_aux, stream_succ_of_int, Option.bind]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) 0) none
have zero₂ : Eq.{u_1 + 1} (α := Option (Pair K)) none none
Tactic: rw [of_s_head_aux, stream_succ_of_int, Option.bind]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
inst_3 : IsStrictOrderedRing K
a : ℤ
n : ℕ
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) n) none
have zero : Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) 0) 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) n) none
have 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
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have inl : ∀ (h : fract v = 0), (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
Tactic: rcases eq_or_ne (fract v) 0 with h | h
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have inr : ∀ (h : fract v ≠ 0), (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
Tactic: rcases eq_or_ne (fract v) 0 with h | h
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have 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)
Tactic: obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
Cleared hypotheses: v, h
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ 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)
have inl : Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) (n + 1)) (Stream'.Seq.get? (s (of 0⁻¹)) 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]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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)
⊢ 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)
have inl₁ : Eq.{u_1 + 1} (α := Option (Pair K)) (Stream'.Seq.get? (s (of (↑a : K))) (n + 1)) (Stream'.Seq.get? (s (of 0)) 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]