awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
obtain : ∀ (Rt : ℝ) (hRt : ∀ x ∈ t, ‖x‖ ≤ Rt), IsBounded (s * t)
⊢ IsBounded (s * t)

Tactic:
obtain ⟨Rt, hRt⟩ : ∃ R, ∀ x ∈ t, ‖x‖ ≤ R := ht.exists_norm_le'

Premises used: Bornology.IsBounded.exists_norm_le'
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
⊢ IsBounded (s * t)

Tactic:
isBounded_iff_forall_norm_le'.2 ⟨Rs + Rt, ?_⟩

Premises used: Iff.mpr, isBounded_iff_forall_norm_le', HAdd.hAdd, Exists.intro
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
refine : ∀ x ∈ s * t, ‖x‖ ≤ Rs + Rt
⊢ IsBounded (s * t)

Tactic:
refine isBounded_iff_forall_norm_le'.2 ⟨Rs + Rt, ?_⟩

Premises used: Iff.mpr, isBounded_iff_forall_norm_le', HAdd.hAdd, Exists.intro
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
x : E
hx : x ∈ s
y : E
hy : y ∈ t
⊢ norm.{u_1} (E := E) ((fun (x1 x2 : E) ↦ x1 * x2) x y) ≤ Rs + Rt

Tactic:
norm_mul_le_of_le' (hRs x hx) (hRt y hy)

Premises used: norm_mul_le_of_le'
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
x : E
hx : x ∈ s
y : E
hy : y ∈ t
⊢ norm.{u_1} (E := E) ((fun (x1 x2 : E) ↦ x1 * x2) x y) ≤ Rs + Rt

Tactic:
exact norm_mul_le_of_le' (hRs x hx) (hRt y hy)

Premises used: norm_mul_le_of_le'
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
symm : IsBounded t ∨ IsBounded s
⊢ IsBounded s ∨ IsBounded t

Tactic:
symm
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
rwa rwa₁ rwa₂ rwa₃ : IsBounded (α := E) (image2 (fun (a b : E) ↦ a * b) s t)
⊢ IsBounded (α := E) (image2 (fun (a x : E) ↦ x * a) t s)

Tactic:
rwa [image2_swap]

Premises used: Set.image2_swap
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
⊢ IsBounded t ∨ IsBounded s

Tactic:
exact AntilipschitzWith.isBounded_of_image2_left _ (fun x => (isometry_mul_left x).antilipschitz)
    (by rwa [image2_swap])

Premises used: AntilipschitzWith.isBounded_of_image2_left, isometry_mul_left, Isometry.antilipschitz
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s : Set E
simp_rw : (∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C) → ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C
⊢ IsBounded s → IsBounded s⁻¹

Tactic:
simp_rw [isBounded_iff_forall_norm_le', ← image_inv_eq_inv, forall_mem_image, norm_inv']

Premises used: isBounded_iff_forall_norm_le', norm_inv', Set.image_inv_eq_inv, Set.forall_mem_image
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s : Set E
⊢ (∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C) → ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

Tactic:
id

Premises used: id
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s : Set E
⊢ (∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C) → ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
⊢ IsBounded (s / t)

Tactic:
div_eq_mul_inv s t ▸ hs.mul ht.inv

Premises used: Eq.rec, Bornology.IsBounded.inv, div_eq_mul_inv, Bornology.IsBounded.mul, Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
x : E
s : Set E
rw : infEDist x⁻¹ ((fun (x : E) ↦ x⁻¹) '' s) = infEDist x s
rw₁ rw₂ : infEDist x s = infEDist x s
⊢ infEDist x⁻¹ s⁻¹ = infEDist x s

Tactic:
rw [← image_inv_eq_inv, infEDist_image isometry_inv]

Premises used: Metric.infEDist_image, Set.image_inv_eq_inv, isometry_inv
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
x : E
s : Set E
rw : infEDist x⁻¹⁻¹ s⁻¹ = infEDist x s⁻¹
rw₁ rw₂ : infEDist x s⁻¹ = infEDist x s⁻¹
⊢ infEDist x⁻¹ s = infEDist x s⁻¹

Tactic:
rw [← infEDist_inv_inv, inv_inv]

