awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
q : ℚ≥0
simp_rw : ofRat (↑q : β) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
simp_rw₁ :
  ofRat (HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
simp_rw₂ :
  HDiv.hDiv (α := Cauchy abv) (ofRat (↑q.num : β)) (ofRat (↑q.den : β)) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
⊢ (↑q : Cauchy abv) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)

Tactic:
simp_rw [← ofRat_nnratCast, NNRat.cast_def, ofRat_div, ofRat_natCast]

Premises used: CauSeq.Completion.ofRat_div, NNRat.cast_def, CauSeq.Completion.ofRat_nnratCast, CauSeq.Completion.ofRat_natCast
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
q : ℚ
rw : ofRat (↑q : β) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
rw₁ :
  ofRat (HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
rw₂ :
  HDiv.hDiv (α := Cauchy abv) (ofRat (↑q.num : β)) (ofRat (↑q.den : β)) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
rw₃ :
  HDiv.hDiv (α := Cauchy abv) (ofRat (↑q.num : β)) (↑q.den : Cauchy abv) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
rw₄ rw₅ :
  HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
⊢ (↑q : Cauchy abv) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)

Tactic:
rw [← ofRat_ratCast, Rat.cast_def, ofRat_div, ofRat_natCast, ofRat_intCast]

Premises used: CauSeq.Completion.ofRat_div, CauSeq.Completion.ofRat_ratCast, Rat.cast_def, CauSeq.Completion.ofRat_intCast, CauSeq.Completion.ofRat_natCast
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
⊢ ∀ (s : CauSeq β abv), ∃ (b : β), s ≈ const abv b

Tactic:
IsComplete.isComplete

Premises used: CauSeq.IsComplete.isComplete
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
s : CauSeq β abv
⊢ s ≈ const abv s.lim

Tactic:
Classical.choose_spec (complete s)

Premises used: Classical.choose_spec, CauSeq.lim, CauSeq.complete
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
x : β
h : const abv x ≈ f
⊢ x = f.lim

Tactic:
const_equiv.mp <| Setoid.trans h <| equiv_lim f

Premises used: CauSeq.equiv_lim, CauSeq.const_equiv, Iff.mp, Setoid.trans
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
x : β
h : f ≈ const abv x
⊢ f.lim = x

Tactic:
(eq_lim_of_const_equiv <| Setoid.symm h).symm

Premises used: Setoid.symm, Eq.symm, CauSeq.eq_lim_of_const_equiv
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
h : f ≈ g
⊢ f.lim = g.lim

Tactic:
lim_eq_of_equiv_const <| Setoid.trans h <| equiv_lim g

Premises used: CauSeq.equiv_lim, CauSeq.lim_eq_of_equiv_const, Setoid.trans
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
x : β
⊢ lim (const abv x) = x

Tactic:
lim_eq_of_equiv_const <| Setoid.refl _

Premises used: CauSeq.lim_eq_of_equiv_const, Setoid.refl
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
rw : (const abv f.lim - f + (const abv g.lim - g)).LimZero
⊢ (const abv (f.lim + g.lim) - (f + g)).LimZero

Tactic:
rw [const_add, add_sub_add_comm]

Premises used: CauSeq.const_add, add_sub_add_comm
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
⊢ (const abv f.lim - f + (const abv g.lim - g)).LimZero

Tactic:
add_limZero (Setoid.symm (equiv_lim f)) (Setoid.symm (equiv_lim g))

Premises used: CauSeq.equiv_lim, Setoid.symm, CauSeq.add_limZero
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
⊢ (const abv f.lim - f + (const abv g.lim - g)).LimZero

Tactic:
exact add_limZero (Setoid.symm (equiv_lim f)) (Setoid.symm (equiv_lim g))

Premises used: CauSeq.equiv_lim, Setoid.symm, CauSeq.add_limZero
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
a :
  (↑(const abv (f.lim * g.lim) - f * g) : ℕ → β) =
    (↑((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)) : ℕ → β)
⊢ const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
a :
  (↑(const abv (f.lim * g.lim) - f * g) : ℕ → β) =
    (↑((const abv f.lim - f) * g) : ℕ → β) + (↑(const abv f.lim * (const abv g.lim - g)) : ℕ → β)
