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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : CauSeq β abv
this : Eq (α := Cauchy abv) (mk f) 0 ↔ (f - 0).LimZero
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Eq (α := Cauchy abv) (mk f) 0 ↔ f.LimZero), Eq (α := Cauchy abv) (mk f) 0 ↔ f.LimZero
⊢ Eq (α := Cauchy abv) (mk f) 0 ↔ f.LimZero

Tactic:
rwa [sub_zero] at this

Premises used: sub_zero
-- 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
f g : CauSeq β abv
⊢ HAdd.hAdd (α := Cauchy abv) (mk f) (mk g) = mk (f + g)

Tactic:
rfl

Premises used: Quotient.map₂, CauSeq.Completion.mk, 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
f : CauSeq β abv
⊢ Eq (α := Cauchy abv) (-mk f) (mk (-f))

Tactic:
rfl

Premises used: Quotient.map, CauSeq.Completion.mk, Quot.map, 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
f g : CauSeq β abv
⊢ HMul.hMul (α := Cauchy abv) (mk f) (mk g) = mk (f * g)

Tactic:
rfl

Premises used: Quotient.map₂, CauSeq.Completion.mk, 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
f g : CauSeq β abv
⊢ HSub.hSub (α := Cauchy abv) (mk f) (mk g) = mk (f - g)

Tactic:
rfl

Premises used: Quotient.map₂, CauSeq.Completion.mk, 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
γ : Type u_3
inst_5 : SMul γ β
inst_6 : IsScalarTower γ β β
c : γ
f : CauSeq β abv
⊢ HSMul.hSMul (β := Cauchy abv) c (mk f) = mk (c • f)

Tactic:
rfl

Premises used: Quotient.map, CauSeq.Completion.mk, Quot.map, 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
n : ℕ
f : CauSeq β abv
⊢ HPow.hPow (α := Cauchy abv) (mk f) n = mk (f ^ n)

Tactic:
rfl

Premises used: Quotient.map, CauSeq.Completion.mk, Quot.map, 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
n : ℕ
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (ofRat (↑n : β)) (↑n : Cauchy abv)

Tactic:
rfl

Premises used: CauSeq.Completion.ofRat, 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
z : ℤ
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (ofRat (↑z : β)) (↑z : Cauchy abv)

Tactic:
rfl

Premises used: CauSeq.Completion.ofRat, 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
x y : β
⊢ ofRat (x + y) = HAdd.hAdd (α := Cauchy abv) (ofRat x) (ofRat y)

Tactic:
congr_arg mk (const_add _ _)

Premises used: CauSeq.const_add, CauSeq.Completion.ofRat, Quotient.map₂, CauSeq.Completion.mk, congr_arg
-- 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
x : β
⊢ Eq (α := Cauchy abv) (ofRat (-x)) (-ofRat x)

Tactic:
congr_arg mk (const_neg _)

Premises used: CauSeq.const_neg, Quotient.map, CauSeq.Completion.ofRat, CauSeq.Completion.mk, congr_arg, Quot.map
-- 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
x y : β
⊢ ofRat (x * y) = HMul.hMul (α := Cauchy abv) (ofRat x) (ofRat y)

Tactic:
congr_arg mk (const_mul _ _)

Premises used: CauSeq.Completion.ofRat, Quotient.map₂, CauSeq.Completion.mk, CauSeq.const_mul, congr_arg
-- 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
x y : β
h : Eq (α := Cauchy abv) (ofRat x) (ofRat y)
⊢ x = y

Tactic:
simpa [ofRat, mk_eq, ← const_sub, const_limZero, sub_eq_zero] using h

Premises used: sub_eq_zero, CauSeq.Completion.ofRat, CauSeq.const_limZero, CauSeq.const_sub, CauSeq.Completion.mk_eq
-- 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
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (mk 0) 0

Tactic:
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
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (mk 1) 1

Tactic:
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
x y : β
⊢ ofRat (x - y) = HSub.hSub (α := Cauchy abv) (ofRat x) (ofRat y)

Tactic:
congr_arg mk (const_sub _ _)

Premises used: CauSeq.Completion.ofRat, Quotient.map₂, CauSeq.Completion.mk, congr_arg, CauSeq.const_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 : Nontrivial β
⊢ Nontrivial.{u_2} (Cauchy abv)

