awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
m : Multiset R
⊢ 0 < m.prod ↔ ∀ (x : R), x ∈ m → 0 < x
have mk : ∀ (l : List R),
  0 < prod (Quot.mk (⇑(List.isSetoid R) : List R → List R → Prop) l) ↔
    ∀ (x : R), Membership.mem (γ := Multiset R) (Quot.mk (⇑(List.isSetoid R) : List R → List R → Prop) l) x → 0 < x
Tactic: rcases m with ⟨l⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < prod (Quot.mk (⇑(List.isSetoid R) : List R → List R → Prop) l) ↔
    ∀ (x : R), Membership.mem (γ := Multiset R) (Quot.mk (⇑(List.isSetoid R) : List R → List R → Prop) l) x → 0 < x
have mk : 0 < l.prod ↔ ∀ (x : R), x ∈ (↑l : Multiset R) → 0 < x
Tactic: rw [Multiset.quot_mk_to_coe'', Multiset.prod_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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)
s : Multiset α
hps : ∀ (a : α), a ∈ s → p a
⊢ f s.prod ≤ (map f s).prod
have revert : ∀ (s : Multiset α) (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
Tactic: revert s
Cleared hypotheses: s, hps
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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)
⊢ ∀ (s : Multiset α) (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
have refine : ∀ (a : α) (s : Multiset α),
  (∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod) →
    ∀ (hps : ∀ (a_2 : α), a_2 ∈ a ::ₘ s → p a_2), f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
Tactic: refine Multiset.induction (by simp [h_one]) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
have pos : ∀ (hs0 : s = ∅), f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
Tactic: by_cases hs0 : s = ∅
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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
pos : ∀ (hs0 : s = ∅), f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
have neg : ∀ (hs0 : ¬s = ∅), f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
Tactic: by_cases hs0 : s = ∅
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (hypothesis)
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 = ∅
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
have hps : ∀ (x : α), x ∈ s → p x
Tactic: have hps : ∀ x, x ∈ s → p x := fun x hx ↦ hpsa x (mem_cons_of_mem hx)
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (hypothesis)
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
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
have hp_prod : p s.prod
Tactic: have hp_prod : p s.prod := prod_induction_nonempty p hp_mul hs0 hps
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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 ≤ (map f (a ::ₘ s)).prod
have neg : f (a * s.prod) ≤ f a * (map f s).prod
Tactic: rw [prod_cons, map_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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 * f s.prod ≤ f a * (map f s).prod
have ha : 0 ≤ f a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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
⊢ f a * f s.prod ≤ f a * (map f s).prod
have hbc : f s.prod ≤ (map f s).prod
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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
⊢ f a ≤ (map f s).prod
have obtain : ∀ (s' : Multiset α) (ha : a ∈ a ::ₘ s'), f a ≤ (map f (a ::ₘ s')).prod
Tactic: obtain ⟨s', rfl⟩ := exists_cons_of_mem ha
Cleared hypotheses: s, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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 ≤ (map f (a ::ₘ s')).prod
have rw : f a ≤ f a * (map f s').prod
Tactic: rw [map_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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 * 1 ≤ f a * (map f s').prod
have ha₁ : 0 ≤ f a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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
⊢ f a * 1 ≤ f a * (map f s').prod
have hbc : 1 ≤ (map f s').prod
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Multiset (goal)
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 * (map f s').prod
have calc : f a * 1 ≤ 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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,
    ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε
have K0 : 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 _ _)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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,
    ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε
have εK : 0 < ε / 2 / max 1 (max K₁ K₂)
Tactic: have εK := div_pos (half_pos ε0) K0
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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₂) < ε
have 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₂) < ε
Tactic: refine ⟨_, εK, fun {a₁ a₂ b₁ b₂} ha₁ hb₂ h₁ h₂ => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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₁ * a₂ - b₁ * b₂) < ε
have ha₂ : 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 _))
Cleared hypotheses: ha₁
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 (a₁ * a₂ - b₁ * b₂) < ε
have hb₃ : 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 _))
Cleared hypotheses: hb₂
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
have h₃ : 0 ≤ abv (a₁ - b₁)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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₁)
⊢ abv (a₁ - b₁) * abv b₂ + abv (a₂ - b₂) * abv a₁ < ε / 2 / M * M + ε / 2 / M * M
have h₄ : 0 ≤ abv b₂
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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₂
⊢ abv (a₁ - b₁) * abv b₂ + abv (a₂ - b₂) * abv a₁ < ε / 2 / M * M + ε / 2 / M * M
have h₅ : 0 ≤ abv (a₂ - b₂)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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₂)
⊢ abv (a₁ - b₁) * abv b₂ + abv (a₂ - b₂) * abv a₁ < ε / 2 / M * M + ε / 2 / M * M
have h₆ : 0 ≤ abv a₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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₁ * a₂ - b₁ * b₂) < ε
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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₁ * a₂ - b₁ * b₂) < ε
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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⁻¹) < ε
have refine : ∀ {a b : β} (ha : K ≤ abv a) (hb : K ≤ abv b) (h : abv (a - b) < K * ε * K), abv (a⁻¹ - b⁻¹) < ε
Tactic: refine ⟨K * ε * K, mul_pos (mul_pos K0 ε0) K0, fun {a b} ha hb h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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
⊢ abv (a⁻¹ - b⁻¹) < ε
have a0 : 0 < abv a
Tactic: have a0 := K0.trans_le ha
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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
⊢ abv (a⁻¹ - b⁻¹) < ε
have b0 : 0 < abv b
Tactic: have b0 := K0.trans_le hb
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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⁻¹) < ε
have rw : (abv a)⁻¹ * abv (a - b) * (abv 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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)⁻¹ < ε
have refine : abv a * ((abv a)⁻¹ * abv (a - b) * (abv b)⁻¹) * abv b < abv a * ε * abv b
Tactic: refine lt_of_mul_lt_mul_left (lt_of_mul_lt_mul_right ?_ b0.le) a0.le
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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)⁻¹ * abv (a - b) * (abv b)⁻¹) * abv b < abv a * ε * abv b
have rw : abv (a - b) < abv a * ε * abv b
Tactic: rw [mul_assoc, inv_mul_cancel_right₀ b0.ne', ← mul_assoc, mul_inv_cancel₀ a0.ne', one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
have refine : K * ε * K ≤ abv a * ε * abv b
Tactic: refine h.trans_le ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ K * ε * K ≤ abv a * ε * abv b
have b0₁ : 0 ≤ abv a * ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ∀ k ≥ i, abv (f j - f k) < ε
have refine : ∀ (i : ℕ) (hi : ∀ j ≥ i, abv (f j - f i) < ε / 2) (j : ℕ) (ij : j ≥ i) (k : ℕ) (ik : k ≥ i), abv (f j - f k) < ε
Tactic: refine (hf _ (half_pos ε0)).imp fun i hi j ij k ik => ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε
have rw : abv (f j - f k) < ε / 2 + ε / 2
Tactic: rw [← add_halves ε]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε / 2 + ε / 2
have refine : abv (f i - f k) < ε / 2
Tactic: refine lt_of_le_of_lt (abv_sub_le abv _ _ _) (add_lt_add (hi _ ij) ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f i - f k) < ε / 2
have rw : abv (f k - f i) < ε / 2
Tactic: rw [abv_sub abv]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
⊢ ∃ (r : α), ∀ (i : ℕ), abv (f i) < r
have obtain : ∀ (i : ℕ) (h : ∀ j ≥ i, abv (f j - f i) < 1), ∃ (r : α), ∀ (i : ℕ), abv (f i) < r
Tactic: obtain ⟨i, h⟩ := hf _ zero_lt_one
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i : ℕ
h : ∀ j ≥ i, abv (f j - f i) < 1
⊢ ∃ (r : α), ∀ (i : ℕ), abv (f i) < r
have hR : let R : ℕ → α :=
  Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ));
R = Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))
Tactic: set R : ℕ → α := @Nat.rec (fun _ => α) (abv (f 0)) fun i c => max c (abv (f i.succ)) with hR
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i : ℕ
h : ∀ j ≥ i, abv (f j - f i) < 1
R : ℕ → α :=
  Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))
hR : R = Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))
⊢ ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i
have refine : ∀ (n : ℕ) (n_ih : ∀ j ≤ n, abv (f j) ≤ R n), ∀ j ≤ n.succ, abv (f j) ≤ R n.succ
Tactic: refine Nat.rec (by simp [hR]) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i : ℕ
h : ∀ j ≥ i, abv (f j - f i) < 1
R : ℕ → α :=
  Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))
hR : R = Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))
⊢ ∃ (r : α), ∀ (i : ℕ), abv (f i) < r
have this : ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i
Tactic: have : ∀ i, ∀ j ≤ i, abv (f j) ≤ R i := by
    refine Nat.rec (by simp [hR]) ?_
    rintro i hi j (rfl | hj)
    · simp [R]
    · exact (hi j hj).trans (le_max_left _ _)