awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
have obtain : ∀ (ifp_n' : IntFractPair ℚ) (stream_nth_eq' : IntFractPair.stream q n = some ifp_n')
  (ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0) (IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n),
  ifp_succ_n.fr.num < ifp_n.fr.num
Tactic: obtain ⟨ifp_n', stream_nth_eq', ifp_n_fract_ne_zero, IntFractPair.of_eq_ifp_succ_n⟩ :
    ∃ ifp_n',
      IntFractPair.stream q n = some ifp_n' ∧
        ifp_n'.fr ≠ 0 ∧ IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n :=
    succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n' : IntFractPair ℚ
stream_nth_eq' : IntFractPair.stream q n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
have this : ifp_n = ifp_n'
Tactic: have : ifp_n = ifp_n' := by injection Eq.trans stream_nth_eq.symm stream_nth_eq'
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n' : IntFractPair ℚ
stream_nth_eq' : IntFractPair.stream q n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
this : ifp_n = ifp_n'
stream_nth_eq'₁ : IntFractPair.stream q n = some ifp_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
have ifp_n_fract_ne_zero₁ : ifp_n.fr ≠ 0
Tactic: cases this
Cleared hypotheses: ifp_n', stream_nth_eq', ifp_n_fract_ne_zero, IntFractPair.of_eq_ifp_succ_n, this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n' : IntFractPair ℚ
stream_nth_eq' : IntFractPair.stream q n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
this : ifp_n = ifp_n'
stream_nth_eq'₁ : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero₁ : ifp_n.fr ≠ 0
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
have IntFractPair : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
Tactic: cases this
Cleared hypotheses: ifp_n', stream_nth_eq', ifp_n_fract_ne_zero, IntFractPair.of_eq_ifp_succ_n, this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
have refl : (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
Tactic: rw [← IntFractPair.of_eq_ifp_succ_n]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
have zero_le_ifp_n_fract : 0 ≤ ifp_n.fr
Tactic: obtain ⟨zero_le_ifp_n_fract, _⟩ := nth_stream_fr_nonneg_lt_one stream_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
zero_le_ifp_n_fract : 0 ≤ ifp_n.fr
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
have right : ifp_n.fr < 1
Tactic: obtain ⟨zero_le_ifp_n_fract, _⟩ := nth_stream_fr_nonneg_lt_one stream_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
zero_le_ifp_n_fract : 0 ≤ ifp_n.fr
right : ifp_n.fr < 1
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
have this : 0 < ifp_n.fr
Tactic: have : 0 < ifp_n.fr := lt_of_le_of_ne zero_le_ifp_n_fract <| ifp_n_fract_ne_zero.symm
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q 0 = some ifp_zero
⊢ ifp_zero.fr.num ≤ (IntFractPair.of q).fr.num - (↑0 : ℤ)
have this : IntFractPair.of q = ifp_zero
Tactic: have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
q : ℚ
n_1 n : ℕ
IH :
  ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
this : ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑(n + 1) : ℤ)
have rw : ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑n : ℤ) - 1
Tactic: rw [Int.natCast_succ, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
q : ℚ
n_1 n : ℕ
IH :
  ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑(n + 1) : ℤ)
have succ : ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
Tactic: suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n by
      rw [Int.natCast_succ, sub_add_eq_sub_sub]
      solve_by_elim [le_sub_right_of_add_le]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
q : ℚ
n_1 n : ℕ
IH :
  ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
have succ : ∀ (ifp_n : IntFractPair ℚ) (stream_nth_eq : IntFractPair.stream q n = some ifp_n),
  ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
Tactic: rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
n_1 n : ℕ
IH :
  ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
have this : ifp_succ_n.fr.num < ifp_n.fr.num
Tactic: have : ifp_succ_n.fr.num < ifp_n.fr.num :=
      stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
