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
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)
⊢ 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? Stream'.Seq.nil (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)
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)
⊢ 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? Stream'.Seq.nil (n + 1)) (Stream'.Seq.get? (s (of (↑0 : 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]
-- 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)
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)
⊢ 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? Stream'.Seq.nil (n + 1)) (Stream'.Seq.get? Stream'.Seq.nil 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)
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)
⊢ 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)) none (Stream'.Seq.get? Stream'.Seq.nil 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)
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)
⊢ 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)) none none
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
v : K
inst_3 : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have inr : ∀ (h₁ : (of (fract v)⁻¹).s.get? n = none), (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₁
-- 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
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
have inr₁ : ∀ (h₁ : (of (fract v)⁻¹).s.get? n ≠ none), (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₁
-- 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
h₁ : (of (fract v)⁻¹).s.get? n = none
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have inr : (of v).s.get? (n + 1) = none
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]
-- 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
h₁ : (of (fract v)⁻¹).s.get? n = none
inr : (of v).s.get? (n + 1) = none
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have inr₁ : (of v).TerminatedAt (n + 1)
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]
-- 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
h₁ : (of (fract v)⁻¹).s.get? n = none
inr : (of v).s.get? (n + 1) = none
inr₁ : (of v).TerminatedAt (n + 1)
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have inr₂ : IntFractPair.stream v (n + 1 + 1) = none
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]
-- 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
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
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have inr₃ : IntFractPair.stream (fract v)⁻¹ (n + 1) = none
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]
-- 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
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
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have inr₄ : (of (fract v)⁻¹).TerminatedAt 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]
-- 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
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have 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
Tactic: obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp 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
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have 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
Tactic: obtain ⟨p', hp'₁, _⟩ := exists_succ_get?_stream_of_gcf_of_get?_eq_some hp
-- 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
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 v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have Hp : (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'₁
-- 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
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) }
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have hp'₂ : IntFractPair.stream v (n + 1 + 1) = some p'
Tactic: rw [← stream_succ h] at hp'₁
Cleared hypotheses: hp'₁, right, 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
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) }
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have inr : (of v).s.get? (n + 1) = some { a := 1, b := (↑p'.b : K) }
Tactic: rw [Hp, get?_of_eq_some_of_succ_get?_intFractPair_stream 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
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) }
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
have inr₁ : Eq.{u_1 + 1} (α := Option (Pair K)) (some { a := 1, b := (↑p'.b : K) }) (some { a := 1, b := (↑p'.b : K) })
Tactic: rw [Hp, get?_of_eq_some_of_succ_get?_intFractPair_stream 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
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
n_1 : ℕ
h : Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) n_1) (↑a : K)
⊢ Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) (n_1 + 1)) (↑a : K)
have succ : Eq.{u_1 + 1} (α := K) (convs'Aux (s (of (↑a : K))) (n_1 + 1)) 0
Tactic: rw [convs', of_h_eq_floor, floor_intCast, add_eq_left]
-- 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
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
⊢ Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) n) (↑a : K)
have zero : Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) 0) (↑a : K)
Tactic: induction n with
  | zero => simp only [zeroth_conv'_eq_h, of_h_eq_floor, floor_intCast]
  | succ =>
    rw [convs', of_h_eq_floor, floor_intCast, add_eq_left]
    exact convs'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _
-- 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
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
zero : Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) 0) (↑a : K)
⊢ Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) n) (↑a : K)
have succ : ∀ (n : ℕ),
  Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) n) (↑a : K) →
    Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) (n + 1)) (↑a : K)
Tactic: induction n with
  | zero => simp only [zeroth_conv'_eq_h, of_h_eq_floor, floor_intCast]
  | succ =>
    rw [convs', of_h_eq_floor, floor_intCast, add_eq_left]
    exact convs'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _
-- 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 : ℕ
inst_3 : IsStrictOrderedRing K
⊢ (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' n
have inl : ∀ (h : fract v = 0), (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' 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
n : ℕ
inst_3 : IsStrictOrderedRing K
inl : ∀ (h : fract v = 0), (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' n
⊢ (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' n
have inr : ∀ (h : fract v ≠ 0), (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' 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
n : ℕ
inst_3 : IsStrictOrderedRing K
h : fract v = 0
⊢ (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' n
have inl : ∀ (a : ℤ) (h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0),
  convs' (of (↑a : K)) (n + 1) =
    (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (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
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0
⊢ convs' (of (↑a : K)) (n + 1) =
    (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
have inl : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
Tactic: rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]
-- 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
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0
inl : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
⊢ convs' (of (↑a : K)) (n + 1) =
    (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
have inl₁ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0⁻¹) n)
Tactic: rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]
-- 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
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0
inl : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
inl₁ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0⁻¹) n)
⊢ convs' (of (↑a : K)) (n + 1) =
    (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
have inl₂ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0) n)
Tactic: rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]
-- 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
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0
inl : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
inl₁ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0⁻¹) n)
inl₂ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0) n)
⊢ convs' (of (↑a : K)) (n + 1) =
    (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
have inl₃ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (↑0 : K)) n)
Tactic: rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]
-- 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
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0
inl : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
inl₁ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0⁻¹) n)
inl₂ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0) n)
inl₃ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (↑0 : K)) n)
⊢ convs' (of (↑a : K)) (n + 1) =
    (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
have inl₄ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (↑0 : K)
Tactic: rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]
-- 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
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0
inl : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
inl₁ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0⁻¹) n)
inl₂ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0) n)
inl₃ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (↑0 : K)) n)
inl₄ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (↑0 : K)
⊢ convs' (of (↑a : K)) (n + 1) =
    (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
have inl₅ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + 1 / 0
Tactic: rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]
-- 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
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0
inl : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
inl₁ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0⁻¹) n)
inl₂ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0) n)
inl₃ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (↑0 : K)) n)
inl₄ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (↑0 : K)
inl₅ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + 1 / 0
⊢ convs' (of (↑a : K)) (n + 1) =
    (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
have inl₆ : (↑a : K) = HAdd.hAdd (α := K) (↑(floor.{u_1} (α := K) (↑a : K)) : K) 0
Tactic: rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]