Premises used: inv_inv, infEDist_inv_inv
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
x y : Set E
⊢ (↑1 : ENNReal) * ediam x + (↑1 : ENNReal) * ediam y = ediam x + ediam y

Tactic:
simp only [ENNReal.coe_one, one_mul]

Premises used: ENNReal.coe_one, one_mul
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
simp_rw :
  Eq.{u_1 + 1} (α := Set E) {x : E | infEDist x s < ENNReal.ofReal δ}⁻¹ {x : E | infEDist x⁻¹ s < ENNReal.ofReal δ}
⊢ (thickening δ s)⁻¹ = thickening δ s⁻¹

Tactic:
simp_rw [thickening, ← infEDist_inv]

Premises used: Metric.thickening, infEDist_inv
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ Eq.{u_1 + 1} (α := Set E) {x : E | infEDist x s < ENNReal.ofReal δ}⁻¹ {x : E | infEDist x⁻¹ s < ENNReal.ofReal δ}

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
simp_rw :
  Eq.{u_1 + 1} (α := Set E) {x : E | infEDist x s ≤ ENNReal.ofReal δ}⁻¹ {x : E | infEDist x⁻¹ s ≤ ENNReal.ofReal δ}
⊢ (cthickening δ s)⁻¹ = cthickening δ s⁻¹

Tactic:
simp_rw [cthickening, ← infEDist_inv]

Premises used: Metric.cthickening, infEDist_inv
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ Eq.{u_1 + 1} (α := Set E) {x : E | infEDist x s ≤ ENNReal.ofReal δ}⁻¹ {x : E | infEDist x⁻¹ s ≤ ENNReal.ofReal δ}

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ (ball x δ)⁻¹ = ball x⁻¹ δ

Tactic:
(IsometryEquiv.inv E).preimage_ball x δ

Premises used: IsometryEquiv.inv, IsometryEquiv.preimage_ball
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ (closedBall x δ)⁻¹ = closedBall x⁻¹ δ

Tactic:
(IsometryEquiv.inv E).preimage_closedBall x δ

Premises used: IsometryEquiv.inv, IsometryEquiv.preimage_closedBall
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * ball y δ = ball (x * y) δ

Tactic:
simp only [preimage_mul_ball, image_mul_left, singleton_mul, div_inv_eq_mul, mul_comm y x]

Premises used: Set.image_mul_left, mul_comm, div_inv_eq_mul, preimage_mul_ball, Set.singleton_mul
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
simp_rw : {x} * (ball y δ)⁻¹ = ball (x * y⁻¹) δ
simp_rw₁ : {x} * ball y⁻¹ δ = ball (x * y⁻¹) δ
⊢ {x} / ball y δ = ball (x / y) δ

Tactic:
simp_rw [div_eq_mul_inv, inv_ball, singleton_mul_ball]

Premises used: div_eq_mul_inv, inv_ball, singleton_mul_ball
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
rw : {y} * ball x δ = ball (x * y) δ
rw₁ : ball (y * x) δ = ball (x * y) δ
rw₂ rw₃ : ball (x * y) δ = ball (x * y) δ
⊢ ball x δ * {y} = ball (x * y) δ

Tactic:
rw [mul_comm, singleton_mul_ball, mul_comm y]

Premises used: mul_comm, singleton_mul_ball
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
simp_rw : ball x δ * {y}⁻¹ = ball (x * y⁻¹) δ
simp_rw₁ : ball x δ * {y⁻¹} = ball (x * y⁻¹) δ
⊢ ball x δ / {y} = ball (x / y) δ

Tactic:
simp_rw [div_eq_mul_inv, inv_singleton, ball_mul_singleton]

Premises used: ball_mul_singleton, div_eq_mul_inv, Set.inv_singleton
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ HMul.hMul (α := Set E) {x} (ball 1 δ) = ball x δ

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
rw : ball (x / 1) δ = ball x δ
rw₁ rw₂ : ball x δ = ball x δ
⊢ HDiv.hDiv (α := Set E) {x} (ball 1 δ) = ball x δ

Tactic:
rw [singleton_div_ball, div_one]

Premises used: singleton_div_ball, div_one
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ HMul.hMul (α := Set E) (ball 1 δ) {x} = ball x δ

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
rw : ball (1 / x) δ = ball x⁻¹ δ
rw₁ rw₂ : ball x⁻¹ δ = ball x⁻¹ δ
⊢ HDiv.hDiv (α := Set E) (ball 1 δ) {x} = ball x⁻¹ δ

