awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
refine : 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
⊢ |v - (of v).convs n| ≤ 1 / (b * (of v).dens n * (of v).dens n)

Tactic:
refine (abs_sub_convs_le not_terminatedAt_n).trans ?_

Premises used: LE.le.trans, GenContFract.abs_sub_convs_le
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
inl : ∀ (hB : (of v).dens n = 0), 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
inr : ∀ (hB : 0 < (of v).dens n), 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)

Tactic:
rcases (zero_le_of_den (K := K)).eq_or_lt' with
    ((hB : (GenContFract.of v).dens n = 0) | hB)

Premises used: GenContFract.dens, GenContFract.zero_le_of_den, GenContFract.of, LE.le.eq_or_lt'
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : (of v).dens n = 0
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)

Tactic:
simp only [hB, mul_zero, zero_mul, div_zero, le_refl]

Premises used: le_refl, MulZeroClass.zero_mul, MulZeroClass.mul_zero, div_zero
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
inr : 0 < b * (of v).dens n * (of v).dens n
inr₁ : b * (of v).dens n * (of v).dens n ≤ (of v).dens n * (of v).dens (n + 1)
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)

Tactic:
apply one_div_le_one_div_of_le

Premises used: one_div_le_one_div_of_le
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
⊢ 0 < b

Tactic:
have : 0 < b := zero_lt_one.trans_le (of_one_le_get?_partDen nth_partDen_eq)
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
this : 0 < b
⊢ 0 < b * (of v).dens n * (of v).dens n

Tactic:
apply_rules [mul_pos]

Premises used: mul_pos
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
rw : (of v).dens (n + 1) * (of v).dens n
| (of v).dens n * (of v).dens (n + 1)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
inr : b * (of v).dens n * (of v).dens n ≤ (of v).dens (n + 1) * (of v).dens n
⊢ b * (of v).dens n * (of v).dens n ≤ (of v).dens n * (of v).dens (n + 1)

Tactic:
conv_rhs => rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
inr : b * (of v).dens n ≤ (of v).dens (n + 1)
⊢ b * (of v).dens n * (of v).dens n ≤ (of v).dens (n + 1) * (of v).dens n

Tactic:
gcongr
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
⊢ b * (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
le_of_succ_get?_den nth_partDen_eq

Premises used: GenContFract.le_of_succ_get?_den
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
⊢ b * (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
exact le_of_succ_get?_den nth_partDen_eq

Premises used: GenContFract.le_of_succ_get?_den
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
field_simp : (↑⌊a⌋ : K) * b + c + b * Int.fract a = b * a + c
⊢ ((↑⌊a⌋ : K) * b + c) / Int.fract a + b = (b * a + c) / Int.fract a

Tactic:
field_simp
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
rw : (↑⌊a⌋ : K) * b + c + b * (a - (↑⌊a⌋ : K)) = b * a + c
⊢ (↑⌊a⌋ : K) * b + c + b * Int.fract a = b * a + c

Tactic:
rw [Int.fract]

Premises used: Int.fract
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ (↑⌊a⌋ : K) * b + c + b * (a - (↑⌊a⌋ : K)) = b * a + c

Tactic:
ring
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v 0 = some ifp_zero
⊢ IntFractPair.stream v 0 = some (IntFractPair.of v)

Tactic:
have : IntFractPair.stream v 0 = some (IntFractPair.of v) := rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v 0 = some ifp_zero
this : IntFractPair.stream v 0 = some (IntFractPair.of v)
⊢ IntFractPair.of v = ifp_zero

Tactic:
simpa only [this, Option.some.injEq] using stream_zero_eq

Premises used: Option.some.injEq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v 0 = some ifp_zero
zero :
  ∀ (stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)),
    v = compExactValue ((of v).contsAux 0) ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)) (IntFractPair.of v).fr
⊢ v = compExactValue ((of v).contsAux 0) ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)) ifp_zero.fr

Tactic:
obtain rfl : IntFractPair.of v = ifp_zero := by
      have : IntFractPair.stream v 0 = some (IntFractPair.of v) := rfl
      simpa only [this, Option.some.injEq] using stream_zero_eq

Premises used: GenContFract.IntFractPair.of, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
this : v = (↑⌊v⌋ : K)
⊢ v = compExactValue ((of v).contsAux 0) ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)) (IntFractPair.of v).fr

Tactic:
simpa [nextConts, nextNum, nextDen, compExactValue, IntFractPair.of, fract_eq_zero]

Premises used: GenContFract.nextDen, GenContFract.IntFractPair.of, GenContFract.nextConts, GenContFract.compExactValue, GenContFract.nextNum
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
zero : v = (↑⌊v⌋ : K)
⊢ v = compExactValue ((of v).contsAux 0) ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)) (IntFractPair.of v).fr

Tactic:
suffices v = ⌊v⌋ by
        simpa [nextConts, nextNum, nextDen, compExactValue, IntFractPair.of, fract_eq_zero]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
rw rw₁ : v = v
⊢ v = Int.fract v + (↑⌊v⌋ : K)

Tactic:
rw [Int.fract_add_floor]

Premises used: Int.fract_add_floor
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ Int.fract v + (↑⌊v⌋ : K) = (↑⌊v⌋ : K)

Tactic:
simp [fract_eq_zero]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
v₁ : v = Int.fract v + (↑⌊v⌋ : K)
v₂ : Int.fract v + (↑⌊v⌋ : K) = (↑⌊v⌋ : K)
⊢ v = (↑⌊v⌋ : K)

