awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
⊢ (∀ (x y : E), norm.{u_3} (E := F) ((f : (a : E) → F) (x⁻¹ * y) : F) = ‖x⁻¹ * y‖) ↔
    ∀ (x : E), norm.{u_3} (E := F) ((f : (a : E) → F) x : F) = ‖x‖

Tactic:
⟨fun h x => ?_, fun h x y => h _⟩

Premises used: HMul.hMul, Inv.inv, Iff.intro
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
refine :
  ∀ (h : ∀ (x y : E), norm.{u_3} (E := F) ((f : (a : E) → F) (x⁻¹ * y) : F) = ‖x⁻¹ * y‖) (x : E),
    norm.{u_3} (E := F) ((f : (a : E) → F) x : F) = ‖x‖
⊢ (∀ (x y : E), norm.{u_3} (E := F) ((f : (a : E) → F) (x⁻¹ * y) : F) = ‖x⁻¹ * y‖) ↔
    ∀ (x : E), norm.{u_3} (E := F) ((f : (a : E) → F) x : F) = ‖x‖

Tactic:
refine ⟨fun h x => ?_, fun h x y => h _⟩
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∀ (x y : E), norm.{u_3} (E := F) ((f : (a : E) → F) (x⁻¹ * y) : F) = ‖x⁻¹ * y‖
x : E
⊢ norm.{u_3} (E := F) ((f : (a : E) → F) x : F) = ‖x‖

Tactic:
simpa using h x 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
C : ℝ≥0
h : ∀ (x : E), nnnorm.{u_3} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖₊
⊢ LipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f : (a : E) → F)

Tactic:
@Real.toNNReal_coe C ▸ MonoidHomClass.lipschitz_of_bound f C h

Premises used: Eq.rec, Real.toNNReal_coe, MonoidHomClass.lipschitz_of_bound, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
K : ℝ≥0
h : ∀ (x : E), ‖x‖ ≤ (↑K : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
x y : E
⊢ dist x y ≤ (↑K : ℝ) * dist.{u_3} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)

Tactic:
simpa only [dist_eq_norm_inv_mul, map_inv, map_mul] using h (x⁻¹ * y)

Premises used: HMul.hMul, map_inv, dist_eq_norm_inv_mul, map_mul, Inv.inv
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
f : E → F
K : ℝ≥0
h : LipschitzWith K f
hf : f 1 = 1
x : E
⊢ ‖f x‖ ≤ (↑K : ℝ) * ‖x‖

Tactic:
simpa only [dist_one_right, hf] using h.dist_le_mul x 1

Premises used: LipschitzWith.dist_le_mul, OfNat.ofNat, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
f : E → F
K : ℝ≥0
h : LipschitzWith K f
hf : f 1 = 1
x : E
⊢ ‖f x‖₊ ≤ K * ‖x‖₊

Tactic:
h.norm_le_mul' hf x

Premises used: LipschitzWith.norm_le_mul', NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
f : E → F
K : ℝ≥0
h : AntilipschitzWith K f
hf : f 1 = 1
x : E
⊢ ‖x‖ ≤ (↑K : ℝ) * ‖f x‖

Tactic:
simpa only [dist_one_right, hf] using h.le_mul_dist x 1

Premises used: AntilipschitzWith.le_mul_dist, OfNat.ofNat, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∃ (K : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)
K : ℝ≥0
hK : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)
⊢ ((↑K : ℝ) + 1)⁻¹ > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
⊢ 0 ≤ c⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
refine_1 :
  (∃ (K : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)) →
    ∀ (K : ℝ≥0) (hK : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)) (x : E),
      ((↑K : ℝ) + 1)⁻¹ * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
refine_2 :
  (∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)) →
    ∀ (c : ℝ) (hc0 : c > 0) (hc : ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)) (x : E),
      ‖x‖ ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
⊢ (∃ (K : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)) ↔
    ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)