Tactic:
rw [ball_div_singleton, one_div]

Premises used: ball_div_singleton, one_div
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
rw : ball (HSMul.hSMul (β := E) x 1) δ = ball x δ
rw₁ : ball (x * 1) δ = ball x δ
rw₂ rw₃ : ball x δ = ball x δ
⊢ HSMul.hSMul (β := Set E) x (ball 1 δ) = ball x δ

Tactic:
rw [smul_ball, smul_eq_mul, mul_one]

Premises used: Metric.smul_ball, smul_eq_mul, mul_one
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
simp_rw : (fun (x_1 : E) ↦ x * x_1) '' closedBall y δ = closedBall (x * y) δ
simp_rw₁ : (fun (a : E) ↦ x • a) '' closedBall y δ = closedBall (x • y) δ
simp_rw₂ : x • closedBall y δ = closedBall (x • y) δ
⊢ {x} * closedBall y δ = closedBall (x * y) δ

Tactic:
simp_rw [singleton_mul, ← smul_eq_mul, image_smul, smul_closedBall]

Premises used: Set.image_smul, Metric.smul_closedBall, smul_eq_mul, Set.singleton_mul
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
simp_rw : {x} * (closedBall y δ)⁻¹ = closedBall (x * y⁻¹) δ
simp_rw₁ : {x} * closedBall y⁻¹ δ = closedBall (x * y⁻¹) δ
⊢ {x} / closedBall y δ = closedBall (x / y) δ

Tactic:
simp_rw [div_eq_mul_inv, inv_closedBall, singleton_mul_closedBall]

Premises used: div_eq_mul_inv, singleton_mul_closedBall, inv_closedBall
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ closedBall x δ * {y} = closedBall (x * y) δ

Tactic:
simp [mul_comm _ {y}, mul_comm y]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ closedBall x δ / {y} = closedBall (x / y) δ

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ HMul.hMul (α := Set E) {x} (closedBall 1 δ) = closedBall x δ

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
rw : closedBall (x / 1) δ = closedBall x δ
rw₁ rw₂ : closedBall x δ = closedBall x δ
⊢ HDiv.hDiv (α := Set E) {x} (closedBall 1 δ) = closedBall x δ

Tactic:
rw [singleton_div_closedBall, div_one]

Premises used: singleton_div_closedBall, div_one
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ HMul.hMul (α := Set E) (closedBall 1 δ) {x} = closedBall x δ

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ HDiv.hDiv (α := Set E) (closedBall 1 δ) {x} = closedBall x⁻¹ δ

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ HSMul.hSMul (β := Set E) x (closedBall 1 δ) = closedBall x δ

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
rw : s * ball 1 δ = ⋃ x ∈ s, ball x δ
⊢ s * ball 1 δ = thickening δ s

Tactic:
rw [thickening_eq_biUnion_ball]

Premises used: Metric.thickening_eq_biUnion_ball
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ HMul.hMul (α := Set E) (⋃ i ∈ s, {i}) (ball 1 δ) = ⋃ i ∈ s, HMul.hMul (α := Set E) {i} (ball 1 δ)

Tactic:
iUnion₂_mul (fun x (_ : x ∈ s) => { x }) (ball (1 : E) δ)

Premises used: Metric.ball, Set.iUnion₂_mul, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
h : s = ⋃ i ∈ s, {i}
h₁ : ∀ x ∈ s, ball x δ = HMul.hMul (α := Set E) {x} (ball 1 δ)
⊢ s * ball 1 δ = ⋃ x ∈ s, ball x δ

Tactic:
convert! iUnion₂_mul (fun x (_ : x ∈ s) => { x }) (ball (1 : E) δ)

Premises used: Metric.ball, Set.iUnion₂_mul, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s = ⋃ i ∈ s, {i}

Tactic:
s.biUnion_of_singleton.symm

Premises used: Set.biUnion_of_singleton, Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s = ⋃ i ∈ s, {i}

Tactic:
exact s.biUnion_of_singleton.symm

