awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ℝ≥0∞
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
⊢ enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ a
have pos : ∀ (hf : Summable f), enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ a
Tactic: by_cases hf : Summable f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ℝ≥0∞
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
pos : ∀ (hf : Summable f), enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ a
⊢ enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ a
have neg : ∀ (hf : ¬Summable f), enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ a
Tactic: by_cases hf : Summable f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a
have pos : ∀ (hf : Summable f), norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a
Tactic: by_cases hf : Summable f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
pos : ∀ (hf : Summable f), norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a
⊢ norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a
have neg : ∀ (hf : ¬Summable f), norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a
Tactic: by_cases hf : Summable f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a
have neg : 0 ≤ a
Tactic: rw [tsum_eq_zero_of_not_summable hf, norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖₊ ≤ g i
⊢ nnnorm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a
have simp : ∀ (hg : HasSum (fun (a : ι) ↦ (↑(g a) : ℝ)) (↑a : ℝ)) (h : ∀ (i : ι), ‖f i‖ ≤ (↑(g i) : ℝ)),
  norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ (↑a : ℝ)
Tactic: simp only [← NNReal.coe_le_coe, ← NNReal.hasSum_coe, coe_nnnorm] at *
Cleared hypotheses: hg, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Int (goal)
Goal:
α : Type u_1
m n : ℤ
⊢ dist m n = norm (E := ℝ) (↑(-m + n) : ℝ)
have simp : |HSub.hSub (α := ℝ) (↑m : ℝ) (↑n : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑m : ℝ)) (↑n : ℝ)|
Tactic: simp only [dist_eq, norm, cast_add, cast_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Int (goal)
Goal:
α : Type u_1
m n : ℤ
⊢ |HSub.hSub (α := ℝ) (↑m : ℝ) (↑n : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑m : ℝ)) (↑n : ℝ)|
have rw : |HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑m : ℝ)) (↑n : ℝ)|
Tactic: rw [abs_sub_comm, neg_add_eq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Int (goal)
Goal:
α : Type u_1
m n : ℤ
rw : |HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑m : ℝ)) (↑n : ℝ)|
⊢ |HSub.hSub (α := ℝ) (↑m : ℝ) (↑n : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑m : ℝ)) (↑n : ℝ)|
have rw₁ : |HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)| = |HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)|
Tactic: rw [abs_sub_comm, neg_add_eq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Int (goal)
Goal:
z : ℤ
c : ℝ≥0
⊢ |z| ≤ (↑⌊c⌋₊ : ℤ) ↔ ‖z‖₊ ≤ c
have rw : LE.le (α := ℤ) (↑z.natAbs : ℤ) (↑⌊c⌋₊ : ℤ) ↔ ‖z‖₊ ≤ c
Tactic: rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff zero_le, NNReal.natCast_natAbs z]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Int (goal)
Goal:
z : ℤ
c : ℝ≥0
rw : LE.le (α := ℤ) (↑z.natAbs : ℤ) (↑⌊c⌋₊ : ℤ) ↔ ‖z‖₊ ≤ c
⊢ |z| ≤ (↑⌊c⌋₊ : ℤ) ↔ ‖z‖₊ ≤ c
have rw₁ : z.natAbs ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c
Tactic: rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff zero_le, NNReal.natCast_natAbs z]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Int (goal)
Goal:
z : ℤ
c : ℝ≥0
rw : LE.le (α := ℤ) (↑z.natAbs : ℤ) (↑⌊c⌋₊ : ℤ) ↔ ‖z‖₊ ≤ c
rw₁ : z.natAbs ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c
⊢ |z| ≤ (↑⌊c⌋₊ : ℤ) ↔ ‖z‖₊ ≤ c
have rw₂ : (↑z.natAbs : ℝ≥0) ≤ c ↔ ‖z‖₊ ≤ c
Tactic: rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff zero_le, NNReal.natCast_natAbs z]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Int (goal)
Goal:
z : ℤ
c : ℝ≥0
rw : LE.le (α := ℤ) (↑z.natAbs : ℤ) (↑⌊c⌋₊ : ℤ) ↔ ‖z‖₊ ≤ c
rw₁ : z.natAbs ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c
rw₂ : (↑z.natAbs : ℝ≥0) ≤ c ↔ ‖z‖₊ ≤ c
⊢ |z| ≤ (↑⌊c⌋₊ : ℤ) ↔ ‖z‖₊ ≤ c
have rw₃ : ‖z‖₊ ≤ c ↔ ‖z‖₊ ≤ c
Tactic: rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff zero_le, NNReal.natCast_natAbs z]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Int (goal)
Goal:
α : Type u_1
inst : SeminormedCommGroup α
n : ℤ
a : α
⊢ ‖a ^ n‖ ≤ ‖n‖ * ‖a‖
have inl : ∀ (n : ℕ), ‖HPow.hPow (β := ℤ) a (↑n : ℤ)‖ ≤ norm (E := ℤ) (↑n : ℤ) * ‖a‖
Tactic: rcases n.eq_nat_or_neg with ⟨n, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Int (goal)
Goal:
α : Type u_1
inst : SeminormedCommGroup α
n : ℤ
a : α
inl : ∀ (n : ℕ), ‖HPow.hPow (β := ℤ) a (↑n : ℤ)‖ ≤ norm (E := ℤ) (↑n : ℤ) * ‖a‖
⊢ ‖a ^ n‖ ≤ ‖n‖ * ‖a‖
have inr : ∀ (n : ℕ), ‖HPow.hPow (β := ℤ) a (-(↑n : ℤ))‖ ≤ norm (E := ℤ) (-(↑n : ℤ)) * ‖a‖
Tactic: rcases n.eq_nat_or_neg with ⟨n, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.NullSubmodule (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
⊢ Membership.mem (γ := Set M) {x : M | ‖x‖ = 0} (x * y)
have apply : ‖x * y‖ ≤ 0
Tactic: apply le_antisymm _ (norm_nonneg' _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.NullSubmodule (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
⊢ ‖x * y‖ ≤ 0
have refine : ‖x‖ + ‖y‖ = 0
Tactic: refine (norm_mul_le' x y).trans_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.NullSubmodule (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
⊢ ‖x‖ + ‖y‖ = 0
have rw : 0 + ‖y‖ = 0
Tactic: rw [hx, hy, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.NullSubmodule (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
rw : 0 + ‖y‖ = 0
⊢ ‖x‖ + ‖y‖ = 0
have rw₁ : HAdd.hAdd (α := ℝ) 0 0 = 0
Tactic: rw [hx, hy, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.NullSubmodule (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
rw : 0 + ‖y‖ = 0
rw₁ : HAdd.hAdd (α := ℝ) 0 0 = 0
⊢ ‖x‖ + ‖y‖ = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [hx, hy, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.NullSubmodule (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
⊢ c • x ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (nullAddSubgroup E)))
have apply : ‖c • x‖ ≤ 0
Tactic: apply le_antisymm _ (norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.NullSubmodule (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
⊢ ‖c • x‖ ≤ 0
have refine : ‖c‖ * ‖x‖ = 0
Tactic: refine (norm_smul_le _ _).trans_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.NullSubmodule (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
⊢ ‖c‖ * ‖x‖ = 0
have rw : ‖c‖ * 0 = 0
Tactic: rw [hx, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.NullSubmodule (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
rw : ‖c‖ * 0 = 0
⊢ ‖c‖ * ‖x‖ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [hx, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
⊢ IsBounded (s * t)
have obtain : ∀ (Rs : ℝ) (hRs : ∀ x ∈ s, ‖x‖ ≤ Rs), IsBounded (s * t)
Tactic: obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
⊢ IsBounded (s * t)
have obtain : ∀ (Rt : ℝ) (hRt : ∀ x ∈ t, ‖x‖ ≤ Rt), IsBounded (s * t)
Tactic: obtain ⟨Rt, hRt⟩ : ∃ R, ∀ x ∈ t, ‖x‖ ≤ R := ht.exists_norm_le'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
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)
have refine : ∀ x ∈ s * t, ‖x‖ ≤ Rs + Rt
Tactic: refine isBounded_iff_forall_norm_le'.2 ⟨Rs + Rt, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
⊢ IsBounded s ∨ IsBounded t
have symm : IsBounded t ∨ IsBounded s
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
⊢ IsBounded (α := E) (image2 (fun (a x : E) ↦ x * a) t s)
have rwa : IsBounded (α := E) (image2 (fun (a b : E) ↦ a * b) s t)
Tactic: rwa [image2_swap]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedGroup E
s : Set E
⊢ IsBounded s → IsBounded s⁻¹
have simp_rw : (∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C) → ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C
Tactic: simp_rw [isBounded_iff_forall_norm_le', ← image_inv_eq_inv, forall_mem_image, norm_inv']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
x : E
s : Set E
⊢ infEDist x⁻¹ s⁻¹ = infEDist x s
have rw : infEDist x⁻¹ ((fun (x : E) ↦ x⁻¹) '' s) = infEDist x s
Tactic: rw [← image_inv_eq_inv, infEDist_image isometry_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
x : E
s : Set E
rw : infEDist x⁻¹ ((fun (x : E) ↦ x⁻¹) '' s) = infEDist x s
⊢ infEDist x⁻¹ s⁻¹ = infEDist x s
have rw₁ : infEDist x s = infEDist x s
Tactic: rw [← image_inv_eq_inv, infEDist_image isometry_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
x : E
s : Set E
⊢ infEDist x⁻¹ s = infEDist x s⁻¹
have rw : infEDist x⁻¹⁻¹ s⁻¹ = infEDist x s⁻¹
Tactic: rw [← infEDist_inv_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
x : E
s : Set E
rw : infEDist x⁻¹⁻¹ s⁻¹ = infEDist x s⁻¹
⊢ infEDist x⁻¹ s = infEDist x s⁻¹
have rw₁ : infEDist x s⁻¹ = infEDist x s⁻¹
Tactic: rw [← infEDist_inv_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ (thickening δ s)⁻¹ = thickening δ s⁻¹
have simp_rw : Eq.{u_1 + 1} (α := Set E) {x : E | infEDist x s < ENNReal.ofReal δ}⁻¹ {x : E | infEDist x⁻¹ s < ENNReal.ofReal δ}
Tactic: simp_rw [thickening, ← infEDist_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ (cthickening δ s)⁻¹ = cthickening δ s⁻¹
have simp_rw : Eq.{u_1 + 1} (α := Set E) {x : E | infEDist x s ≤ ENNReal.ofReal δ}⁻¹ {x : E | infEDist x⁻¹ s ≤ ENNReal.ofReal δ}
Tactic: simp_rw [cthickening, ← infEDist_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} / ball y δ = ball (x / y) δ
have simp_rw : {x} * (ball y δ)⁻¹ = ball (x * y⁻¹) δ
Tactic: simp_rw [div_eq_mul_inv, inv_ball, singleton_mul_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
simp_rw : {x} * (ball y δ)⁻¹ = ball (x * y⁻¹) δ
⊢ {x} / ball y δ = ball (x / y) δ
have simp_rw₁ : {x} * ball y⁻¹ δ = ball (x * y⁻¹) δ
Tactic: simp_rw [div_eq_mul_inv, inv_ball, singleton_mul_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ ball x δ * {y} = ball (x * y) δ
have rw : {y} * ball x δ = ball (x * y) δ
Tactic: rw [mul_comm, singleton_mul_ball, mul_comm y]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
rw : {y} * ball x δ = ball (x * y) δ
⊢ ball x δ * {y} = ball (x * y) δ
have rw₁ : ball (y * x) δ = ball (x * y) δ
Tactic: rw [mul_comm, singleton_mul_ball, mul_comm y]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
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) δ
⊢ ball x δ * {y} = ball (x * y) δ
have rw₂ : ball (x * y) δ = ball (x * y) δ
Tactic: rw [mul_comm, singleton_mul_ball, mul_comm y]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ ball x δ / {y} = ball (x / y) δ
have simp_rw : ball x δ * {y}⁻¹ = ball (x * y⁻¹) δ
Tactic: simp_rw [div_eq_mul_inv, inv_singleton, ball_mul_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
simp_rw : ball x δ * {y}⁻¹ = ball (x * y⁻¹) δ
⊢ ball x δ / {y} = ball (x / y) δ
have simp_rw₁ : ball x δ * {y⁻¹} = ball (x * y⁻¹) δ
Tactic: simp_rw [div_eq_mul_inv, inv_singleton, ball_mul_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ HDiv.hDiv (α := Set E) {x} (ball 1 δ) = ball x δ
have rw : ball (x / 1) δ = ball x δ
Tactic: rw [singleton_div_ball, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
rw : ball (x / 1) δ = ball x δ
⊢ HDiv.hDiv (α := Set E) {x} (ball 1 δ) = ball x δ
have rw₁ : ball x δ = ball x δ
Tactic: rw [singleton_div_ball, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ HDiv.hDiv (α := Set E) (ball 1 δ) {x} = ball x⁻¹ δ
have rw : ball (1 / x) δ = ball x⁻¹ δ
Tactic: rw [ball_div_singleton, one_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
rw : ball (1 / x) δ = ball x⁻¹ δ
⊢ HDiv.hDiv (α := Set E) (ball 1 δ) {x} = ball x⁻¹ δ
have rw₁ : ball x⁻¹ δ = ball x⁻¹ δ
Tactic: rw [ball_div_singleton, one_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ HSMul.hSMul (β := Set E) x (ball 1 δ) = ball x δ
have rw : ball (HSMul.hSMul (β := E) x 1) δ = ball x δ
Tactic: rw [smul_ball, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
rw : ball (HSMul.hSMul (β := E) x 1) δ = ball x δ
⊢ HSMul.hSMul (β := Set E) x (ball 1 δ) = ball x δ
have rw₁ : ball (x * 1) δ = ball x δ
Tactic: rw [smul_ball, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
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 δ
⊢ HSMul.hSMul (β := Set E) x (ball 1 δ) = ball x δ
have rw₂ : ball x δ = ball x δ
Tactic: rw [smul_ball, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * closedBall y δ = closedBall (x * y) δ
have simp_rw : (fun (x_1 : E) ↦ x * x_1) '' closedBall y δ = closedBall (x * y) δ
Tactic: simp_rw [singleton_mul, ← smul_eq_mul, image_smul, smul_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
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) δ
⊢ {x} * closedBall y δ = closedBall (x * y) δ
have simp_rw₁ : (fun (a : E) ↦ x • a) '' closedBall y δ = closedBall (x • y) δ
Tactic: simp_rw [singleton_mul, ← smul_eq_mul, image_smul, smul_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
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) δ
⊢ {x} * closedBall y δ = closedBall (x * y) δ
have simp_rw₂ : x • closedBall y δ = closedBall (x • y) δ
Tactic: simp_rw [singleton_mul, ← smul_eq_mul, image_smul, smul_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} / closedBall y δ = closedBall (x / y) δ
have simp_rw : {x} * (closedBall y δ)⁻¹ = closedBall (x * y⁻¹) δ
Tactic: simp_rw [div_eq_mul_inv, inv_closedBall, singleton_mul_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x y : E
simp_rw : {x} * (closedBall y δ)⁻¹ = closedBall (x * y⁻¹) δ
⊢ {x} / closedBall y δ = closedBall (x / y) δ
have simp_rw₁ : {x} * closedBall y⁻¹ δ = closedBall (x * y⁻¹) δ
Tactic: simp_rw [div_eq_mul_inv, inv_closedBall, singleton_mul_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
⊢ HDiv.hDiv (α := Set E) {x} (closedBall 1 δ) = closedBall x δ
have rw : closedBall (x / 1) δ = closedBall x δ
Tactic: rw [singleton_div_closedBall, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
x : E
rw : closedBall (x / 1) δ = closedBall x δ
⊢ HDiv.hDiv (α := Set E) {x} (closedBall 1 δ) = closedBall x δ
have rw₁ : closedBall x δ = closedBall x δ
Tactic: rw [singleton_div_closedBall, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s * ball 1 δ = thickening δ s
have rw : s * ball 1 δ = ⋃ x ∈ s, ball x δ
Tactic: rw [thickening_eq_biUnion_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s * ball 1 δ = ⋃ x ∈ s, ball x δ
have h : s = ⋃ i ∈ s, {i}
Tactic: convert! iUnion₂_mul (fun x (_ : x ∈ s) => { x }) (ball (1 : E) δ)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
h : s = ⋃ i ∈ s, {i}
⊢ s * ball 1 δ = ⋃ x ∈ s, ball x δ
have h₁ : ∀ x ∈ s, ball x δ = HMul.hMul (α := Set E) {x} (ball 1 δ)
Tactic: convert! iUnion₂_mul (fun x (_ : x ∈ s) => { x }) (ball (1 : E) δ)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
h : x ∈ s
⊢ ball x δ = HMul.hMul (α := Set E) {x} (ball 1 δ)
have h : ∀ (x_1 : E), x_1 ∈ ball x δ ↔ x_1 ∈ HMul.hMul (α := Set E) {x} (ball 1 δ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
x_1 : E
h : x_1 ∈ s
x : E
⊢ x ∈ ball x_1 δ ↔ x ∈ HMul.hMul (α := Set E) {x_1} (ball 1 δ)
have h : x ∈ ball x_1 δ ↔ x ∈ ball (x_1 * 1) δ
Tactic: simp_rw [singleton_mul_ball, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ ball 1 δ * s = thickening δ s
have rw : s * ball 1 δ = thickening δ s
Tactic: rw [mul_comm, mul_ball_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
rw : s * ball 1 δ = thickening δ s
⊢ ball 1 δ * s = thickening δ s
have rw₁ : thickening δ s = thickening δ s
Tactic: rw [mul_comm, mul_ball_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ s * ball x δ = x • thickening δ s
have rw : s * HSMul.hSMul (β := Set E) x (ball 1 δ) = x • thickening δ s
Tactic: rw [← smul_ball_one, mul_smul_comm, mul_ball_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
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
⊢ s * ball x δ = x • thickening δ s
have rw₁ : x • (s * ball 1 δ) = x • thickening δ s
Tactic: rw [← smul_ball_one, mul_smul_comm, mul_ball_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
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
⊢ s * ball x δ = x • thickening δ s
have rw₂ : x • thickening δ s = x • thickening δ s
Tactic: rw [← smul_ball_one, mul_smul_comm, mul_ball_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ ball x δ * s = x • thickening δ s
have rw : s * ball x δ = x • thickening δ s
Tactic: rw [mul_comm, mul_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
rw : s * ball x δ = x • thickening δ s
⊢ ball x δ * s = x • thickening δ s
have rw₁ : x • thickening δ s = x • thickening δ s
Tactic: rw [mul_comm, mul_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = cthickening δ s
have rw : s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ
Tactic: rw [hs.cthickening_eq_biUnion_closedBall hδ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ
have h : ∀ (x : E), x ∈ s * closedBall 1 δ ↔ Membership.mem (γ := Set E) (⋃ x ∈ s, closedBall x δ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ closedBall 1 δ * s = cthickening δ s
have rw : s * closedBall 1 δ = cthickening δ s
Tactic: rw [mul_comm, hs.mul_closedBall_one hδ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
rw : s * closedBall 1 δ = cthickening δ s
⊢ closedBall 1 δ * s = cthickening δ s
have rw₁ : cthickening δ s = cthickening δ s
Tactic: rw [mul_comm, hs.mul_closedBall_one hδ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ s * closedBall x δ = x • cthickening δ s
have rw : s * HSMul.hSMul (β := Set E) x (closedBall 1 δ) = x • cthickening δ s
Tactic: rw [← smul_closedBall_one, mul_smul_comm, hs.mul_closedBall_one hδ]