Tactic:
refine ⟨fun ⟨K, hK⟩ ↦ ⟨(K + 1)⁻¹, by positivity, fun x ↦ ?_⟩, fun ⟨c, hc0, hc⟩ ↦
    ⟨.mk c⁻¹ (by positivity), MonoidHomClass.antilipschitz_of_bound f fun x ↦ ?_⟩⟩
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∃ (K : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)
K : ℝ≥0
hK : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)
x : E
refine_1 :
  ((↑K : ℝ) + 1)⁻¹ * (↑K : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F) ≤
    norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
⊢ ((↑K : ℝ) + 1)⁻¹ * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)

Tactic:
grw [hK.le_mul_norm' (map_one f), ← mul_assoc]

Premises used: AntilipschitzWith.le_mul_norm', mul_assoc, map_one
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∃ (K : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)
K : ℝ≥0
hK : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)
x : E
⊢ ((↑K : ℝ) + 1)⁻¹ * (↑K : ℝ) ≤ 1

Tactic:
simp [field]
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∃ (K : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)
K : ℝ≥0
hK : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)
x : E
⊢ ((↑K : ℝ) + 1)⁻¹ * (↑K : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F) ≤
    norm.{u_3} (E := F) ((f : (a : E) → F) x : F)

Tactic:
exact mul_le_of_le_one_left (norm_nonneg' (f x)) (by simp [field])

Premises used: norm_nonneg', mul_le_of_le_one_left, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
x : E
h₂ : 0 ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ)
refine_2 : ‖x‖ ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ) * (c * ‖x‖)
refine_2₁ : ‖x‖ ≤ c⁻¹ * (c * ‖x‖)
refine_2₂ refine_2₃ : ‖x‖ ≤ ‖x‖
⊢ ‖x‖ ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F)

Tactic:
grw [← hc, NNReal.coe_mk, inv_mul_cancel_left₀ hc0.ne']

Premises used: inv_mul_cancel_left₀, NNReal.coe_mk, LT.lt.ne'
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
f : E → F
K : ℝ≥0
h : AntilipschitzWith K f
hf : f 1 = 1
x : E
⊢ ‖x‖₊ ≤ K * ‖f x‖₊

Tactic:
h.le_mul_norm' hf x

Premises used: AntilipschitzWith.le_mul_norm', NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : OneHomClass 𝓕 E F
f : 𝓕
K : ℝ≥0
h : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)
x : E
⊢ ‖x‖ ≤ (↑K : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F)

Tactic:
h.le_mul_nnnorm' (map_one f) x

Premises used: OneHomClass.map_one, AntilipschitzWith.le_mul_nnnorm', NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
f : E → F
hi : Isometry f
h₁ : f 1 = 1
x : E
⊢ ‖f x‖₊ = ‖x‖₊

Tactic:
Subtype.ext <| hi.norm_map_of_map_one h₁ x

Premises used: NNReal, Isometry.norm_map_of_map_one, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedGroup E
⊢ LipschitzWith.{u_2, 0} (α := E) 1 norm

Tactic:
simpa using LipschitzWith.dist_right (1 : E)

Premises used: LipschitzWith.dist_right, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedGroup E
⊢ LipschitzWith.{u_2, 0} (α := E) 1 nnnorm

Tactic:
lipschitzWith_one_norm'

Premises used: LipschitzWith, lipschitzWith_one_norm', NNReal.mk
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedGroup E
⊢ UniformContinuous.{u_2, 0} (α := E) norm

Tactic:
lipschitzWith_one_norm'.uniformContinuous

Premises used: lipschitzWith_one_norm', LipschitzWith.uniformContinuous
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedGroup E
⊢ UniformContinuous (β := ℝ≥0) fun (a : E) ↦ ‖a‖₊

Tactic:
uniformContinuous_norm'.subtype_mk _