Tactic:
ofRat_injective.nontrivial

Premises used: Function.Injective.nontrivial, CauSeq.Completion.ofRat_injective
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : CommRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (mk 0) 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : CommRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (mk 1) 1

Tactic:
rfl
-- 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
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (ofRat (↑q : β)) (↑q : Cauchy abv)

Tactic:
rfl

Premises used: rfl
-- 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 : ℚ
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (ofRat (↑q : β)) (↑q : Cauchy abv)

Tactic:
rfl

Premises used: rfl
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
⊢ f.LimZero ↔ g.LimZero

Tactic:
have := limZero_congr fg
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
pos :
  ∀ (hf : f.LimZero),
    Eq.{u_2 + 1} (α := Cauchy abv) (mk (if h : f.LimZero then 0 else f.inv h))
      (mk (if h : g.LimZero then 0 else g.inv h))
neg :
  ∀ (hf : ¬f.LimZero),
    Eq.{u_2 + 1} (α := Cauchy abv) (mk (if h : f.LimZero then 0 else f.inv h))
      (mk (if h : g.LimZero then 0 else g.inv h))
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (mk (if h : f.LimZero then 0 else f.inv h)) (mk (if h : g.LimZero then 0 else g.inv h))

Tactic:
by_cases hf : LimZero f

Premises used: CauSeq.LimZero
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : f.LimZero
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (mk (if h : f.LimZero then 0 else f.inv h)) (mk (if h : g.LimZero then 0 else g.inv h))

Tactic:
simp [hf, this.1 hf]

Premises used: Iff.mp
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
⊢ ¬g.LimZero

Tactic:
have hg := mt this.2 hf
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
neg : Eq (α := Cauchy abv) (mk (f.inv ⋯)) (mk (g.inv ⋯))
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (mk (if h : f.LimZero then 0 else f.inv h)) (mk (if h : g.LimZero then 0 else g.inv h))

Tactic:
simp only [hf, dite_false, hg]

Premises used: dite_false
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
⊢ HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) (mk f) = 1

Tactic:
have If : mk (inv f hf) * mk f = 1 := mk_eq.2 (inv_mul_cancel hf)
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) (mk f) = 1
⊢ HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g) = 1

Tactic:
have Ig : mk (inv g hg) * mk g = 1 := mk_eq.2 (inv_mul_cancel hg)
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) (mk f) = 1
Ig : HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g) = 1
⊢ HMul.hMul (α := Cauchy abv) (mk g) (mk (g.inv hg)) = 1

Tactic:
have Ig' : mk g * mk (inv g hg) = 1 := mk_eq.2 (mul_inv_cancel hg)
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) (mk f) = 1
Ig : HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g) = 1
Ig' : HMul.hMul (α := Cauchy abv) (mk g) (mk (g.inv hg)) = 1
⊢ HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) (mk g) = HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g)

Tactic:
rw [mk_eq.2 fg, ← Ig] at If

Premises used: Iff.mpr, CauSeq.Completion.mk_eq
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) (mk f) = 1
Ig : HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g) = 1
Ig' : HMul.hMul (α := Cauchy abv) (mk g) (mk (g.inv hg)) = 1
If₁ : HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) (mk g) = HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g)
⊢ HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g) = 1

Tactic:
rw [mk_eq.2 fg, ← Ig] at If

Premises used: Iff.mpr, CauSeq.Completion.mk_eq
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) (mk f) = 1
Ig : HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g) = 1
Ig' : HMul.hMul (α := Cauchy abv) (mk g) (mk (g.inv hg)) = 1
If₁ : HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) (mk g) = HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g)
Ig₁ : HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g) = 1
⊢ HMul.hMul (α := Cauchy abv) (mk g) (mk (g.inv hg)) = 1

Tactic:
rw [mk_eq.2 fg, ← Ig] at If