q : ℚ
n : ℕ
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
have zero : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q 0 = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑0 : ℤ)
Tactic: induction n with
  | zero =>
    intro ifp_zero stream_zero_eq
    have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
    simp [this.symm]
  | succ n IH =>
    intro ifp_succ_n stream_succ_nth_eq
    suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n by
      rw [Int.natCast_succ, sub_add_eq_sub_sub]
      solve_by_elim [le_sub_right_of_add_le]
    rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
    have : ifp_succ_n.fr.num < ifp_n.fr.num :=
      stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq
    exact le_trans this (IH stream_nth_eq)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
q : ℚ
n : ℕ
zero :
  ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q 0 = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑0 : ℤ)
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
have succ : ∀ (n : ℕ)
  (IH :
    ∀ {ifp_n : IntFractPair ℚ},
      IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑n : ℤ))
  {ifp_n : IntFractPair ℚ},
  IntFractPair.stream q (n + 1) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑(n + 1) : ℤ)
Tactic: induction n with
  | zero =>
    intro ifp_zero stream_zero_eq
    have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
    simp [this.symm]
  | succ n IH =>
    intro ifp_succ_n stream_succ_nth_eq
    suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n by
      rw [Int.natCast_succ, sub_add_eq_sub_sub]
      solve_by_elim [le_sub_right_of_add_le]
    rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
    have : ifp_succ_n.fr.num < ifp_n.fr.num :=
      stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq
    exact le_trans this (IH stream_nth_eq)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
⊢ ∃ (n : ℕ), IntFractPair.stream q n = none
have none : ∀ (stream_nth_eq : IntFractPair.stream q n = none), ∃ (n : ℕ), IntFractPair.stream q n = none
Tactic: rcases stream_nth_eq : IntFractPair.stream q n with ifp | ifp
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
none : ∀ (stream_nth_eq : IntFractPair.stream q n = Option.none), ∃ (n : ℕ), IntFractPair.stream q n = Option.none
⊢ ∃ (n : ℕ), IntFractPair.stream q n = Option.none
have some : ∀ (ifp : IntFractPair ℚ) (stream_nth_eq : IntFractPair.stream q n = some ifp),
  ∃ (n : ℕ), IntFractPair.stream q n = Option.none
Tactic: rcases stream_nth_eq : IntFractPair.stream q n with ifp | ifp
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
⊢ ∃ (n : ℕ), IntFractPair.stream q n = none
have ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - (↑n : ℤ)
Tactic: have ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - n :=
      stream_nth_fr_num_le_fr_num_sub_n_rat stream_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - (↑n : ℤ)
⊢ fract_q_num - (↑n : ℤ) = -1
have this : 0 ≤ fract_q_num
Tactic: have : 0 ≤ fract_q_num := Rat.num_nonneg.mpr (Int.fract_nonneg q)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - (↑n : ℤ)
⊢ ∃ (n : ℕ), IntFractPair.stream q n = none
have this : fract_q_num - (↑n : ℤ) = -1
Tactic: have : fract_q_num - n = -1 := by
      have : 0 ≤ fract_q_num := Rat.num_nonneg.mpr (Int.fract_nonneg q)
      simp only [n, Nat.cast_add, Int.natAbs_of_nonneg this, Nat.cast_one,
        sub_add_eq_sub_sub_swap, sub_right_comm, sub_self, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - (↑n : ℤ)
this : fract_q_num - (↑n : ℤ) = -1
⊢ ∃ (n : ℕ), IntFractPair.stream q n = none
have this₁ : 0 ≤ ifp.fr
Tactic: have : 0 ≤ ifp.fr := (nth_stream_fr_nonneg_lt_one stream_nth_eq).left
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - (↑n : ℤ)
this_1 : fract_q_num - (↑n : ℤ) = -1
this : 0 ≤ ifp.fr
⊢ ∃ (n : ℕ), IntFractPair.stream q n = none
have this₁ : 0 ≤ ifp.fr.num
Tactic: have : 0 ≤ ifp.fr.num := Rat.num_nonneg.mpr this
-- 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 : ℕ
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
nth_fr_eq_zero : ifp_n.fr = 0
⊢ IntFractPair.stream v (n + 1) = none
have obtain : ∀ (b : ℤ) (fr : K) (stream_nth_eq : IntFractPair.stream v n = some { b := b, fr := fr })
  (nth_fr_eq_zero : { b := b, fr := fr : IntFractPair K }.fr = 0), IntFractPair.stream v (n + 1) = none
Tactic: obtain ⟨_, fr⟩ := ifp_n
Cleared hypotheses: ifp_n, stream_nth_eq, nth_fr_eq_zero
-- 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
n : ℕ
b : ℤ
fr : K
stream_nth_eq : IntFractPair.stream v n = some { b := b, fr := fr }
nth_fr_eq_zero : { b := b, fr := fr : IntFractPair K }.fr = 0
⊢ IntFractPair.stream v (n + 1) = none
have nth_fr_eq_zero₁ : fr = 0
Tactic: change fr = 0 at nth_fr_eq_zero
Cleared hypotheses: nth_fr_eq_zero
-- 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 : ℕ
⊢ Eq (α := Option (IntFractPair K))
      ((IntFractPair.stream v n).bind fun (ap_n : IntFractPair K) ↦
        if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹))
      none ↔
    IntFractPair.stream v n = none ∨ ∃ (ifp : IntFractPair K), IntFractPair.stream v n = some ifp ∧ ifp.fr = 0