Premises used: NNReal.mk, NNReal, uniformContinuous_norm', UniformContinuous.subtype_mk
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
a₁ a₂ b₁ b₂ : E
r₁ r₂ : ℝ
a : Eᵐᵒᵖ
b c : E
⊢ dist (a • b) (a • c) = dist b c

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
rw : dist a (b * a) = dist 1 b
rw₁ : dist a (b * a) = dist (a * 1) (a * b)
rw₂ : dist a (b * a) = dist a (a * b)
rw₃ rw₄ : dist a (a * b) = dist a (a * b)
⊢ dist a (b * a) = ‖b‖

Tactic:
rw [← dist_one_left, ← dist_mul_left a 1 b, mul_one, mul_comm]

Premises used: dist_mul_left, dist_one_left, mul_comm, mul_one, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
rw : dist a (b * a) = ‖b‖
rw₁ rw₂ : ‖b‖ = ‖b‖
⊢ dist (b * a) a = ‖b‖

Tactic:
rw [dist_comm, dist_mul_self_right]

Premises used: dist_comm, dist_mul_self_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
rw : dist a (a * b⁻¹) = ‖b‖
rw₁ : ‖b⁻¹‖ = ‖b‖
rw₂ rw₃ : ‖b‖ = ‖b‖
⊢ dist a (a / b) = ‖b‖

Tactic:
rw [div_eq_mul_inv, dist_self_mul_right, norm_inv']

Premises used: norm_inv', div_eq_mul_inv, dist_self_mul_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
rw : dist a (a / b) = ‖b‖
rw₁ rw₂ : ‖b‖ = ‖b‖
⊢ dist (a / b) a = ‖b‖

Tactic:
rw [dist_comm, dist_self_div_right]

Premises used: dist_comm, dist_self_div_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b c : E
rw : dist (a / b * b) (c * b) = dist a (c * b)
rw₁ rw₂ : dist a (c * b) = dist a (c * b)
⊢ dist (a / b) c = dist a (c * b)

Tactic:
rw [← dist_mul_right _ _ b, div_mul_cancel]

Premises used: div_mul_cancel, dist_mul_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b c : E
rw : dist (a * c) (b / c * c) = dist (a * c) b
rw₁ rw₂ : dist (a * c) b = dist (a * c) b
⊢ dist a (b / c) = dist (a * c) b

Tactic:
rw [← dist_mul_right _ _ c, div_mul_cancel]

Premises used: div_mul_cancel, dist_mul_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂

Tactic:
simpa only [dist_mul_left, dist_mul_right] using dist_triangle (a₁ * a₂) (b₁ * a₂) (b₁ * b₂)

Premises used: dist_triangle, HMul.hMul, dist_mul_left, dist_mul_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
r₁ r₂ : ℝ
h₁ : dist a₁ b₁ ≤ r₁
h₂ : dist a₂ b₂ ≤ r₂
⊢ dist (a₁ * a₂) (b₁ * b₂) ≤ r₁ + r₂

Tactic:
(dist_mul_mul_le a₁ a₂ b₁ b₂).trans <| add_le_add h₁ h₂

Premises used: add_le_add, dist_mul_mul_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂

Tactic:
simpa only [div_eq_mul_inv, dist_inv_inv] using dist_mul_mul_le a₁ a₂⁻¹ b₁ b₂⁻¹

Premises used: dist_inv_inv, div_eq_mul_inv, Inv.inv, dist_mul_mul_le
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
r₁ r₂ : ℝ
h₁ : dist a₁ b₁ ≤ r₁
h₂ : dist a₂ b₂ ≤ r₂
⊢ dist (a₁ / a₂) (b₁ / b₂) ≤ r₁ + r₂

Tactic:
(dist_div_div_le a₁ a₂ b₁ b₂).trans <| add_le_add h₁ h₂

Premises used: dist_div_div_le, add_le_add, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)

Tactic:
simpa only [dist_mul_left, dist_mul_right, dist_comm b₂] using
    abs_dist_sub_le (a₁ * a₂) (b₁ * b₂) (b₁ * a₂)

Premises used: HMul.hMul, abs_dist_sub_le, dist_mul_left, dist_comm, dist_mul_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂

Tactic:
NNReal.coe_le_coe.1 <| dist_mul_mul_le a₁ a₂ b₁ b₂