Premises used: Iff.mpr, CauSeq.Completion.mk_eq
-- 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
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) (mk g) = HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g)
Ig : HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g) = 1
Ig' : HMul.hMul (α := Cauchy abv) (mk g) (mk (g.inv hg)) = 1
neg : HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) 1 = mk (g.inv ⋯)
neg₁ : mk (f.inv hf) * HMul.hMul (α := Cauchy abv) (mk g) (mk (g.inv hg)) = mk (g.inv ⋯)
neg₂ : HMul.hMul (α := Cauchy abv) (mk (f.inv hf)) (mk g) * mk (g.inv hg) = mk (g.inv ⋯)
neg₃ : HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) (mk g) * mk (g.inv hg) = mk (g.inv ⋯)
neg₄ : mk (g.inv hg) * HMul.hMul (α := Cauchy abv) (mk g) (mk (g.inv hg)) = mk (g.inv ⋯)
neg₅ : HMul.hMul (α := Cauchy abv) (mk (g.inv hg)) 1 = mk (g.inv ⋯)
neg₆ neg₇ : Eq (α := Cauchy abv) (mk (g.inv hg)) (mk (g.inv ⋯))
⊢ Eq (α := Cauchy abv) (mk (f.inv ⋯)) (mk (g.inv ⋯))

Tactic:
rw [← mul_one (mk (inv f hf)), ← Ig', ← mul_assoc, If, mul_assoc, Ig', mul_one]

Premises used: CauSeq.inv, mul_assoc, CauSeq.Completion.mk, mul_one
-- 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
rw : Eq (α := CauSeq β abv) 0 (const abv 0)
hc : LimZero (const abv 0)
⊢ Eq (α := CauSeq β abv) (if h : LimZero (const abv 0) then 0 else inv (const abv 0) h) (const abv 0)

Tactic:
rw [dif_pos]

Premises used: dif_pos
-- 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
⊢ Eq (α := CauSeq β abv) 0 (const abv 0)

Tactic:
rfl
-- 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
⊢ LimZero (const abv 0)

Tactic:
zero_limZero

Premises used: CauSeq.zero_limZero
-- 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
⊢ LimZero (const abv 0)

Tactic:
exact zero_limZero

Premises used: CauSeq.zero_limZero
-- 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
rw : Eq (α := CauSeq β abv) 0 (const abv 0)
hc : LimZero (const abv 0)
rw₁ : Eq (α := CauSeq β abv) 0 (const abv 0)
hc₁ : LimZero (const abv 0)
rw₂ : Eq (α := CauSeq β abv) 0 (const abv 0)
hc₂ : LimZero (const abv 0)
rw₃ : Eq (α := CauSeq β abv) 0 (const abv 0)
hc₃ : LimZero (const abv 0)
⊢ Eq (α := CauSeq β abv) (if h : LimZero (const abv 0) then 0 else inv (const abv 0) h) (const abv 0)

Tactic:
rw [dif_pos] <;> [rfl; exact zero_limZero]

Premises used: dif_pos, CauSeq.zero_limZero
-- 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
f : CauSeq β abv
hf : ¬f.LimZero
rw : f.inv hf = f.inv hf
hnc : ¬f.LimZero
rw₁ : f.inv hf = f.inv hf
hnc₁ : ¬f.LimZero
⊢ (if h : f.LimZero then 0 else f.inv h) = f.inv hf

Tactic:
rw [dif_neg]

Premises used: dif_neg
-- 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
h : HasEquiv.Equiv.{u_2 + 1, 0} (α := CauSeq β abv) 0 1
this : (HSub.hSub (α := CauSeq β abv) 1 0).LimZero
⊢ LimZero.{u_1, u_2} (α := α) (β := β) (abv := abv) 1

Tactic:
simpa
-- 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
⊢ Ne.{u_2 + 1} (α := Cauchy abv) 0 1

Tactic:
fun h => cau_seq_zero_ne_one <| mk_eq.1 h

Premises used: CauSeq.Completion.cau_seq_zero_ne_one, Iff.mp, CauSeq.Completion.mk_eq, Not
-- 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
x : Cauchy abv
f : CauSeq β abv
hf : Ne (α := Cauchy abv) ⟦f⟧ 0
⊢ ¬f.LimZero

Tactic:
simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf

Premises used: ne_eq, CauSeq.Completion.mk_eq_mk, CauSeq.Completion.mk_eq_zero
-- 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
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
simp : Eq (α := Cauchy abv) (mk (f.inv ⋯ * f)) 1
⊢ HMul.hMul (α := Cauchy abv) (⟦f⟧)⁻¹ ⟦f⟧ = 1

