awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
inst_3 : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_4 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)
i : ι
H :
  Eq (α := Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) 0
    ((Ring.DirectLimit.of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) i :
        (a : G i) → Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
      1)
j : ι
hij : i ≤ j
hf : Eq (α := G j) ((f' i j hij : (a : G i) → G j) 1 : G j) (0 : G j)
⊢ Eq.{u_2 + 1} (α := G j) 1 0

Tactic:
rw [(f' i j hij).map_one] at hf

Premises used: RingHom.map_one
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
inst_3 : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_4 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)
i : ι
H :
  Eq (α := Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) 0
    ((Ring.DirectLimit.of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) i :
        (a : G i) → Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
      1)
j : ι
hij : i ≤ j
hf : Eq.{u_2 + 1} (α := G j) 1 0
⊢ False

Tactic:
one_ne_zero hf

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
inst_3 : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_4 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)
i : ι
H :
  Eq (α := Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) 0
    ((Ring.DirectLimit.of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) i :
        (a : G i) → Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
      1)
j : ι
hij : i ≤ j
hf : Eq.{u_2 + 1} (α := G j) 1 0
⊢ False

Tactic:
exact one_ne_zero hf

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
inst_3 : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
i : ι
x : G i
H :
  Ne (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f) (0 : Ring.DirectLimit G f)
h : x = 0
rw : Eq (α := Ring.DirectLimit G f) ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) 0) 0
rw₁ rw₂ : Eq (α := Ring.DirectLimit G f) 0 0
⊢ Eq (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f) (0 : Ring.DirectLimit G f)

Tactic:
rw [h, (Ring.DirectLimit.of _ _ _).map_zero]

Premises used: Ring.DirectLimit.of, RingHom.map_zero
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
inst_3 : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
i : ι
x : G i
H :
  Ne (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f) (0 : Ring.DirectLimit G f)
rw :
  Eq (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) (x * x⁻¹) : Ring.DirectLimit G f)
    (1 : Ring.DirectLimit G f)
rw₁ : Eq (α := Ring.DirectLimit G f) ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) 1) 1
rw₂ rw₃ : Eq (α := Ring.DirectLimit G f) 1 1
⊢ HMul.hMul (α := Ring.DirectLimit G f) (β := Ring.DirectLimit G f)
      ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f)
      ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x⁻¹ : Ring.DirectLimit G f) =
    1

Tactic:
rw [← (Ring.DirectLimit.of _ _ _).map_mul,
        mul_inv_cancel₀ fun h : x = 0 ↦ H <| by rw [h, (Ring.DirectLimit.of _ _ _).map_zero],
        (Ring.DirectLimit.of _ _ _).map_one]

Premises used: mul_inv_cancel₀, Ring.DirectLimit.of, RingHom.map_one, RingHom.map_mul
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
inst_3 : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
hp : p ≠ 0
rw : (p * if H : p = 0 then 0 else Classical.choose (p := fun (x : Ring.DirectLimit G f) ↦ p * x = 1) ⋯) = 1
rw₁ : p * Classical.choose (p := fun (x : Ring.DirectLimit G f) ↦ p * x = 1) ⋯ = 1
rw₂ rw₃ : Eq (α := Ring.DirectLimit G f) 1 1
⊢ p * inv G f p = 1

Tactic:
rw [inv, dif_neg hp, Classical.choose_spec (DirectLimit.exists_inv G f hp)]

Premises used: Field.DirectLimit.exists_inv, dif_neg, Field.DirectLimit.inv, Classical.choose_spec
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
inst_3 : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
hp : p ≠ 0
rw : p * inv G f p = 1
rw₁ rw₂ : Eq (α := Ring.DirectLimit G f) 1 1
⊢ inv G f p * p = 1

Tactic:
rw [_root_.mul_comm, DirectLimit.mul_inv_cancel G f hp]

Premises used: Field.DirectLimit.mul_inv_cancel, mul_comm
-- Module: Mathlib.Algebra.Colimit.TensorProduct
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
N : Submodule R P
hN : N.FG
x y : TensorProduct.{u_1, u_3, u_2} R (↥N) M
eq :
  Eq (α := P ⊗[R] M) ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
    ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
⊢ N.FG

