awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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

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]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
⊢ 0 ≤ ifp.fr

Tactic:
have : 0 ≤ ifp.fr := (nth_stream_fr_nonneg_lt_one stream_nth_eq).left
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
⊢ 0 ≤ ifp.fr.num

Tactic:
have : 0 ≤ ifp.fr.num := Rat.num_nonneg.mpr this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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_2 : 0 ≤ ifp.fr
this : 0 ≤ ifp.fr.num
⊢ ∃ (n : ℕ), IntFractPair.stream q n = none

Tactic:
lia
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
⊢ (of q).Terminates

Tactic:
Exists.elim (IntFractPair.exists_nth_stream_eq_none_of_rat q) fun n stream_nth_eq_none =>
    Exists.intro n
      (have : IntFractPair.stream q (n + 1) = none := IntFractPair.stream_isSeq q stream_nth_eq_none
      of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.mpr this)

Premises used: Iff.mpr, GenContFract.IntFractPair.stream_isSeq, GenContFract.IntFractPair.exists_nth_stream_eq_none_of_rat, GenContFract.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, Exists.intro, Exists.elim
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
⊢ (of v).Terminates ↔ ∃ (q : ℚ), v = (↑q : K)

Tactic:
Iff.intro
    (fun terminates_v : (of v).Terminates =>
      show ∃ q : ℚ, v = (q : K) from exists_rat_eq_of_terminates terminates_v)
    fun exists_q_eq_v : ∃ q : ℚ, v = (↑q : K) =>
    Exists.elim exists_q_eq_v fun q => fun v_eq_q : v = ↑q =>
      have : (of q).Terminates := terminates_of_rat q
      (of_terminates_iff_of_rat_terminates v_eq_q).mpr this

Premises used: Iff.mpr, GenContFract.exists_rat_eq_of_terminates, GenContFract.of_terminates_iff_of_rat_terminates, Iff.intro, GenContFract.terminates_of_rat, Exists.elim
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
⊢ IntFractPair.stream v 0 = some (IntFractPair.of v)

Tactic:
rfl

Premises used: GenContFract.IntFractPair.stream, 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 : ℕ
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
nth_fr_eq_zero : ifp_n.fr = 0
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
⊢ IntFractPair.stream v (n + 1) = none

Tactic:
obtain ⟨_, fr⟩ := ifp_n

Premises used: GenContFract.IntFractPair.fr
-- 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 : ℕ
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
⊢ fr = 0

Tactic:
change fr = 0 at nth_fr_eq_zero
-- 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 : ℕ
b : ℤ
fr : K
stream_nth_eq : IntFractPair.stream v n = some { b := b, fr := fr }
nth_fr_eq_zero : fr = 0
⊢ IntFractPair.stream v (n + 1) = none

Tactic:
simp [IntFractPair.stream, stream_nth_eq, nth_fr_eq_zero]

Premises used: GenContFract.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
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 Option.some (IntFractPair.of ap_n.fr⁻¹))
      Option.none ↔
    Eq.{u_1 + 1} (α := Option (IntFractPair K)) Option.none Option.none ∨
      ∃ (ifp : IntFractPair K), Option.none = Option.some ifp ∧ ifp.fr = 0
some :
  ∀ (val : IntFractPair K),
    Eq (α := Option (IntFractPair K))
        ((Option.some val).bind fun (ap_n : IntFractPair K) ↦
          if ap_n.fr = 0 then Option.none else Option.some (IntFractPair.of ap_n.fr⁻¹))
        Option.none ↔
      Option.some val = Option.none ∨ ∃ (ifp : IntFractPair K), Option.some val = Option.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 Option.some (IntFractPair.of ap_n.fr⁻¹))
      Option.none ↔
    IntFractPair.stream v n = Option.none ∨
      ∃ (ifp : IntFractPair K), IntFractPair.stream v n = Option.some ifp ∧ ifp.fr = 0

Tactic:
cases IntFractPair.stream v n