Premises used: Set.biUnion_of_singleton, Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
h_1 : x ∈ s
h : ∀ (x_1 : E), x_1 ∈ ball x δ ↔ x_1 ∈ HMul.hMul (α := Set E) {x} (ball 1 δ)
⊢ ball x δ = HMul.hMul (α := Set E) {x} (ball 1 δ)

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
x_1 : E
h_1 : x_1 ∈ s
x : E
h : x ∈ ball x_1 δ ↔ x ∈ ball (x_1 * 1) δ
⊢ x ∈ ball x_1 δ ↔ x ∈ HMul.hMul (α := Set E) {x_1} (ball 1 δ)

Tactic:
simp_rw [singleton_mul_ball, mul_one]

Premises used: mul_one, singleton_mul_ball
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s / ball 1 δ = thickening δ s

Tactic:
simp [div_eq_mul_inv, mul_ball_one]

Premises used: div_eq_mul_inv, mul_ball_one
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
rw : s * ball 1 δ = thickening δ s
rw₁ rw₂ : thickening δ s = thickening δ s
⊢ ball 1 δ * s = thickening δ s

Tactic:
rw [mul_comm, mul_ball_one]

Premises used: mul_ball_one, mul_comm
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ ball 1 δ / s = thickening δ s⁻¹

Tactic:
simp [div_eq_mul_inv, ball_mul_one]

Premises used: ball_mul_one, div_eq_mul_inv
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
rw : s * HSMul.hSMul (β := Set E) x (ball 1 δ) = x • thickening δ s
rw₁ : x • (s * ball 1 δ) = x • thickening δ s
rw₂ rw₃ : x • thickening δ s = x • thickening δ s
⊢ s * ball x δ = x • thickening δ s

Tactic:
rw [← smul_ball_one, mul_smul_comm, mul_ball_one]

Premises used: mul_ball_one, mul_smul_comm, smul_ball_one
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ s / ball x δ = x⁻¹ • thickening δ s

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
rw : s * ball x δ = x • thickening δ s
rw₁ rw₂ : x • thickening δ s = x • thickening δ s
⊢ ball x δ * s = x • thickening δ s

Tactic:
rw [mul_comm, mul_ball]

Premises used: mul_ball, mul_comm
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ ball x δ / s = x • thickening δ s⁻¹

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
rw : s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ
⊢ s * closedBall 1 δ = cthickening δ s

Tactic:
rw [hs.cthickening_eq_biUnion_closedBall hδ]

Premises used: IsCompact.cthickening_eq_biUnion_closedBall
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
h : ∀ (x : E), x ∈ s * closedBall 1 δ ↔ Membership.mem (γ := Set E) (⋃ x ∈ s, closedBall x δ) x
⊢ s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ x ∈ s * closedBall 1 δ ↔ Membership.mem (γ := Set E) (⋃ x ∈ s, closedBall x δ) x

Tactic:
simp only [mem_mul, dist_eq_norm_div, exists_prop, mem_iUnion, mem_closedBall,
    ← eq_div_iff_mul_eq'', div_one, exists_eq_right]

Premises used: Set.mem_iUnion, exists_eq_right, eq_div_iff_mul_eq'', exists_prop, dist_eq_norm_div, Metric.mem_closedBall, div_one, Set.mem_mul
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s / closedBall 1 δ = cthickening δ s

Tactic:
simp [div_eq_mul_inv, hs.mul_closedBall_one hδ]

Premises used: IsCompact.mul_closedBall_one, div_eq_mul_inv
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
rw : s * closedBall 1 δ = cthickening δ s
rw₁ rw₂ : cthickening δ s = cthickening δ s
⊢ closedBall 1 δ * s = cthickening δ s

Tactic:
rw [mul_comm, hs.mul_closedBall_one hδ]

Premises used: IsCompact.mul_closedBall_one, mul_comm
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ closedBall 1 δ / s = cthickening δ s⁻¹

Tactic:
simp [div_eq_mul_inv, mul_comm, hs.inv.mul_closedBall_one hδ]

Premises used: IsCompact.mul_closedBall_one, div_eq_mul_inv, IsCompact.inv, mul_comm
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
rw : s * HSMul.hSMul (β := Set E) x (closedBall 1 δ) = x • cthickening δ s
rw₁ : x • (s * closedBall 1 δ) = x • cthickening δ s
rw₂ rw₃ : x • cthickening δ s = x • cthickening δ s
⊢ s * closedBall x δ = x • cthickening δ s