Premises used: dist_mul_mul_le, Iff.mp, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
simp : (↑(nndist (a₁ * a₂) (b₁ * b₂)) : ℝ≥0∞) ≤ (↑(nndist a₁ b₁) : ℝ≥0∞) + (↑(nndist a₂ b₂) : ℝ≥0∞)
⊢ edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂

Tactic:
simp only [edist_nndist]

Premises used: edist_nndist
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
norm_cast : nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂
⊢ (↑(nndist (a₁ * a₂) (b₁ * b₂)) : ℝ≥0∞) ≤ (↑(nndist a₁ b₁) : ℝ≥0∞) + (↑(nndist a₂ b₂) : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂

Tactic:
apply nndist_mul_mul_le

Premises used: nndist_mul_mul_le
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
K : ℝ≥0
f : α → E
⊢ LipschitzWith K f⁻¹ ↔ LipschitzWith K f

Tactic:
simp [LipschitzWith]

Premises used: LipschitzWith
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
K : ℝ≥0
f : α → E
⊢ AntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f

Tactic:
simp [AntilipschitzWith]

Premises used: AntilipschitzWith
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
K : ℝ≥0
f : α → E
s : Set α
⊢ LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s

Tactic:
simp [LipschitzOnWith]

Premises used: LipschitzOnWith
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
f : α → E
⊢ LocallyLipschitz f⁻¹ ↔ LocallyLipschitz f

Tactic:
simp [LocallyLipschitz]

Premises used: LocallyLipschitz
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
f : α → E
s : Set α
⊢ LocallyLipschitzOn s f⁻¹ ↔ LocallyLipschitzOn s f

Tactic:
simp [LocallyLipschitzOn]

Premises used: LocallyLipschitzOn
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
s : Set α
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
⊢ LipschitzOnWith.{u_4, u_5} (β := E) (Kf + Kg) (fun (x : α) ↦ f x * g x) s

Tactic:
fun x hx y hy ↦
  calc
    edist (f x * g x) (f y * g y) ≤ edist (f x) (f y) + edist (g x) (g y) :=
      edist_mul_mul_le _ _ _ _
    _ ≤ Kf * edist x y + Kg * edist x y := add_le_add (hf hx hy) (hg hx hy)
    _ = (Kf + Kg) * edist x y := (add_mul _ _ _).symm

Premises used: add_mul, ENNReal.ofNNReal, Trans.trans, add_le_add, WithTop.map₂, edist_mul_mul_le, WithTop.some, LipschitzOnWith, EDist.edist, Eq.symm, Option.map₂
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith.{u_4, u_5} (β := E) (Kf + Kg) fun (x : α) ↦ f x * g x

Tactic:
simpa [← lipschitzOnWith_univ] using hf.lipschitzOnWith.mul hg.lipschitzOnWith

Premises used: lipschitzOnWith_univ, LipschitzWith.lipschitzOnWith, LipschitzOnWith.mul
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
obtain :
  ∀ (Kf : ℝ≥0) (t : Set α) (ht : t ∈ 𝓝[s] x) (hKf : LipschitzOnWith Kf f t),
    ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith.{u_4, u_5} (β := E) K (fun (x : α) ↦ f x * g x) t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith.{u_4, u_5} (β := E) K (fun (x : α) ↦ f x * g x) t

Tactic:
obtain ⟨Kf, t, ht, hKf⟩ := hf hx
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
Kf : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] x
hKf : LipschitzOnWith Kf f t
obtain :
  ∀ (Kg : ℝ≥0) (u : Set α) (hu : u ∈ 𝓝[s] x) (hKg : LipschitzOnWith Kg g u),
    ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith.{u_4, u_5} (β := E) K (fun (x : α) ↦ f x * g x) t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith.{u_4, u_5} (β := E) K (fun (x : α) ↦ f x * g x) t