have none : Eq.{u_1 + 1} (α := Option (IntFractPair K))
    (Option.bind none fun (ap_n : IntFractPair K) ↦ if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹))
    none ↔
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) none none ∨ ∃ (ifp : IntFractPair K), none = some ifp ∧ ifp.fr = 0
Tactic: cases IntFractPair.stream v 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
n : ℕ
none :
  Eq.{u_1 + 1} (α := Option (IntFractPair K))
      (Option.bind Option.none fun (ap_n : IntFractPair K) ↦
        if ap_n.fr = 0 then Option.none else some (IntFractPair.of ap_n.fr⁻¹))
      Option.none ↔
    Eq.{u_1 + 1} (α := Option (IntFractPair K)) Option.none Option.none ∨
      ∃ (ifp : IntFractPair K), Option.none = some ifp ∧ ifp.fr = 0
⊢ Eq (α := Option (IntFractPair K))
      ((IntFractPair.stream v n).bind fun (ap_n : IntFractPair K) ↦
        if ap_n.fr = 0 then Option.none else some (IntFractPair.of ap_n.fr⁻¹))
      Option.none ↔
    IntFractPair.stream v n = Option.none ∨ ∃ (ifp : IntFractPair K), IntFractPair.stream v n = some ifp ∧ ifp.fr = 0
have some : ∀ (val : IntFractPair K),
  Eq (α := Option (IntFractPair K))
      ((some val).bind fun (ap_n : IntFractPair K) ↦
        if ap_n.fr = 0 then Option.none else some (IntFractPair.of ap_n.fr⁻¹))
      Option.none ↔
    some val = Option.none ∨ ∃ (ifp : IntFractPair K), some val = some ifp ∧ ifp.fr = 0
Tactic: cases IntFractPair.stream v 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 : ℤ
⊢ Eq.{u_1 + 1} (α := Option (IntFractPair K)) (IntFractPair.stream (↑a : K) (HAdd.hAdd (α := ℕ) 0 1)) none
have zero : Eq.{u_1 + 1} (α := K) (fr (IntFractPair.of (↑a : K))) 0
Tactic: refine IntFractPair.stream_eq_none_of_fr_eq_zero (IntFractPair.stream_zero (a : K)) ?_
-- 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 (IntFractPair K)) (IntFractPair.stream (↑a : K) (n + 1)) none
have zero : Eq.{u_1 + 1} (α := Option (IntFractPair K)) (IntFractPair.stream (↑a : K) (HAdd.hAdd (α := ℕ) 0 1)) none
Tactic: induction n with
  | zero =>
    refine IntFractPair.stream_eq_none_of_fr_eq_zero (IntFractPair.stream_zero (a : K)) ?_
    simp only [IntFractPair.of, Int.fract_intCast]
  | succ n ih => exact IntFractPair.succ_nth_stream_eq_none_iff.mpr (Or.inl 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 (IntFractPair K)) (IntFractPair.stream (↑a : K) (HAdd.hAdd (α := ℕ) 0 1)) none