Tactic:
hN
-- Module: Mathlib.Algebra.Colimit.TensorProduct
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
N : Submodule R P
hN : N.FG
x y : TensorProduct.{u_1, u_3, u_2} R (↥N) M
eq :
  Eq (α := P ⊗[R] M) ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
    ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
lift :
  ∀ (N : { x : Submodule R P // x.FG }) {x y : TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M}
    (eq :
      Eq (α := P ⊗[R] M)
        ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x :
          P ⊗[R] M)
        ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y :
          P ⊗[R] M)),
    ∃ (N' : Submodule R P),
      N'.FG ∧
        ∃ (h : (↑N : Submodule R P) ≤ N'),
          Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
            ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) x :
              TensorProduct.{u_1, u_3, u_2} R (↥N') M)
            ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) y :
              TensorProduct.{u_1, u_3, u_2} R (↥N') M)
⊢ ∃ (N' : Submodule R P),
    N'.FG ∧
      ∃ (h : N ≤ N'),
        Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥N ⊗[R] M) → ↥N' ⊗[R] M) x :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥N ⊗[R] M) → ↥N' ⊗[R] M) y :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)

Tactic:
lift N to {N : Submodule R P // N.FG} using hN

Premises used: Submodule, Submodule.FG
-- Module: Mathlib.Algebra.Colimit.TensorProduct
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
N : { x : Submodule R P // x.FG }
x y : TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M
eq :
  Eq (α := P ⊗[R] M)
    ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
    ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
⊢ Eq (α :=
    TensorProduct.{u_1, u_3, u_2} R
      (Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P)) (Module.fgSystem R P)) M)
    ((LinearMap.rTensor M
            (↑(LinearEquiv.symm (Module.fgSystem.equiv R P)) :
              P →ₗ[R]
                Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                  (Module.fgSystem R P)) :
          (a : P ⊗[R] M) →
            Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                (Module.fgSystem R P) ⊗[R]
              M)
        ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x) :
      TensorProduct.{u_1, u_3, u_2} R
        (Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P)) (Module.fgSystem R P)) M)
    ((LinearMap.rTensor M
            (↑(LinearEquiv.symm (Module.fgSystem.equiv R P)) :
              P →ₗ[R]
                Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                  (Module.fgSystem R P)) :
          (a : P ⊗[R] M) →
            Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                (Module.fgSystem R P) ⊗[R]
              M)
        ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y) :
      TensorProduct.{u_1, u_3, u_2} R
        (Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P)) (Module.fgSystem R P)) M)

Tactic:
apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq

Premises used: LinearEquiv.symm, Module.fgSystem.equiv, LinearEquiv.toLinearMap, LinearMap.rTensor
-- Module: Mathlib.Algebra.ContinuedFractions.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Coe α β
a b : α
⊢ Eq.{u_2 + 1} (α := Pair β) (↑{ a := a, b := b : Pair α } : Pair β) { a := Coe.coe a, b := Coe.coe b }

Tactic:
rfl