Tactic:
rw [← smul_closedBall_one, mul_smul_comm, hs.mul_closedBall_one hδ]

Premises used: IsCompact.mul_closedBall_one, smul_closedBall_one, mul_smul_comm
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ s / closedBall x δ = x⁻¹ • cthickening δ s

Tactic:
simp [div_eq_mul_inv, hs.mul_closedBall hδ]

Premises used: IsCompact.mul_closedBall, div_eq_mul_inv
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
rw : s * closedBall x δ = x • cthickening δ s
rw₁ rw₂ : x • cthickening δ s = x • cthickening δ s
⊢ closedBall x δ * s = x • cthickening δ s

Tactic:
rw [mul_comm, hs.mul_closedBall hδ]

Premises used: IsCompact.mul_closedBall, mul_comm
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ closedBall x δ * s = x • cthickening δ s

Tactic:
simp [hs.closedBall_mul hδ]

Premises used: IsCompact.closedBall_mul
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
⊢ Set.Nonempty.{u_1} (α := M) {m : M | (↑m : M ⧸ S) = x}

Tactic:
Quot.exists_rep x

Premises used: Set.Mem, setOf, Quot.exists_rep, Set.Nonempty, Quotient
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ Membership.mem (γ := Set M) {m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) 1} 1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
simp :
  ⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = x * y} : Type u_1)), dist 1 (↑y_1 : M) ≤
    HAdd.hAdd (α := ℝ) (⨅ (y : (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)), dist 1 (↑y : M))
      (⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)), dist 1 (↑y_1 : M))
⊢ infDist.{u_1} (α := M) 1 {m : M | (↑m : M ⧸ S) = x * y} ≤
    infDist.{u_1} (α := M) 1 {m : M | (↑m : M ⧸ S) = x} + infDist.{u_1} (α := M) 1 {m : M | (↑m : M ⧸ S) = y}

Tactic:
simp only [infDist_eq_iInf]

Premises used: Metric.infDist_eq_iInf
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
⊢ Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)

Tactic:
have := (norm_aux x).to_subtype
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
this : Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)
⊢ Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)

Tactic:
have := (norm_aux y).to_subtype
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
this_1 : Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)
this : Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)
⊢ ⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = x * y} : Type u_1)), dist 1 (↑y_1 : M) ≤
    HAdd.hAdd (α := ℝ) (⨅ (y : (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)), dist 1 (↑y : M))
      (⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)), dist 1 (↑y_1 : M))

Tactic:
le_ciInf_add_ciInf ?_

Premises used: le_ciInf_add_ciInf
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
this_1 : Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)
this : Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)
refine :
  ∀ (i : (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)) (j : (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)),
    ⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = x * y} : Type u_1)), dist 1 (↑y_1 : M) ≤ dist 1 (↑i : M) + dist 1 (↑j : M)
⊢ ⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = x * y} : Type u_1)), dist 1 (↑y_1 : M) ≤
    HAdd.hAdd (α := ℝ) (⨅ (y : (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)), dist 1 (↑y : M))
      (⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)), dist 1 (↑y_1 : M))

Tactic:
refine le_ciInf_add_ciInf ?_

Premises used: le_ciInf_add_ciInf
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
a : M
this_1 : Nonempty.{u_1 + 1} (↑{m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑a : M ⧸ S)} : Type u_1)
b : M
this : Nonempty.{u_1 + 1} (↑{m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑b : M ⧸ S)} : Type u_1)
⊢ ⨅ (y : (↑{m : M | (↑m : M ⧸ S) = HMul.hMul (α := M ⧸ S) (↑a : M ⧸ S) (↑b : M ⧸ S)} : Type u_1)), dist 1 (↑y : M) ≤
    dist 1
        (↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) {m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑a : M ⧸ S)} x) a ⋯) :
          M) +
      dist 1
        (↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) {m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑b : M ⧸ S)} x) b ⋯) :
          M)

Tactic:
ciInf_le_of_le ⟨0, forall_mem_range.2 fun _ ↦ dist_nonneg⟩ ⟨a * b, rfl⟩ ?_

Premises used: Iff.mpr, HMul.hMul, Set.forall_mem_range, dist_nonneg, ciInf_le_of_le, Subtype.mk, Exists.intro, OfNat.ofNat, rfl