⊢ (↑(const abv (f.lim * g.lim) - f * g) : ℕ → β) =
    (↑((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)) : ℕ → β)

Tactic:
rw [coe_add]

Premises used: CauSeq.coe_add
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
⊢ (↑(const abv (f.lim * g.lim) - f * g) : ℕ → β) =
    (↑((const abv f.lim - f) * g) : ℕ → β) + (↑(const abv f.lim * (const abv g.lim - g)) : ℕ → β)

Tactic:
simp [sub_mul, mul_sub]

Premises used: mul_sub, sub_mul
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
⊢ const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)

Tactic:
have h :
        const abv (lim f * lim g) - f * g =
          (const abv (lim f) - f) * g + const abv (lim f) * (const abv (lim g) - g) := by
              apply Subtype.ext
              rw [coe_add]
              simp [sub_mul, mul_sub]
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
rw : ((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)).LimZero
⊢ (const abv (f.lim * g.lim) - f * g).LimZero

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
⊢ ((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)).LimZero

Tactic:
add_limZero (mul_limZero_left _ (Setoid.symm (equiv_lim _)))
          (mul_limZero_right _ (Setoid.symm (equiv_lim _)))

Premises used: CauSeq.equiv_lim, CauSeq.mul_limZero_right, Setoid.symm, CauSeq.mul_limZero_left, CauSeq.add_limZero
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
⊢ ((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)).LimZero

Tactic:
exact
        add_limZero (mul_limZero_left _ (Setoid.symm (equiv_lim _)))
          (mul_limZero_right _ (Setoid.symm (equiv_lim _)))

Premises used: CauSeq.equiv_lim, CauSeq.mul_limZero_right, Setoid.symm, CauSeq.mul_limZero_left, CauSeq.add_limZero
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
x : β
rw : f.lim * x = f.lim * lim (const abv x)
rw₁ rw₂ : f.lim * x = f.lim * x
⊢ f.lim * x = (f * const abv x).lim

Tactic:
rw [← lim_mul_lim, lim_const]

Premises used: CauSeq.lim_const, CauSeq.lim_mul_lim
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
rw : (const abv f.lim - f).LimZero
⊢ (-f - const abv (-f.lim)).LimZero

Tactic:
rw [const_neg, sub_neg_eq_add, add_comm, ← sub_eq_add_neg]

Premises used: CauSeq.const_neg, sub_eq_add_neg, add_comm, sub_neg_eq_add
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
⊢ (const abv f.lim - f).LimZero

Tactic:
Setoid.symm (equiv_lim f)

Premises used: CauSeq.equiv_lim, Setoid.symm
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
⊢ (const abv f.lim - f).LimZero

Tactic:
exact Setoid.symm (equiv_lim f)

Premises used: CauSeq.equiv_lim, Setoid.symm
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
rw : f.lim + -g.lim = (f - g).lim
rw₁ : f.lim + -g.lim = (f + -g).lim
rw₂ : f.lim + (-g).lim = (f + -g).lim
rw₃ rw₄ : (f + -g).lim = (f + -g).lim
⊢ f.lim - g.lim = (f - g).lim

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, ← lim_neg, lim_add f (-g)]

Premises used: sub_eq_add_neg, CauSeq.lim_add, CauSeq.lim_neg, Neg.neg
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
⊢ f ≈ const abv f.lim

Tactic:
have hf := equiv_lim f
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv f.lim
⊢ f ≈ const abv 0

Tactic:
rw [h] at hf
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv 0
⊢ f.LimZero

Tactic:
(limZero_congr hf).mpr (const_limZero.mpr rfl)

Premises used: Iff.mpr, CauSeq.limZero_congr, CauSeq.const_limZero, rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv 0
⊢ f.LimZero

Tactic:
exact (limZero_congr hf).mpr (const_limZero.mpr rfl)

Premises used: Iff.mpr, CauSeq.limZero_congr, CauSeq.const_limZero, rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
n : ℕ
⊢ (↑f : ℕ → β) n = (↑(f - const abv 0) : ℕ → β) n

Tactic:
simp
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
⊢ f = f - const abv 0

Tactic:
have h₁ : f = f - const abv 0 := ext fun n => by simp
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
h : (f - const abv 0).LimZero
h₁ : f = f - const abv 0
⊢ f.lim = 0