Premises used: GenContFract.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
n : ℕ
⊢ 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:
simp [imp_false]

Premises used: imp_false
-- 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 : ℕ
val : IntFractPair K
⊢ Eq (α := Option (IntFractPair K))
      ((some val).bind fun (ap_n : IntFractPair K) ↦ if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹))
      none ↔
    some val = none ∨ ∃ (ifp : IntFractPair K), some val = some ifp ∧ ifp.fr = 0

Tactic:
simp [imp_false]

Premises used: imp_false
-- 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
⊢ IntFractPair.stream v (n + 1) = some ifp_succ_n ↔
    ∃ (ifp_n : IntFractPair K),
      IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n

Tactic:
simp [IntFractPair.stream, ite_eq_iff, Option.bind_eq_some_iff]

Premises used: GenContFract.IntFractPair.stream, Option.bind_eq_some_iff, ite_eq_iff
-- 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 : ℕ
p : IntFractPair K
h : IntFractPair.stream v n = some p
h' : p.fr ≠ 0
⊢ IntFractPair.stream v (n + 1) = some (IntFractPair.of p.fr⁻¹)

Tactic:
succ_nth_stream_eq_some_iff.mpr ⟨p, h, h', rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, rfl, GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
-- 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 : ℤ
⊢ Eq.{u_1 + 1} (α := Option (IntFractPair K)) (IntFractPair.stream (↑a : K) (HAdd.hAdd (α := ℕ) 0 1)) none

Tactic:
IntFractPair.stream_eq_none_of_fr_eq_zero (IntFractPair.stream_zero (a : K)) ?_

Premises used: Int.cast, GenContFract.IntFractPair.stream_eq_none_of_fr_eq_zero, GenContFract.IntFractPair.stream_zero
-- 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} (α := K) (fr (IntFractPair.of (↑a : K))) 0
⊢ Eq.{u_1 + 1} (α := Option (IntFractPair K)) (IntFractPair.stream (↑a : K) (HAdd.hAdd (α := ℕ) 0 1)) none

Tactic:
refine IntFractPair.stream_eq_none_of_fr_eq_zero (IntFractPair.stream_zero (a : K)) ?_

Premises used: Int.cast, GenContFract.IntFractPair.stream_eq_none_of_fr_eq_zero, GenContFract.IntFractPair.stream_zero
-- 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 : ℤ
⊢ Eq.{u_1 + 1} (α := K) (fr (IntFractPair.of (↑a : K))) 0

Tactic:
simp only [IntFractPair.of, Int.fract_intCast]

Premises used: Int.fract_intCast, GenContFract.IntFractPair.of
-- 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 (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:
IntFractPair.succ_nth_stream_eq_none_iff.mpr (Or.inl ih)

Premises used: Iff.mpr, GenContFract.IntFractPair.succ_nth_stream_eq_none_iff, Or.inl
-- 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 (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:
exact IntFractPair.succ_nth_stream_eq_none_iff.mpr (Or.inl ih)

Premises used: Iff.mpr, GenContFract.IntFractPair.succ_nth_stream_eq_none_iff, Or.inl
-- 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 (IntFractPair K)) (IntFractPair.stream (↑a : K) (HAdd.hAdd (α := ℕ) 0 1)) none
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
⊢ Eq.{u_1 + 1} (α := Option (IntFractPair K)) (IntFractPair.stream (↑a : K) (n + 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)

Premises used: Int.cast, Int.fract_intCast, GenContFract.IntFractPair.stream_eq_none_of_fr_eq_zero, GenContFract.IntFractPair.of, GenContFract.IntFractPair.stream_zero
-- 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
succ_nth_fr_eq_zero : ifp_succ_n.fr = 0
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)
⊢ ∃ (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⟩

Premises used: Iff.mp, rfl, GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
-- 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
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)

Tactic:
⟨ifp_n, seq_nth_eq, ?_⟩

Premises used: And.intro, 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
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
refine : ifp_n.fr⁻¹ = (↑⌊ifp_n.fr⁻¹⌋ : K)
⊢ ∃ (ifp_n : IntFractPair K), IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = (↑⌊ifp_n.fr⁻¹⌋ : K)

Tactic:
refine ⟨ifp_n, seq_nth_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_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.fr⁻¹ = (↑⌊ifp_n.fr⁻¹⌋ : K)

Tactic:
simpa only [IntFractPair.of, Int.fract, sub_eq_zero] using succ_nth_fr_eq_zero

Premises used: sub_eq_zero, Int.fract, GenContFract.IntFractPair.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
h : Int.fract v ≠ 0
⊢ (IntFractPair.of v).fr = Int.fract v

Tactic:
simp [IntFractPair.of]

Premises used: GenContFract.IntFractPair.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
h : Int.fract v ≠ 0
⊢ (IntFractPair.of v).fr = Int.fract v

Tactic:
have H : (IntFractPair.of v).fr = Int.fract v := by simp [IntFractPair.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
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)⁻¹)
zero₂ zero₃ : some (IntFractPair.of (Int.fract v)⁻¹) = some (IntFractPair.of (Int.fract v)⁻¹)
⊢ IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = IntFractPair.stream (Int.fract v)⁻¹ 0

