awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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 * (of v).dens n * (of v).dens n
have this : 0 < b
Tactic: have : 0 < b := zero_lt_one.trans_le (of_one_le_get?_partDen nth_partDen_eq)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
| (of v).dens n * (of v).dens (n + 1)
have rw : (of v).dens (n + 1) * (of v).dens n
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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 ≤ (of v).dens n * (of v).dens (n + 1)
have inr : b * (of v).dens n * (of v).dens n ≤ (of v).dens (n + 1) * (of v).dens n
Tactic: conv_rhs => rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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 ≤ (of v).dens (n + 1) * (of v).dens n
have inr : b * (of v).dens n ≤ (of v).dens (n + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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) / Int.fract a + b = (b * a + c) / Int.fract a
have field_simp : (↑⌊a⌋ : K) * b + c + b * Int.fract a = b * a + c
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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 * Int.fract a = b * a + c
have rw : (↑⌊a⌋ : K) * b + c + b * (a - (↑⌊a⌋ : K)) = b * a + c
Tactic: rw [Int.fract]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
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.of v = ifp_zero
have this : IntFractPair.stream v 0 = some (IntFractPair.of v)
Tactic: have : IntFractPair.stream v 0 = some (IntFractPair.of v) := rfl
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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
⊢ v = compExactValue ((of v).contsAux 0) ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)) ifp_zero.fr
have 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
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
Cleared hypotheses: ifp_zero, stream_zero_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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 = compExactValue ((of v).contsAux 0) ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)) (IntFractPair.of v).fr
have zero : v = (↑⌊v⌋ : K)
Tactic: suffices v = ⌊v⌋ by
        simpa [nextConts, nextNum, nextDen, compExactValue, IntFractPair.of, fract_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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 = Int.fract v + (↑⌊v⌋ : K)
have rw : v = v
Tactic: rw [Int.fract_add_floor]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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⌋ : K)
have v₁ : v = Int.fract v + (↑⌊v⌋ : K)
Tactic: calc
        v = Int.fract v + ⌊v⌋ := by rw [Int.fract_add_floor]
        _ = ⌊v⌋ := by simp [fract_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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 = (↑⌊v⌋ : K)
have v₂ : Int.fract v + (↑⌊v⌋ : K) = (↑⌊v⌋ : K)
Tactic: calc
        v = Int.fract v + ⌊v⌋ := by rw [Int.fract_add_floor]
        _ = ⌊v⌋ := by simp [fract_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
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)
⊢ v = compExactValue ((of v).contsAux 0) ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)) (IntFractPair.of v).fr
have x : 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]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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
⊢ v = compExactValue ((of v).contsAux (n + 1)) ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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)
⊢ v = compExactValue ((of v).contsAux (n + 1)) ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr
have 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
Tactic: set pconts := g.contsAux (n + 1) with pconts_eq
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
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
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr
have ppconts_eq : let ppconts := g.contsAux n;
ppconts = g.contsAux n
Tactic: set ppconts := g.contsAux n with ppconts_eq
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr
have succ : v = conts.a / conts.b
Tactic: suffices v = conts.a / conts.b by simpa [compExactValue, ifp_succ_n_fr_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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
⊢ v = conts.a / conts.b
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
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)
⊢ v = conts.a / conts.b
have this : ifp_n' = ifp_n
Tactic: have : ifp_n' = ifp_n := by injection Eq.trans nth_stream_eq'.symm nth_stream_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
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)
this : ifp_n' = ifp_n
nth_stream_eq'₁ : IntFractPair.stream v n = some ifp_n
⊢ v = conts.a / conts.b
have ifp_n_fract_inv_eq_floor₁ : ifp_n.fr⁻¹ = (↑⌊ifp_n.fr⁻¹⌋ : K)
Tactic: cases this
Cleared hypotheses: ifp_n', nth_stream_eq', ifp_n_fract_inv_eq_floor, this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
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
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
have s_nth_eq : g.s.get? n = some { a := 1, b := (↑⌊ifp_n.fr⁻¹⌋ : K) }
Tactic: have s_nth_eq : g.s.get? n = some ⟨1, ⌊ifp_n.fr⁻¹⌋⟩ :=
        get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero nth_stream_eq nth_fract_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
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
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = (↑⌊ifp_n.fr⁻¹⌋ : K)
s_nth_eq : g.s.get? n = some { a := 1, b := (↑⌊ifp_n.fr⁻¹⌋ : K) }
⊢ v = conts.a / conts.b
have s_nth_eq₁ : g.s.get? n = some { a := 1, b := ifp_n.fr⁻¹ }
Tactic: rw [← ifp_n_fract_inv_eq_floor] at s_nth_eq
Cleared hypotheses: s_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = (↑⌊ifp_n.fr⁻¹⌋ : K)
s_nth_eq : g.s.get? n = some { a := 1, b := ifp_n.fr⁻¹ }
⊢ v = conts.a / conts.b
have succ : v = compExactValue ppconts pconts ifp_n.fr
Tactic: suffices v = compExactValue ppconts pconts ifp_n.fr by
        simpa [conts, contsAux, s_nth_eq, compExactValue, nth_fract_ne_zero] using this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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_ne_zero : ifp_succ_n.fr ≠ 0
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr
have succ : compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
Tactic: suffices
        compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr by grind
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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_ne_zero : ifp_succ_n.fr ≠ 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
have succ : ∀ (ifp_n' : IntFractPair K) (nth_stream_eq' : IntFractPair.stream v n = some ifp_n')
  (ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0)
  (succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n'.fr⁻¹))
  (ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n'.fr⁻¹).fr ≠ 0),
  compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n'.fr⁻¹).fr
Tactic: obtain ⟨ifp_n', nth_stream_eq', ifp_n_fract_ne_zero, ⟨refl⟩⟩ :
        ∃ 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
Cleared hypotheses: ifp_succ_n, succ_nth_stream_eq, ifp_succ_n_fr_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
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_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_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n'.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n'.fr⁻¹).fr ≠ 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n'.fr⁻¹).fr
have this : ifp_n' = ifp_n
Tactic: have : ifp_n' = ifp_n := by injection Eq.trans nth_stream_eq'.symm nth_stream_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
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_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_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n'.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n'.fr⁻¹).fr ≠ 0
this : ifp_n' = ifp_n
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n'.fr⁻¹).fr
have succ : ∀ (nth_stream_eq' : IntFractPair.stream v n = some ifp_n) (ifp_n_fract_ne_zero : ifp_n.fr ≠ 0)
  (succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹))
  (ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0),
  compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
Tactic: cases this
Cleared hypotheses: ifp_n', nth_stream_eq', ifp_n_fract_ne_zero, succ_nth_stream_eq, ifp_succ_n_fr_ne_zero, this