Premises used: GenContFract.Pair.coeFn, GenContFract.Pair.map, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Coe α β
g : GenContFract α
⊢ Eq.{u_2 + 1} (α := GenContFract β) (↑g : GenContFract β) { h := Coe.coe g.h, s := Stream'.Seq.map Pair.coeFn g.s }

Tactic:
rfl

Premises used: GenContFract.coeFn, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Basic
Goal:
α : Type u_1
inst : One α
a : α
n : ℕ
aₙ : α
h : (GenContFract.ofInteger a).partNums.get? n = some aₙ
⊢ aₙ = 1

Tactic:
cases h
-- Module: Mathlib.Algebra.ContinuedFractions.Basic
Goal:
α : Type u_1
inst : One α
inst_1 : Zero α
inst_2 : LT α
a : α
n : ℕ
bₙ : α
h : (↑(SimpContFract.ofInteger a) : GenContFract α).partDens.get? n = some bₙ
⊢ 0 < bₙ

Tactic:
cases h
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
⊢ (of v).convs = (of v).convs'

Tactic:
ContFract.convs_eq_convs' (c := ContFract.of v)

Premises used: ContFract.convs_eq_convs', GenContFract.of
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
rw : (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs n
rw₁ : (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs' n = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs n
rw₂ rw₃ : (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs' n = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs' n
⊢ (of v).convs (n + 1) = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs n

Tactic:
rw [of_convs_eq_convs', convs'_succ, of_convs_eq_convs']

Premises used: GenContFract.convs'_succ, GenContFract.of_convs_eq_convs'
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
rcases : ∀ (N' : ℕ) (one_div_ε_lt_N' : 1 / ε < (↑N' : K)), ∃ (N : ℕ), ∀ n ≥ N, |v - (of v).convs n| < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, |v - (of v).convs n| < ε

Tactic:
rcases (exists_nat_gt (1 / ε) : ∃ N' : ℕ, 1 / ε < N') with ⟨N', one_div_ε_lt_N'⟩

Premises used: HDiv.hDiv, exists_nat_gt, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
exists : ∀ n ≥ N, |v - (of v).convs n| < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, |v - (of v).convs n| < ε

Tactic:
exists N
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
inl : ∀ (terminatedAt_n : g.TerminatedAt n), |v - (of v).convs n| < ε
inr : ∀ (not_terminatedAt_n : ¬g.TerminatedAt n), |v - (of v).convs n| < ε
⊢ |v - (of v).convs n| < ε

Tactic:
rcases Decidable.em (g.TerminatedAt n) with terminatedAt_n | not_terminatedAt_n

Premises used: Decidable.em, GenContFract.TerminatedAt
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
⊢ v = g.convs n

Tactic:
have : v = g.convs n := of_correctness_of_terminatedAt terminatedAt_n
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
this : v = g.convs n
⊢ v - g.convs n = 0

Tactic:
have : v - g.convs n = 0 := sub_eq_zero.mpr this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
this_1 : v = g.convs n
this : v - g.convs n = 0
inl : |0| < ε
⊢ |v - (of v).convs n| < ε

Tactic:
rw [this]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
this_1 : v = g.convs n
this : v - g.convs n = 0
⊢ |0| < ε

Tactic:
mod_cast ε_pos

Premises used: Nat.abs_cast, abs, congrArg, cast, GT.gt, LT.lt, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
this_1 : v = g.convs n
this : v - g.convs n = 0
⊢ |0| < ε

Tactic:
exact mod_cast ε_pos
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
⊢ |v - g.convs n| ≤ 1 / (B * nB)

Tactic:
have abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB) :=
      abs_sub_convs_le not_terminatedAt_n
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
inr : 1 / (B * nB) < ε
⊢ |v - (of v).convs n| < ε

Tactic:
suffices 1 / (B * nB) < ε from lt_of_le_of_lt abs_v_sub_conv_le this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
⊢ (↑(fib (n + 2)) : K) ≤ nB

Tactic:
have nB_ineq : (fib (n + 2) : K) ≤ nB :=
      haveI : ¬g.TerminatedAt (n + 1 - 1) := not_terminatedAt_n
      succ_nth_fib_le_of_nth_den (Or.inr this)
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
⊢ (↑(fib (n + 1)) : K) ≤ B

Tactic:
have B_ineq : (fib (n + 1) : K) ≤ B :=
      haveI : ¬g.TerminatedAt (n - 1) := mt (terminated_stable n.pred_le) not_terminatedAt_n
      succ_nth_fib_le_of_nth_den (Or.inr this)
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
⊢ 0 < B

Tactic:
have zero_lt_B : 0 < B := B_ineq.trans_lt' <| mod_cast fib_pos.2 n.succ_pos
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
⊢ 0 < nB

Tactic:
have nB_pos : 0 < nB := nB_ineq.trans_lt' <| mod_cast fib_pos.2 <| succ_pos _
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
⊢ 0 < B * nB

Tactic:
positivity
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
⊢ 0 < B * nB

Tactic:
have zero_lt_mul_conts : 0 < B * nB := by positivity
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
inr : 1 < ε * (B * nB)
⊢ 1 / (B * nB) < ε

Tactic:
suffices 1 < ε * (B * nB) from (div_lt_iff₀ zero_lt_mul_conts).mpr this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ 1 < ε * (↑N' : K)

Tactic:
(div_lt_iff₀' ε_pos).mp one_div_ε_lt_N'

Premises used: div_lt_iff₀', Iff.mp
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ ε * (↑N' : K) ≤ ε * (B * nB)

Tactic:
?_