awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
inst_1 : Subsingleton E
a : E
⊢ ‖a‖ = 0
have rw : norm.{u_5} (E := E) 1 = 0
Tactic: rw [Subsingleton.elim a 1, norm_one']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
inst_1 : Subsingleton E
a : E
rw : norm.{u_5} (E := E) 1 = 0
⊢ ‖a‖ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [Subsingleton.elim a 1, norm_one']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖v‖ + ‖u / v‖
have rw : ‖u‖ ≤ ‖u / v‖ + ‖v‖
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖u / v‖ + ‖v‖
have refine : ‖u / v * v‖ = ‖u‖
Tactic: refine (norm_mul_le' _ _).trans_eq' ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖u / v * v‖ = ‖u‖
have rw : ‖u‖ = ‖u‖
Tactic: rw [div_mul_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖v‖ + ‖u⁻¹ * v‖
have rw : ‖u⁻¹‖ ≤ ‖u⁻¹ * v‖ + ‖v⁻¹‖
Tactic: rw [add_comm, ← norm_inv' v, ← norm_inv' u]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖u⁻¹‖ ≤ ‖u⁻¹ * v‖ + ‖v⁻¹‖
have refine : ‖u⁻¹ * v * v⁻¹‖ = ‖u⁻¹‖
Tactic: refine (norm_mul_le' _ _).trans_eq' ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖v‖ ≤ ‖u‖ + ‖u / v‖
have rw : ‖v‖ ≤ ‖u‖ + ‖v / u‖
Tactic: rw [norm_div_rev]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖u‖ = ‖u * v / v‖
have rw : ‖u‖ = ‖u‖
Tactic: rw [mul_div_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖v‖ = ‖u⁻¹ * (u * v)‖
have rw : ‖v‖ = ‖u⁻¹ * u * v‖
Tactic: rw [← mul_assoc, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
rw : ‖v‖ = ‖u⁻¹ * u * v‖
⊢ ‖v‖ = ‖u⁻¹ * (u * v)‖
have rw₁ : ‖v‖ = ‖1 * v‖
Tactic: rw [← mul_assoc, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
rw : ‖v‖ = ‖u⁻¹ * u * v‖
rw₁ : ‖v‖ = ‖1 * v‖
⊢ ‖v‖ = ‖u⁻¹ * (u * v)‖
have rw₂ : ‖v‖ = ‖v‖
Tactic: rw [← mul_assoc, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖u⁻¹‖ + ‖u * v‖ = ‖u * v‖ + ‖u‖
have rw : ‖u‖ + ‖u * v‖ = ‖u * v‖ + ‖u‖
Tactic: rw [norm_inv', add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
rw : ‖u‖ + ‖u * v‖ = ‖u * v‖ + ‖u‖
⊢ ‖u⁻¹‖ + ‖u * v‖ = ‖u * v‖ + ‖u‖
have rw₁ : ‖u * v‖ + ‖u‖ = ‖u * v‖ + ‖u‖
Tactic: rw [norm_inv', add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x * y‖ = ‖y‖
have apply : ‖x * y‖ ≤ ‖y‖
Tactic: apply le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖x‖ = 0
apply : ‖x * y‖ ≤ ‖y‖
⊢ ‖x * y‖ = ‖y‖
have apply₁ : ‖y‖ ≤ ‖x * y‖
Tactic: apply le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x * y‖ = ‖x‖
have apply : ‖x * y‖ ≤ ‖x‖
Tactic: apply le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖y‖ = 0
apply : ‖x * y‖ ≤ ‖x‖
⊢ ‖x * y‖ = ‖x‖
have apply₁ : ‖x‖ ≤ ‖x * y‖
Tactic: apply le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x / y‖ = ‖y‖
have rw : ‖x * y⁻¹‖ = ‖y‖
Tactic: rw [div_eq_mul_inv, norm_mul_eq_norm_right _ h, norm_inv']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖x‖ = 0
rw : ‖x * y⁻¹‖ = ‖y‖
⊢ ‖x / y‖ = ‖y‖
have rw₁ : ‖y⁻¹‖ = ‖y‖
Tactic: rw [div_eq_mul_inv, norm_mul_eq_norm_right _ h, norm_inv']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖x‖ = 0
rw : ‖x * y⁻¹‖ = ‖y‖
rw₁ : ‖y⁻¹‖ = ‖y‖
⊢ ‖x / y‖ = ‖y‖
have rw₂ : ‖y‖ = ‖y‖
Tactic: rw [div_eq_mul_inv, norm_mul_eq_norm_right _ h, norm_inv']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x / y‖ = ‖x‖
have h₁ : ‖y⁻¹‖ = 0
Tactic: rw [div_eq_mul_inv, norm_mul_eq_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖b⁻¹ * a‖ < r
have rw : dist b a < r ↔ ‖b⁻¹ * a‖ < r
Tactic: rw [mem_ball, dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
rw : dist b a < r ↔ ‖b⁻¹ * a‖ < r
⊢ b ∈ ball a r ↔ ‖b⁻¹ * a‖ < r
have rw₁ : ‖b⁻¹ * a‖ < r ↔ ‖b⁻¹ * a‖ < r
Tactic: rw [mem_ball, dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖a⁻¹ * b‖ < r
have rw : dist a b < r ↔ ‖a⁻¹ * b‖ < r
Tactic: rw [mem_ball', dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
rw : dist a b < r ↔ ‖a⁻¹ * b‖ < r
⊢ b ∈ ball a r ↔ ‖a⁻¹ * b‖ < r
have rw₁ : ‖a⁻¹ * b‖ < r ↔ ‖a⁻¹ * b‖ < r
Tactic: rw [mem_ball', dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
r : ℝ
⊢ Membership.mem (γ := Set E) (ball 1 r) a ↔ ‖a‖ < r
have rw : dist a 1 < r ↔ ‖a‖ < r
Tactic: rw [mem_ball, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
r : ℝ
rw : dist a 1 < r ↔ ‖a‖ < r
⊢ Membership.mem (γ := Set E) (ball 1 r) a ↔ ‖a‖ < r
have rw₁ : ‖a‖ < r ↔ ‖a‖ < r
Tactic: rw [mem_ball, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖b⁻¹ * a‖ ≤ r
have rw : dist b a ≤ r ↔ ‖b⁻¹ * a‖ ≤ r
Tactic: rw [mem_closedBall, dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
rw : dist b a ≤ r ↔ ‖b⁻¹ * a‖ ≤ r
⊢ b ∈ closedBall a r ↔ ‖b⁻¹ * a‖ ≤ r
have rw₁ : ‖b⁻¹ * a‖ ≤ r ↔ ‖b⁻¹ * a‖ ≤ r
Tactic: rw [mem_closedBall, dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
r : ℝ
⊢ Membership.mem (γ := Set E) (closedBall 1 r) a ↔ ‖a‖ ≤ r
have rw : dist a 1 ≤ r ↔ ‖a‖ ≤ r
Tactic: rw [mem_closedBall, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
r : ℝ
rw : dist a 1 ≤ r ↔ ‖a‖ ≤ r
⊢ Membership.mem (γ := Set E) (closedBall 1 r) a ↔ ‖a‖ ≤ r
have rw₁ : ‖a‖ ≤ r ↔ ‖a‖ ≤ r
Tactic: rw [mem_closedBall, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖a⁻¹ * b‖ ≤ r
have rw : dist a b ≤ r ↔ ‖a⁻¹ * b‖ ≤ r
Tactic: rw [mem_closedBall', dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
rw : dist a b ≤ r ↔ ‖a⁻¹ * b‖ ≤ r
⊢ b ∈ closedBall a r ↔ ‖a⁻¹ * b‖ ≤ r
have rw₁ : ‖a⁻¹ * b‖ ≤ r ↔ ‖a⁻¹ * b‖ ≤ r
Tactic: rw [mem_closedBall', dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_8
inst : SeminormedCommGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * min ‖u‖ ‖v‖
have rw : ‖u * v‖ - ‖u / v‖ ≤ min (2 * ‖u‖) (2 * ‖v‖)
Tactic: rw [mul_min_of_nonneg _ _ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_8
inst : SeminormedCommGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ min (2 * ‖u‖) (2 * ‖v‖)
have refine : ‖u * v‖ - ‖u / v‖ ≤ 2 * ‖u‖
Tactic: refine le_min ?_ (norm_mul_sub_norm_div_le_two_mul u v)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_8
inst : SeminormedCommGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * ‖u‖
have rw : ‖v * u‖ - ‖v / u‖ ≤ 2 * ‖u‖
Tactic: rw [norm_div_rev, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
f : E → F
x : E
y : F
⊢ Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x'⁻¹ * x‖ < δ → ‖(f x')⁻¹ * y‖ < ε
have simp_rw : (∀ ε > 0, ∃ δ > 0, ∀ ⦃x_1 : E⦄, dist x_1 x < δ → dist (f x_1) y < ε) ↔
  ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x'⁻¹ * x‖ < δ → ‖(f x')⁻¹ * y‖ < ε
Tactic: simp_rw [Metric.tendsto_nhds_nhds, dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
x : E
⊢ (𝓝 x).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {y : E | ‖y⁻¹ * x‖ < ε}
have simp_rw : (𝓝 x).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ ball x ε
Tactic: simp_rw [← ball_eq_norm_inv_mul_lt]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ HasBasis.{u_5, 1} (α := E) (𝓝 1) (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {y : E | ‖y‖ < ε}
have h : Eq.{u_5 + 1} (α := ℝ → Set E) (fun (ε : ℝ) ↦ {y : E | ‖y‖ < ε}) fun (ε : ℝ) ↦ {y : E | ‖y⁻¹ * 1‖ < ε}
Tactic: convert! NormedGroup.nhds_basis_norm_lt (1 : E) using 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ (𝓤 E).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {p : E × E | ‖p.1⁻¹ * p.2‖ < ε}
have h : Eq.{u_5 + 1} (α := ℝ → Set (E × E)) (fun (ε : ℝ) ↦ {p : E × E | ‖p.1⁻¹ * p.2‖ < ε}) fun (ε : ℝ) ↦
  {p : E × E | dist p.1 p.2 < ε}
Tactic: convert! Metric.uniformity_basis_dist (α := E) using 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
⊢ ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖
have simp : ENNReal.ofReal ‖x‖ = ENNReal.ofReal ‖y‖ ↔ ‖x‖ = ‖y‖
Tactic: simp only [← ofReal_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
⊢ ENNReal.ofReal ‖x‖ = ENNReal.ofReal ‖y‖ ↔ ‖x‖ = ‖y‖
have refine : ∀ (h : ENNReal.ofReal ‖x‖ = ENNReal.ofReal ‖y‖), ‖x‖ = ‖y‖
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by congr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
⊢ ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖
have simp : ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖ ↔ ‖x‖ ≤ ‖y‖
Tactic: simp only [← ofReal_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
⊢ ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖ ↔ ‖x‖ ≤ ‖y‖
have refine : ∀ (h : ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖), ‖x‖ ≤ ‖y‖
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by gcongr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ edist 1 a = (↑‖a‖₊ : ℝ≥0∞)
have rw : (↑(nndist 1 a) : ℝ≥0∞) = (↑‖a‖₊ : ℝ≥0∞)
Tactic: rw [edist_nndist, nndist_one_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
rw : (↑(nndist 1 a) : ℝ≥0∞) = (↑‖a‖₊ : ℝ≥0∞)
⊢ edist 1 a = (↑‖a‖₊ : ℝ≥0∞)
have rw₁ : (↑‖a‖₊ : ℝ≥0∞) = (↑‖a‖₊ : ℝ≥0∞)
Tactic: rw [edist_nndist, nndist_one_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ edist (s.mulIndicator f x) (t.mulIndicator f x) = (↑‖(s ∆ t).mulIndicator f x‖₊ : ℝ≥0∞)
have rw : (↑(nndist (s.mulIndicator f x) (t.mulIndicator f x)) : ℝ≥0∞) = (↑‖(s ∆ t).mulIndicator f x‖₊ : ℝ≥0∞)
Tactic: rw [edist_nndist, nndist_mulIndicator]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
rw : (↑(nndist (s.mulIndicator f x) (t.mulIndicator f x)) : ℝ≥0∞) = (↑‖(s ∆ t).mulIndicator f x‖₊ : ℝ≥0∞)
⊢ edist (s.mulIndicator f x) (t.mulIndicator f x) = (↑‖(s ∆ t).mulIndicator f x‖₊ : ℝ≥0∞)
have rw₁ : (↑‖(s ∆ t).mulIndicator f x‖₊ : ℝ≥0∞) = (↑‖(s ∆ t).mulIndicator f x‖₊ : ℝ≥0∞)
Tactic: rw [edist_nndist, nndist_mulIndicator]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ NontrivialTopology E ↔ ∃ (x : E), ‖x‖₊ ≠ 0
have simp_rw : (∃ (x : E) (y : E), ¬‖x⁻¹ * y‖₊ = 0) ↔ ∃ (x : E), ‖x‖₊ ≠ 0
Tactic: simp_rw [TopologicalSpace.nontrivial_iff_exists_not_inseparable, Metric.inseparable_iff_nndist,
    nndist_eq_nnnorm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_8
inst : TopologicalSpace E
inst_1 : ESeminormedMonoid E
⊢ enorm.{u_8} (E := E) 1 = 0
have rw : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [ESeminormedMonoid.enorm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ edist a b = ‖a⁻¹ * b‖ₑ
have rw : ENNReal.ofReal (dist a b) = ‖a⁻¹ * b‖ₑ
Tactic: rw [edist_dist, dist_eq_norm_inv_mul, ofReal_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
rw : ENNReal.ofReal (dist a b) = ‖a⁻¹ * b‖ₑ
⊢ edist a b = ‖a⁻¹ * b‖ₑ
have rw₁ : ENNReal.ofReal ‖a⁻¹ * b‖ = ‖a⁻¹ * b‖ₑ
Tactic: rw [edist_dist, dist_eq_norm_inv_mul, ofReal_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
rw : ENNReal.ofReal (dist a b) = ‖a⁻¹ * b‖ₑ
rw₁ : ENNReal.ofReal ‖a⁻¹ * b‖ = ‖a⁻¹ * b‖ₑ
⊢ edist a b = ‖a⁻¹ * b‖ₑ
have rw₂ : ‖a⁻¹ * b‖ₑ = ‖a⁻¹ * b‖ₑ
Tactic: rw [edist_dist, dist_eq_norm_inv_mul, ofReal_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_8
inst : SeminormedGroup E
a b : E
⊢ ‖a / b‖ₑ = ‖b / a‖ₑ
have rw : ‖(a / b)⁻¹‖ₑ = ‖b / a‖ₑ
Tactic: rw [← enorm_inv', inv_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_8
inst : SeminormedGroup E
a b : E
rw : ‖(a / b)⁻¹‖ₑ = ‖b / a‖ₑ
⊢ ‖a / b‖ₑ = ‖b / a‖ₑ
have rw₁ : ‖b / a‖ₑ = ‖b / a‖ₑ
Tactic: rw [← enorm_inv', inv_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
r : ℝ≥0∞
⊢ Membership.mem (γ := Set E) (eball 1 r) a ↔ ‖a‖ₑ < r
have rw : edist a 1 < r ↔ ‖a‖ₑ < r
Tactic: rw [Metric.mem_eball, edist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
r : ℝ≥0∞
rw : edist a 1 < r ↔ ‖a‖ₑ < r
⊢ Membership.mem (γ := Set E) (eball 1 r) a ↔ ‖a‖ₑ < r
have rw₁ : ‖a‖ₑ < r ↔ ‖a‖ₑ < r
Tactic: rw [Metric.mem_eball, edist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : FunLike 𝓕 E F
inst_1 : Group E
inst_2 : SeminormedGroup F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
x y : E
⊢ dist x y = norm.{u_6} (E := F) ((f : (a : E) → F) (x⁻¹ * y) : F)
have simp : dist x y = dist.{u_6} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)
Tactic: simp only [map_mul, map_inv, ← dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
⊢ dist a b = ‖a / b‖
have rw : ‖b⁻¹ * a‖ = ‖a / b‖
Tactic: rw [dist_eq_norm_inv_mul', div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
rw : ‖b⁻¹ * a‖ = ‖a / b‖
⊢ dist a b = ‖a / b‖
have rw₁ : ‖b⁻¹ * a‖ = ‖b⁻¹ * a‖
Tactic: rw [dist_eq_norm_inv_mul', div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
⊢ dist a b = ‖b / a‖
have rw : ‖a⁻¹ * b‖ = ‖b / a‖
Tactic: rw [dist_eq_norm_inv_mul, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
rw : ‖a⁻¹ * b‖ = ‖b / a‖
⊢ dist a b = ‖b / a‖
have rw₁ : ‖a⁻¹ * b‖ = ‖a⁻¹ * b‖
Tactic: rw [dist_eq_norm_inv_mul, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
⊢ ‖a⁻¹ * b‖ = ‖a / b‖
have rw : dist a b = ‖a / b‖
Tactic: rw [← dist_eq_norm_inv_mul, dist_eq_norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
rw : dist a b = ‖a / b‖
⊢ ‖a⁻¹ * b‖ = ‖a / b‖
have rw₁ : ‖a / b‖ = ‖a / b‖
Tactic: rw [← dist_eq_norm_inv_mul, dist_eq_norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
⊢ edist a b = ‖a / b‖ₑ
have rw : ENNReal.ofReal (dist a b) = ‖a / b‖ₑ
Tactic: rw [edist_dist, dist_eq_norm_div, ofReal_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
rw : ENNReal.ofReal (dist a b) = ‖a / b‖ₑ
⊢ edist a b = ‖a / b‖ₑ
have rw₁ : ENNReal.ofReal ‖a / b‖ = ‖a / b‖ₑ
Tactic: rw [edist_dist, dist_eq_norm_div, ofReal_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
rw : ENNReal.ofReal (dist a b) = ‖a / b‖ₑ
rw₁ : ENNReal.ofReal ‖a / b‖ = ‖a / b‖ₑ
⊢ edist a b = ‖a / b‖ₑ
have rw₂ : ‖a / b‖ₑ = ‖a / b‖ₑ
Tactic: rw [edist_dist, dist_eq_norm_div, ofReal_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
x y : E
⊢ dist x⁻¹ y = dist x y⁻¹
have simp_rw : ‖x⁻¹⁻¹ * y‖ = ‖x⁻¹ * y⁻¹‖
Tactic: simp_rw [dist_eq_norm_inv_mul, ← norm_inv' (x⁻¹ * y⁻¹), mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
x y : E
simp_rw : ‖x⁻¹⁻¹ * y‖ = ‖x⁻¹ * y⁻¹‖
⊢ dist x⁻¹ y = dist x y⁻¹
have simp_rw₁ : ‖x⁻¹⁻¹ * y‖ = ‖(x⁻¹ * y⁻¹)⁻¹‖
Tactic: simp_rw [dist_eq_norm_inv_mul, ← norm_inv' (x⁻¹ * y⁻¹), mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
x y : E
simp_rw : ‖x⁻¹⁻¹ * y‖ = ‖x⁻¹ * y⁻¹‖
simp_rw₁ : ‖x⁻¹⁻¹ * y‖ = ‖(x⁻¹ * y⁻¹)⁻¹‖
⊢ dist x⁻¹ y = dist x y⁻¹
have simp_rw₂ : ‖x⁻¹⁻¹ * y‖ = ‖x⁻¹⁻¹ * y⁻¹⁻¹‖
Tactic: simp_rw [dist_eq_norm_inv_mul, ← norm_inv' (x⁻¹ * y⁻¹), mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (hypothesis)
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, dist (f b) (a b) ≤ d b
⊢ dist.{u_5} (α := E) (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b
have h₁ : ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b
Tactic: simp_rw [dist_eq_norm_inv_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b
⊢ dist.{u_5} (α := E) (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b
have rw : norm.{u_5} (E := E) (∏ x ∈ s, (f x)⁻¹ * a x) ≤ ∑ b ∈ s, d b
Tactic: rw [dist_eq_norm_inv_mul, ← Finset.prod_inv_distrib, ← Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
y : E
ε : ℝ
⊢ ball y ε = {x : E | ‖x / y‖ < ε}
have simp_rw : Eq.{u_5 + 1} (α := Set E) {x : E | ‖x⁻¹ * y‖ < ε} {x : E | ‖x / y‖ < ε}
Tactic: simp_rw [ball_eq_norm_inv_mul_lt, norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖b / a‖ < r
have rw : dist b a < r ↔ ‖b / a‖ < r
Tactic: rw [mem_ball, dist_eq_norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
rw : dist b a < r ↔ ‖b / a‖ < r
⊢ b ∈ ball a r ↔ ‖b / a‖ < r
have rw₁ : ‖b / a‖ < r ↔ ‖b / a‖ < r
Tactic: rw [mem_ball, dist_eq_norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖a / b‖ < r
have rw : dist a b < r ↔ ‖a / b‖ < r
Tactic: rw [mem_ball', dist_eq_norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
rw : dist a b < r ↔ ‖a / b‖ < r
⊢ b ∈ ball a r ↔ ‖a / b‖ < r
have rw₁ : ‖a / b‖ < r ↔ ‖a / b‖ < r
Tactic: rw [mem_ball', dist_eq_norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖b / a‖ ≤ r
have rw : dist b a ≤ r ↔ ‖b / a‖ ≤ r
Tactic: rw [mem_closedBall, dist_eq_norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
rw : dist b a ≤ r ↔ ‖b / a‖ ≤ r
⊢ b ∈ closedBall a r ↔ ‖b / a‖ ≤ r
have rw₁ : ‖b / a‖ ≤ r ↔ ‖b / a‖ ≤ r
Tactic: rw [mem_closedBall, dist_eq_norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖a / b‖ ≤ r
have rw : dist a b ≤ r ↔ ‖a / b‖ ≤ r
Tactic: rw [mem_closedBall', dist_eq_norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
rw : dist a b ≤ r ↔ ‖a / b‖ ≤ r
⊢ b ∈ closedBall a r ↔ ‖a / b‖ ≤ r
have rw₁ : ‖a / b‖ ≤ r ↔ ‖a / b‖ ≤ r
Tactic: rw [mem_closedBall', dist_eq_norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a * b ∈ ball a r ↔ ‖b‖ < r
have rw : ‖a * b / a‖ < r ↔ ‖b‖ < r
Tactic: rw [mem_ball_iff_norm'']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a * b ∈ closedBall a r ↔ ‖b‖ ≤ r
have rw : ‖a * b / a‖ ≤ r ↔ ‖b‖ ≤ r
Tactic: rw [mem_closedBall_iff_norm'']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun (x : E) ↦ b * x) ⁻¹' ball a r = ball (a / b) r
have h : ∀ (c : E), Membership.mem (γ := Set E) ((fun (x : E) ↦ b * x) ⁻¹' ball a r) c ↔ c ∈ ball (a / b) r
Tactic: ext c
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun (x : E) ↦ b * x) ⁻¹' closedBall a r = closedBall (a / b) r
have h : ∀ (c : E), Membership.mem (γ := Set E) ((fun (x : E) ↦ b * x) ⁻¹' closedBall a r) c ↔ c ∈ closedBall (a / b) r
Tactic: ext c
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun (x : E) ↦ b * x) ⁻¹' sphere a r = sphere (a / b) r
have h : ∀ (c : E), Membership.mem (γ := Set E) ((fun (x : E) ↦ b * x) ⁻¹' sphere a r) c ↔ c ∈ sphere (a / b) r
Tactic: ext c