Tactic:
simp only [mk_eq_mk, hf, not_false_eq_true, inv_mk, mk_mul]

Premises used: CauSeq.Completion.inv_mk, CauSeq.Completion.mk_mul, CauSeq.Completion.mk_eq_mk, not_false_eq_true
-- 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
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ Eq (α := Cauchy abv) (mk (f.inv ⋯ * f)) 1

Tactic:
Quotient.sound (CauSeq.inv_mul_cancel hf)

Premises used: CauSeq.inv_mul_cancel, CauSeq.Completion.Cauchy, CauSeq.Completion.ofRat, CauSeq.Completion.mk, Quotient.sound
-- 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
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ Eq (α := Cauchy abv) (mk (f.inv ⋯ * f)) 1

Tactic:
exact Quotient.sound (CauSeq.inv_mul_cancel hf)

Premises used: CauSeq.inv_mul_cancel, Quotient.sound
-- 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
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
simp : Eq (α := Cauchy abv) (mk (f * f.inv ⋯)) 1
⊢ HMul.hMul (α := Cauchy abv) ⟦f⟧ (⟦f⟧)⁻¹ = 1

Tactic:
simp only [mk_eq_mk, hf, not_false_eq_true, inv_mk, mk_mul]

Premises used: CauSeq.Completion.inv_mk, CauSeq.Completion.mk_mul, CauSeq.Completion.mk_eq_mk, not_false_eq_true
-- 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
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ Eq (α := Cauchy abv) (mk (f * f.inv ⋯)) 1

Tactic:
Quotient.sound (CauSeq.mul_inv_cancel hf)

Premises used: CauSeq.Completion.Cauchy, CauSeq.Completion.ofRat, CauSeq.Completion.mk, CauSeq.mul_inv_cancel, Quotient.sound
-- 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
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ Eq (α := Cauchy abv) (mk (f * f.inv ⋯)) 1

Tactic:
exact Quotient.sound (CauSeq.mul_inv_cancel hf)

Premises used: CauSeq.mul_inv_cancel, Quotient.sound
-- 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
x : β
pos : ∀ (h : LimZero (const abv x)), Eq (α := CauSeq β abv) (const abv x⁻¹) 0
neg : ∀ (h : ¬LimZero (const abv x)), const abv x⁻¹ = inv (const abv x) h
⊢ Eq (α := CauSeq β abv) (const abv x⁻¹) (if h : LimZero (const abv x) then 0 else inv (const abv x) h)

Tactic:
split_ifs with h
-- 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
x : β
h : LimZero (const abv x)
⊢ Eq (α := CauSeq β abv) (const abv x⁻¹) 0

Tactic:
simp only [const_limZero.1 h, GroupWithZero.inv_zero, const_zero]

Premises used: GroupWithZero.inv_zero, CauSeq.const_limZero, Iff.mp, CauSeq.const_zero
-- 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
x : β
h : ¬LimZero (const abv x)
⊢ const abv x⁻¹ = inv (const abv x) h

Tactic:
rfl
-- 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
x : β
pos : ∀ (h : LimZero (const abv x)), Eq (α := CauSeq β abv) (const abv x⁻¹) 0
neg : ∀ (h : ¬LimZero (const abv x)), const abv x⁻¹ = inv (const abv x) h
pos₁ : ∀ (h : LimZero (const abv x)), Eq (α := CauSeq β abv) (const abv x⁻¹) 0
neg₁ : ∀ (h : ¬LimZero (const abv x)), const abv x⁻¹ = inv (const abv x) h
⊢ Eq (α := CauSeq β abv) (const abv x⁻¹) (if h : LimZero (const abv x) then 0 else inv (const abv x) h)

Tactic:
split_ifs with h <;>
    [simp only [const_limZero.1 h, GroupWithZero.inv_zero, const_zero]; rfl]

Premises used: GroupWithZero.inv_zero, CauSeq.const_zero
-- 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
x y : β
⊢ ofRat (x / y) = HDiv.hDiv (α := Cauchy abv) (ofRat x) (ofRat y)

Tactic:
simp only [div_eq_mul_inv, ofRat_inv, ofRat_mul]

Premises used: CauSeq.Completion.ofRat_inv, CauSeq.Completion.ofRat_mul, div_eq_mul_inv