awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : ∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
⊢ ∀ (x : α), x ∈ s → p x

Tactic:
have hps : ∀ x, x ∈ s → p x := fun x hx ↦ hpsa x (mem_cons_of_mem hx)
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : ∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
⊢ p s.prod

Tactic:
have hp_prod : p s.prod := prod_induction_nonempty p hp_mul hs0 hps
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : ∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
neg : f (a * s.prod) ≤ f a * (map f s).prod
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
rw [prod_cons, map_cons, prod_cons]

Premises used: Multiset.map_cons, Multiset.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : ∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
ha : 0 ≤ f a
hbc : f s.prod ≤ (map f s).prod
⊢ f a * f s.prod ≤ f a * (map f s).prod

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : ∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ 0 ≤ f a

Tactic:
h0 _
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : ∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f s.prod ≤ (map f s).prod

Tactic:
hs hps
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : ∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ 0 ≤ f a

Tactic:
exacts [h0 _, hs hps]
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : ∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Tactic:
exact (h_mul a s.prod (hpsa a (mem_cons_self a s)) hp_prod).trans
      (by gcongr; exacts [h0 _, hs hps])

Premises used: Multiset.prod, LE.le.trans, Multiset.mem_cons_self
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
⊢ ∀ (a b : α), (fun (x : α) ↦ True) a → (fun (x : α) ↦ True) b → (fun (x : α) ↦ True) (a * b)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
⊢ ∀ (a : α), a ∈ s → (fun (x : α) ↦ True) a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero β
inst_1 : PartialOrder β
inst_2 : PosMulMono β
inst_3 : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
s : Multiset α
a : α
ha : a ∈ s
obtain : ∀ (s' : Multiset α) (ha : a ∈ a ::ₘ s'), f a ≤ (map f (a ::ₘ s')).prod
⊢ f a ≤ (map f s).prod

Tactic:
obtain ⟨s', rfl⟩ := exists_cons_of_mem ha

Premises used: Multiset.exists_cons_of_mem, rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero β
inst_1 : PartialOrder β
inst_2 : PosMulMono β
inst_3 : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
rw : f a ≤ f a * (map f s').prod
⊢ f a ≤ (map f (a ::ₘ s')).prod

Tactic:
rw [map_cons, prod_cons]

Premises used: Multiset.map_cons, Multiset.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero β
inst_1 : PartialOrder β
inst_2 : PosMulMono β
inst_3 : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ f a = f a * 1

Tactic:
(mul_one (f a)).symm

Premises used: mul_one, Eq.symm
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero β
inst_1 : PartialOrder β
inst_2 : PosMulMono β
inst_3 : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
ha₁ : 0 ≤ f a
hbc : 1 ≤ (map f s').prod
⊢ f a * 1 ≤ f a * (map f s').prod

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero β
inst_1 : PartialOrder β
inst_2 : PosMulMono β
inst_3 : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ 0 ≤ f a

Tactic:
le_trans (zero_le_one' β) (h1 a)

Premises used: zero_le_one', le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero β
inst_1 : PartialOrder β
inst_2 : PosMulMono β
inst_3 : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ 0 ≤ f a

Tactic:
exact le_trans (zero_le_one' β) (h1 a)

Premises used: zero_le_one', le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero β
inst_1 : PartialOrder β
inst_2 : PosMulMono β
inst_3 : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ 1 ≤ (map f s').prod

Tactic:
simp_all [one_le_prod]

Premises used: Multiset.one_le_prod
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero β
inst_1 : PartialOrder β
inst_2 : PosMulMono β
inst_3 : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
calc : f a * 1 ≤ f a * (map f s').prod
⊢ f a ≤ f a * (map f s').prod

Tactic:
calc f a = f a * 1 := (mul_one (f a)).symm
    _ ≤ f a * (s'.map f).prod := by
      gcongr
      · exact le_trans (zero_le_one' β) (h1 a)
      · simp_all [one_le_prod]

Premises used: Multiset.map, Multiset.prod, mul_one, Eq.symm
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2
h₂ : abv (a₂ - b₂) < ε / 2
⊢ abv (a₁ + a₂ - (b₁ + b₂)) < ε

Tactic:
simpa [add_halves, sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using
      lt_of_le_of_lt (abv_add abv _ _) (add_lt_add h₁ h₂)

Premises used: lt_of_le_of_lt, add_halves, add_left_comm, add_assoc, sub_eq_add_neg, add_comm, add_lt_add, IsAbsoluteValue.abv_add
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
⊢ 0 < max 1 (max K₁ K₂)

Tactic:
have K0 : (0 : α) < max 1 (max K₁ K₂) := lt_of_lt_of_le zero_lt_one (le_max_left _ _)
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
⊢ 0 < ε / 2 / max 1 (max K₁ K₂)

Tactic:
have εK := div_pos (half_pos ε0) K0
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
⊢ ∃ δ > 0,
    ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε

Tactic:
⟨_, εK, fun {a₁ a₂ b₁ b₂} ha₁ hb₂ h₁ h₂ => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
refine :
  ∀ {a₁ a₂ b₁ b₂ : β} (ha₁ : abv a₁ < K₁) (hb₂ : abv b₂ < K₂) (h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂))
    (h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)), abv (a₁ * a₂ - b₁ * b₂) < ε
⊢ ∃ δ > 0,
    ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε

Tactic:
refine ⟨_, εK, fun {a₁ a₂ b₁ b₂} ha₁ hb₂ h₁ h₂ => ?_⟩
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
ha₁ : abv a₁ < K₁
hb₂ : abv b₂ < K₂
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
⊢ abv a₁ < max 1 (max K₁ K₂)

Tactic:
replace ha₁ := lt_of_lt_of_le ha₁ (le_trans (le_max_left _ K₂) (le_max_right 1 _))
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
hb₂ : abv b₂ < K₂
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
ha₁ : abv a₁ < max 1 (max K₁ K₂)
⊢ abv b₂ < max 1 (max K₁ K₂)

Tactic:
replace hb₂ := lt_of_lt_of_le hb₂ (le_trans (le_max_right K₁ _) (le_max_right 1 _))
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
ha₁ : abv a₁ < max 1 (max K₁ K₂)
hb₂ : abv b₂ < max 1 (max K₁ K₂)
⊢ let M := max 1 (max K₁ K₂);
  0 < M

Tactic:
set M := max 1 (max K₁ K₂)

Premises used: Max.max, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
ha₁ : abv a₁ < max 1 (max K₁ K₂)
hb₂ : abv b₂ < max 1 (max K₁ K₂)
K0₁ :
  let M := max 1 (max K₁ K₂);
  0 < M
⊢ let M := max 1 (max K₁ K₂);
  0 < ε / 2 / M

Tactic:
set M := max 1 (max K₁ K₂)

Premises used: Max.max, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
ha₁ : abv a₁ < max 1 (max K₁ K₂)
hb₂ : abv b₂ < max 1 (max K₁ K₂)
K0₁ :
  let M := max 1 (max K₁ K₂);
  0 < M
εK₁ :
  let M := max 1 (max K₁ K₂);
  0 < ε / 2 / M
⊢ let M := max 1 (max K₁ K₂);
  abv (a₁ - b₁) < ε / 2 / M

Tactic:
set M := max 1 (max K₁ K₂)

Premises used: Max.max, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
ha₁ : abv a₁ < max 1 (max K₁ K₂)
hb₂ : abv b₂ < max 1 (max K₁ K₂)
K0₁ :
  let M := max 1 (max K₁ K₂);
  0 < M
εK₁ :
  let M := max 1 (max K₁ K₂);
  0 < ε / 2 / M
h₃ :
  let M := max 1 (max K₁ K₂);
  abv (a₁ - b₁) < ε / 2 / M
⊢ let M := max 1 (max K₁ K₂);
  abv (a₂ - b₂) < ε / 2 / M

Tactic:
set M := max 1 (max K₁ K₂)

Premises used: Max.max, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
ha₁ : abv a₁ < max 1 (max K₁ K₂)
hb₂ : abv b₂ < max 1 (max K₁ K₂)
K0₁ :
  let M := max 1 (max K₁ K₂);
  0 < M
εK₁ :
  let M := max 1 (max K₁ K₂);
  0 < ε / 2 / M
h₃ :
  let M := max 1 (max K₁ K₂);
  abv (a₁ - b₁) < ε / 2 / M
h₄ :
  let M := max 1 (max K₁ K₂);
  abv (a₂ - b₂) < ε / 2 / M
⊢ let M := max 1 (max K₁ K₂);
  abv a₁ < M

Tactic:
set M := max 1 (max K₁ K₂)

Premises used: Max.max, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
ha₁ : abv a₁ < max 1 (max K₁ K₂)
hb₂ : abv b₂ < max 1 (max K₁ K₂)
K0₁ :
  let M := max 1 (max K₁ K₂);
  0 < M
εK₁ :
  let M := max 1 (max K₁ K₂);
  0 < ε / 2 / M
h₃ :
  let M := max 1 (max K₁ K₂);
  abv (a₁ - b₁) < ε / 2 / M
h₄ :
  let M := max 1 (max K₁ K₂);
  abv (a₂ - b₂) < ε / 2 / M
ha₂ :
  let M := max 1 (max K₁ K₂);
  abv a₁ < M
⊢ let M := max 1 (max K₁ K₂);
  abv b₂ < M

Tactic:
set M := max 1 (max K₁ K₂)

Premises used: Max.max, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
h₃ : 0 ≤ abv (a₁ - b₁)
h₄ : 0 ≤ abv b₂
h₅ : 0 ≤ abv (a₂ - b₂)
h₆ : 0 ≤ abv a₁
⊢ abv (a₁ - b₁) * abv b₂ + abv (a₂ - b₂) * abv a₁ < ε / 2 / M * M + ε / 2 / M * M

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
⊢ abv (a₁ - b₁) * abv b₂ + abv (a₂ - b₂) * abv a₁ < ε / 2 / M * M + ε / 2 / M * M

Tactic:
have : abv (a₁ - b₁) * abv b₂ + abv (a₂ - b₂) * abv a₁ < ε / 2 / M * M + ε / 2 / M * M := by
    gcongr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
this : abv (a₁ - b₁) * abv b₂ + abv (a₂ - b₂) * abv a₁ < ε / 2 / M * M + ε / 2 / M * M
⊢ abv ((a₁ - b₁) * b₂) + abv (a₁ * (a₂ - b₂)) < ε

Tactic:
rw [← abv_mul abv, mul_comm, div_mul_cancel₀ _ (ne_of_gt K0), ← abv_mul abv, add_halves] at this

Premises used: div_mul_cancel₀, add_halves, ne_of_gt, mul_comm, IsAbsoluteValue.abv_mul
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
this : abv ((a₁ - b₁) * b₂) + abv (a₁ * (a₂ - b₂)) < ε
⊢ abv (a₁ * a₂ - b₁ * b₂) < ε

Tactic:
simpa [sub_eq_add_neg, mul_add, add_mul, add_left_comm] using
    lt_of_le_of_lt (abv_add abv _ _) this

Premises used: add_mul, lt_of_le_of_lt, add_left_comm, sub_eq_add_neg, IsAbsoluteValue.abv_add, mul_add
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
⊢ ∃ δ > 0, ∀ {a b : β}, K ≤ abv a → K ≤ abv b → abv (a - b) < δ → abv (a⁻¹ - b⁻¹) < ε

Tactic:
⟨K * ε * K, mul_pos (mul_pos K0 ε0) K0, fun {a b} ha hb h => ?_⟩

Premises used: HMul.hMul, mul_pos, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
refine : ∀ {a b : β} (ha : K ≤ abv a) (hb : K ≤ abv b) (h : abv (a - b) < K * ε * K), abv (a⁻¹ - b⁻¹) < ε
⊢ ∃ δ > 0, ∀ {a b : β}, K ≤ abv a → K ≤ abv b → abv (a - b) < δ → abv (a⁻¹ - b⁻¹) < ε

Tactic:
refine ⟨K * ε * K, mul_pos (mul_pos K0 ε0) K0, fun {a b} ha hb h => ?_⟩
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
⊢ 0 < abv a

Tactic:
have a0 := K0.trans_le ha
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
⊢ 0 < abv b

Tactic:
have b0 := K0.trans_le hb
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
rw : (abv a)⁻¹ * abv (a - b) * (abv b)⁻¹ < ε
⊢ abv (a⁻¹ - b⁻¹) < ε

Tactic:
rw [inv_sub_inv' ((abv_pos abv).1 a0) ((abv_pos abv).1 b0), abv_mul abv, abv_mul abv, abv_inv abv,
    abv_inv abv, abv_sub abv]

Premises used: IsAbsoluteValue.abv_sub, inv_sub_inv', IsAbsoluteValue.abv_inv, Iff.mp, IsAbsoluteValue.abv_mul, IsAbsoluteValue.abv_pos
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ (abv a)⁻¹ * abv (a - b) * (abv b)⁻¹ < ε

Tactic:
lt_of_mul_lt_mul_left (lt_of_mul_lt_mul_right ?_ b0.le) a0.le

Premises used: lt_of_mul_lt_mul_left, LT.lt.le, lt_of_mul_lt_mul_right
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
refine : abv a * ((abv a)⁻¹ * abv (a - b) * (abv b)⁻¹) * abv b < abv a * ε * abv b
⊢ (abv a)⁻¹ * abv (a - b) * (abv b)⁻¹ < ε

Tactic:
refine lt_of_mul_lt_mul_left (lt_of_mul_lt_mul_right ?_ b0.le) a0.le

Premises used: lt_of_mul_lt_mul_left, LT.lt.le, lt_of_mul_lt_mul_right
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
rw : abv (a - b) < abv a * ε * abv b
⊢ abv a * ((abv a)⁻¹ * abv (a - b) * (abv b)⁻¹) * abv b < abv a * ε * abv b

Tactic:
rw [mul_assoc, inv_mul_cancel_right₀ b0.ne', ← mul_assoc, mul_inv_cancel₀ a0.ne', one_mul]

Premises used: mul_inv_cancel₀, mul_assoc, LT.lt.ne', one_mul, inv_mul_cancel_right₀
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ abv (a - b) < abv a * ε * abv b

Tactic:
h.trans_le ?_

Premises used: LT.lt.trans_le