⊢ Eq.{u_1 + 1} (α := Option (IntFractPair K)) (IntFractPair.stream (↑a : K) (n + 1)) none
have succ : ∀ (n : ℕ) (ih : Eq.{u_1 + 1} (α := Option (IntFractPair K)) (IntFractPair.stream (↑a : K) (n + 1)) none),
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) (IntFractPair.stream (↑a : K) (n + 1 + 1)) none
Tactic: induction n with
  | zero =>
    refine IntFractPair.stream_eq_none_of_fr_eq_zero (IntFractPair.stream_zero (a : K)) ?_
    simp only [IntFractPair.of, Int.fract_intCast]
  | succ n ih => exact IntFractPair.succ_nth_stream_eq_none_iff.mpr (Or.inl 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
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
succ_nth_fr_eq_zero : ifp_succ_n.fr = 0
⊢ ∃ (ifp_n : IntFractPair K), IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = (↑⌊ifp_n.fr⁻¹⌋ : K)
have rcases : ∀ (ifp_n : IntFractPair K) (seq_nth_eq : IntFractPair.stream v n = some ifp_n),
  ifp_n.fr ≠ 0 →
    ∀ (stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹))
      (succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0),
      ∃ (ifp_n : IntFractPair K), IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = (↑⌊ifp_n.fr⁻¹⌋ : K)
Tactic: rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with
    ⟨ifp_n, seq_nth_eq, _, rfl⟩
Cleared hypotheses: ifp_succ_n, stream_succ_nth_eq, succ_nth_fr_eq_zero
-- 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 : ℕ
ifp_n : IntFractPair K
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ∃ (ifp_n : IntFractPair K), IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = (↑⌊ifp_n.fr⁻¹⌋ : K)
have refine : ifp_n.fr⁻¹ = (↑⌊ifp_n.fr⁻¹⌋ : K)
Tactic: refine ⟨ifp_n, seq_nth_eq, ?_⟩
-- 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
⊢ IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = IntFractPair.stream (Int.fract v)⁻¹ 0
have H : (IntFractPair.of v).fr = Int.fract v
Tactic: have H : (IntFractPair.of v).fr = Int.fract v := by simp [IntFractPair.of]
-- 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
H : (IntFractPair.of v).fr = Int.fract v
⊢ IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = IntFractPair.stream (Int.fract v)⁻¹ 0
have zero : IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = some (IntFractPair.of (Int.fract v)⁻¹)
Tactic: rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H 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
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
zero : IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = some (IntFractPair.of (Int.fract v)⁻¹)
⊢ IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = IntFractPair.stream (Int.fract v)⁻¹ 0
have zero₁ : some (IntFractPair.of (IntFractPair.of v).fr⁻¹) = some (IntFractPair.of (Int.fract v)⁻¹)
Tactic: rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H 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
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
zero : IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = some (IntFractPair.of (Int.fract v)⁻¹)
zero₁ : some (IntFractPair.of (IntFractPair.of v).fr⁻¹) = some (IntFractPair.of (Int.fract v)⁻¹)
⊢ IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = IntFractPair.stream (Int.fract v)⁻¹ 0
have zero₂ : some (IntFractPair.of (Int.fract v)⁻¹) = some (IntFractPair.of (Int.fract v)⁻¹)
Tactic: rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H 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
h : Int.fract v ≠ 0
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)
have succ : ∀ (hnone : 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