Tactic:
rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H h), H]

Premises used: ne_of_eq_of_ne, 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 : 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)
succ₁ :
  ∀ (hsome : 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)

Tactic:
rcases eq_or_ne (IntFractPair.stream (Int.fract v)⁻¹ n) none with hnone | hsome

Premises used: GenContFract.IntFractPair.stream, Int.fract, Option.none, Inv.inv, eq_or_ne
-- 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 : 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) = none

Tactic:
rw [hnone] at ih
-- 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 : 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
ih₁ : IntFractPair.stream v (n + 1) = none
⊢ IntFractPair.stream (Int.fract v)⁻¹ n = none

Tactic:
rw [hnone] at ih
-- 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 : 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
succ₁ succ₂ : Eq.{u_1 + 1} (α := Option (IntFractPair K)) none none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rw [succ_nth_stream_eq_none_iff.mpr (Or.inl hnone),
        succ_nth_stream_eq_none_iff.mpr (Or.inl ih)]

Premises used: Iff.mpr, GenContFract.IntFractPair.succ_nth_stream_eq_none_iff, Or.inl
-- 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 : 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
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)
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

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

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
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) = some p

Tactic:
rw [hp] at ih
-- 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 : 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
ih₁ : IntFractPair.stream v (n + 1) = some p
⊢ IntFractPair.stream (Int.fract v)⁻¹ n = some p

Tactic:
rw [hp] at ih
-- 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 : 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)
succ₁ : ∀ (hnz : 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)

Tactic:
rcases eq_or_ne p.fr 0 with hz | hnz

Premises used: GenContFract.IntFractPair.fr, eq_or_ne, 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
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
succ₁ succ₂ : Eq.{u_1 + 1} (α := Option (IntFractPair K)) none none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]

Premises used: GenContFract.IntFractPair.stream_eq_none_of_fr_eq_zero
-- 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 : 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⁻¹)
succ₁ succ₂ : some (IntFractPair.of p.fr⁻¹) = some (IntFractPair.of p.fr⁻¹)
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]

Premises used: 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 : Int.fract v ≠ 0
n : ℕ
zero : IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = IntFractPair.stream (Int.fract v)⁻¹ 0
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)
⊢ IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n

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]

Premises used: GenContFract.IntFractPair.stream, Int.fract, Option.none, Inv.inv, GenContFract.IntFractPair.stream_zero, eq_or_ne
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
⊢ (IntFractPair.seq1 v).1 = IntFractPair.of v

Tactic:
rfl

Premises used: GenContFract.IntFractPair.of, 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
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)
⊢ (of v).h = (↑(IntFractPair.seq1 v).1.b : K)

Tactic:
cases aux_seq_eq : IntFractPair.seq1 v

Premises used: GenContFract.IntFractPair.seq1