Tactic:
obtain ⟨Kg, u, hu, hKg⟩ := hg hx
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
Kf : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] x
hKf : LipschitzOnWith Kf f t
Kg : ℝ≥0
u : Set α
hu : u ∈ 𝓝[s] x
hKg : LipschitzOnWith Kg g u
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith.{u_4, u_5} (β := E) K (fun (x : α) ↦ f x * g x) t

Tactic:
⟨Kf + Kg, t ∩ u, inter_mem ht hu,
    (hKf.mono Set.inter_subset_left).mul (hKg.mono Set.inter_subset_right)⟩

Premises used: LipschitzOnWith.mono, Filter.inter_mem, Set.inter_subset_left, Inter.inter, HAdd.hAdd, And.intro, Exists.intro, LipschitzOnWith.mul, Set.inter_subset_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
Kf : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] x
hKf : LipschitzOnWith Kf f t
Kg : ℝ≥0
u : Set α
hu : u ∈ 𝓝[s] x
hKg : LipschitzOnWith Kg g u
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith.{u_4, u_5} (β := E) K (fun (x : α) ↦ f x * g x) t

Tactic:
exact ⟨Kf + Kg, t ∩ u, inter_mem ht hu,
    (hKf.mono Set.inter_subset_left).mul (hKg.mono Set.inter_subset_right)⟩
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
f g : α → E
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz.{u_4, u_5} (β := E) fun (x : α) ↦ f x * g x

Tactic:
simpa [← locallyLipschitzOn_univ] using hf.locallyLipschitzOn.mul hg.locallyLipschitzOn

Premises used: locallyLipschitzOn_univ, LocallyLipschitz.locallyLipschitzOn, LocallyLipschitzOn.mul
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
s : Set α
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
⊢ LipschitzOnWith.{u_4, u_5} (β := E) (Kf + Kg) (fun (x : α) ↦ f x / g x) s

Tactic:
simpa only [div_eq_mul_inv] using hf.mul hg.inv

Premises used: div_eq_mul_inv, LipschitzOnWith.mul, LipschitzOnWith.inv
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith.{u_4, u_5} (β := E) (Kf + Kg) fun (x : α) ↦ f x / g x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul hg.inv

Premises used: LipschitzWith.inv, div_eq_mul_inv, LipschitzWith.mul
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
⊢ LocallyLipschitzOn.{u_4, u_5} (β := E) s fun (x : α) ↦ f x / g x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul hg.inv

Premises used: div_eq_mul_inv, LocallyLipschitzOn.inv, LocallyLipschitzOn.mul
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
f g : α → E
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz.{u_4, u_5} (β := E) fun (x : α) ↦ f x / g x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul hg.inv

Premises used: LocallyLipschitz.mul, LocallyLipschitz.inv, div_eq_mul_inv
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
⊢ AntilipschitzWith.{u_4, u_5} (β := E) (Kf⁻¹ - Kg)⁻¹ fun (x : α) ↦ f x * g x

Tactic:
AntilipschitzWith.of_le_mul_dist fun x y => ?_

Premises used: AntilipschitzWith.of_le_mul_dist
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
refine : ∀ (x y : α), dist x y ≤ (↑(Kf⁻¹ - Kg)⁻¹ : ℝ) * dist (f x * g x) (f y * g y)
⊢ AntilipschitzWith.{u_4, u_5} (β := E) (Kf⁻¹ - Kg)⁻¹ fun (x : α) ↦ f x * g x

Tactic:
refine AntilipschitzWith.of_le_mul_dist fun x y => ?_

Premises used: AntilipschitzWith.of_le_mul_dist
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
rw : dist x y ≤ dist (f x * g x) (f y * g y) / (↑(Kf⁻¹ - Kg) : ℝ)
⊢ dist x y ≤ (↑(Kf⁻¹ - Kg)⁻¹ : ℝ) * dist (f x * g x) (f y * g y)

Tactic:
rw [NNReal.coe_inv, ← _root_.div_eq_inv_mul]

Premises used: NNReal.coe_inv, div_eq_inv_mul