Tactic:
exact lim_eq_of_equiv_const h

Premises used: CauSeq.lim_eq_of_equiv_const
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
rwa rwa₁ rwa₂ rwa₃ : ∀ (hf : ¬f.lim = 0), f.lim ≠ 0
⊢ f.lim ≠ 0

Tactic:
rwa [← lim_eq_zero_iff] at hf

Premises used: CauSeq.lim_eq_zero_iff
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
rw rw₁ : g - f * f.inv hf * g = g - f * f.inv hf * g
⊢ g - f * f.inv hf * g = 1 * g - f * f.inv hf * g

Tactic:
rw [one_mul g]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
⊢ g - f * f.inv hf * g = 1 * g - f * f.inv hf * g

Tactic:
have h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g := by rw [one_mul g]
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
⊢ f * f.inv hf * g = f * f.inv hf * g

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
⊢ f * f.inv hf * g = f * f.inv hf * g

Tactic:
have h₃ : f * inv f hf * g = (f * inv f hf) * g := by simp [mul_assoc]
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
rw rw₁ : 1 * g - f * f.inv hf * g = (1 - f * f.inv hf) * g
rw₂ rw₃ : (1 - f * f.inv hf) * g = (1 - f * f.inv hf) * g
⊢ g - f * f.inv hf * g = (1 - f * f.inv hf) * g

Tactic:
rw [h₂, h₃, ← sub_mul]

Premises used: sub_mul
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
⊢ g - f * f.inv hf * g = (1 - f * f.inv hf) * g

Tactic:
have h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g := by rw [h₂, h₃, ← sub_mul]
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
rw : (1 - f * f.inv hf) * g = g * (1 - f * f.inv hf)
rw₁ rw₂ : g * (1 - f * f.inv hf) = g * (1 - f * f.inv hf)
⊢ g - f * f.inv hf * g = g * (1 - f * f.inv hf)

Tactic:
rw [h₄, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
⊢ g - f * f.inv hf * g = g * (1 - f * f.inv hf)

Tactic:
have h₅ : g - f * inv f hf * g = g * (1 - f * inv f hf) := by rw [h₄, mul_comm]
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
rw : g * (1 - f * f.inv hf) = g * (1 - f.inv hf * f)
rw₁ rw₂ : g * (1 - f.inv hf * f) = g * (1 - f.inv hf * f)
⊢ g - f * f.inv hf * g = g * (1 - f.inv hf * f)

Tactic:
rw [h₅, mul_comm f]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
⊢ g - f * f.inv hf * g = g * (1 - f.inv hf * f)

Tactic:
have h₆ : g - f * inv f hf * g = g * (1 - inv f hf * f) := by rw [h₅, mul_comm f]
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
h₆ : g - f * f.inv hf * g = g * (1 - f.inv hf * f)
rw : (g * (1 - f.inv hf * f)).LimZero
⊢ (g - f * f.inv hf * g).LimZero

Tactic:
rw [h₆]
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
h₆ : g - f * f.inv hf * g = g * (1 - f.inv hf * f)
⊢ (g * (1 - f.inv hf * f)).LimZero

Tactic:
mul_limZero_right _ (Setoid.symm (CauSeq.inv_mul_cancel _))

Premises used: CauSeq.inv_mul_cancel, CauSeq.mul_limZero_right, Setoid.symm
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
h₆ : g - f * f.inv hf * g = g * (1 - f.inv hf * f)
⊢ (g * (1 - f.inv hf * f)).LimZero

Tactic:
exact mul_limZero_right _ (Setoid.symm (CauSeq.inv_mul_cancel _))

Premises used: CauSeq.inv_mul_cancel, CauSeq.mul_limZero_right, Setoid.symm
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
rw :
  (f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹) -
      (const abv f.lim⁻¹ - f * (f.inv hf * const abv f.lim⁻¹))).LimZero
⊢ (f.inv hf - const abv f.lim⁻¹ - (const abv f.lim - f) * (f.inv hf * const abv f.lim⁻¹)).LimZero

Tactic:
rw [sub_mul, ← sub_add, sub_sub, sub_add_eq_sub_sub, sub_right_comm, sub_add]

Premises used: sub_add, sub_right_comm, sub_mul, sub_sub, sub_add_eq_sub_sub