Tactic:
calc
        v = Int.fract v + ⌊v⌋ := by rw [Int.fract_add_floor]
        _ = ⌊v⌋ := by simp [fract_eq_zero]

Premises used: Int.fract
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_ne_zero : Int.fract v ≠ 0
⊢ v = compExactValue ((of v).contsAux 0) ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)) (IntFractPair.of v).fr

Tactic:
simp [field, contsAux, nextConts, nextNum, nextDen, of_h_eq_floor, compExactValue,
        IntFractPair.of, fract_ne_zero]

Premises used: GenContFract.contsAux, GenContFract.nextDen, GenContFract.IntFractPair.of, GenContFract.nextConts, GenContFract.of_h_eq_floor, GenContFract.compExactValue, GenContFract.nextNum
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
⊢ Int.fract v = 0 ∨ Int.fract v ≠ 0

Tactic:
cases eq_or_ne (Int.fract v) 0 with
    | inl fract_eq_zero =>
      -- Int.fract v = 0; we must then have `v = ⌊v⌋`
      suffices v = ⌊v⌋ by
        simpa [nextConts, nextNum, nextDen, compExactValue, IntFractPair.of, fract_eq_zero]
      calc
        v = Int.fract v + ⌊v⌋ := by rw [Int.fract_add_floor]
        _ = ⌊v⌋ := by simp [fract_eq_zero]
    | inr fract_ne_zero =>
      -- Int.fract v ≠ 0; the claim then easily follows by unfolding a single computation step
      simp [field, contsAux, nextConts, nextNum, nextDen, of_h_eq_floor, compExactValue,
        IntFractPair.of, fract_ne_zero]

Premises used: GenContFract.contsAux, GenContFract.nextDen, Int.fract, GenContFract.IntFractPair.of, GenContFract.nextConts, eq_or_ne, GenContFract.of_h_eq_floor, OfNat.ofNat, GenContFract.compExactValue, GenContFract.nextNum
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) ((of v).contsAux (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : 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:
IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq

Premises used: Iff.mp, GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) ((of v).contsAux (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
succ :
  ∀ (ifp_n : IntFractPair K) (nth_stream_eq : IntFractPair.stream v n = some ifp_n) (nth_fract_ne_zero : ifp_n.fr ≠ 0),
    v = compExactValue ((of v).contsAux (n + 1)) ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr
⊢ v = compExactValue ((of v).contsAux (n + 1)) ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
obtain ⟨ifp_n, nth_stream_eq, nth_fract_ne_zero, -⟩ :
      ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧
        ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
      IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq

Premises used: GenContFract.IntFractPair.stream, Iff.mp, GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) ((of v).contsAux (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
succ :
  let pconts := g.contsAux (n + 1);
  ∀
    (IH :
      ∀ {ifp_n : IntFractPair K},
        IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) pconts ifp_n.fr)
    (pconts_eq : pconts = g.contsAux (n + 1)), v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr
⊢ v = compExactValue ((of v).contsAux (n + 1)) ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
set pconts := g.contsAux (n + 1) with pconts_eq

Premises used: GenContFract.contsAux, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) pconts ifp_n.fr
pconts_eq : pconts = g.contsAux (n + 1)
⊢ let ppconts := g.contsAux n;
  ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr

Tactic:
set ppconts := g.contsAux n with ppconts_eq

Premises used: GenContFract.contsAux
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) pconts ifp_n.fr
pconts_eq : pconts = g.contsAux (n + 1)
IH₁ :
  let ppconts := g.contsAux n;
  ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
⊢ let ppconts := g.contsAux n;
  ppconts = g.contsAux n

Tactic:
set ppconts := g.contsAux n with ppconts_eq

Premises used: GenContFract.contsAux
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
this : v = conts.a / conts.b
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
simpa [compExactValue, ifp_succ_n_fr_eq_zero]

Premises used: GenContFract.compExactValue
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
succ : v = conts.a / conts.b
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
suffices v = conts.a / conts.b by simpa [compExactValue, ifp_succ_n_fr_eq_zero]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_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)

Tactic:
IntFractPair.exists_succ_nth_stream_of_fr_zero succ_nth_stream_eq ifp_succ_n_fr_eq_zero

Premises used: GenContFract.IntFractPair.exists_succ_nth_stream_of_fr_zero
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
succ :
  ∀ (ifp_n' : IntFractPair K) (nth_stream_eq' : IntFractPair.stream v n = some ifp_n')
    (ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = (↑⌊ifp_n'.fr⁻¹⌋ : K)), v = conts.a / conts.b
⊢ v = conts.a / conts.b

Tactic:
obtain ⟨ifp_n', nth_stream_eq', ifp_n_fract_inv_eq_floor⟩ :
          ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋ :=
        IntFractPair.exists_succ_nth_stream_of_fr_zero succ_nth_stream_eq ifp_succ_n_fr_eq_zero

Premises used: GenContFract.IntFractPair.stream, Option.some, GenContFract.IntFractPair.fr, GenContFract.IntFractPair.exists_succ_nth_stream_of_fr_zero
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = (↑⌊ifp_n'.fr⁻¹⌋ : K)
⊢ ifp_n' = ifp_n

Tactic:
injection Eq.trans nth_stream_eq'.symm nth_stream_eq

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = (↑⌊ifp_n'.fr⁻¹⌋ : K)
⊢ ifp_n' = ifp_n

Tactic:
have : ifp_n' = ifp_n := by injection Eq.trans nth_stream_eq'.symm nth_stream_eq