awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)
have rw : b +ᵥ cthickening δ (Metric.closedBall a ε) = Metric.closedBall (a + b) (ε + δ)
Tactic: rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a,
    Metric.vadd_closedBall, vadd_eq_add, add_comm, add_comm δ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
rw : b +ᵥ cthickening δ (Metric.closedBall a ε) = Metric.closedBall (a + b) (ε + δ)
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)
have rw₁ : b +ᵥ Metric.closedBall a (δ + ε) = Metric.closedBall (a + b) (ε + δ)
Tactic: rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a,
    Metric.vadd_closedBall, vadd_eq_add, add_comm, add_comm δ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
rw : b +ᵥ cthickening δ (Metric.closedBall a ε) = Metric.closedBall (a + b) (ε + δ)
rw₁ : b +ᵥ Metric.closedBall a (δ + ε) = Metric.closedBall (a + b) (ε + δ)
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)
have rw₂ : Metric.closedBall (b +ᵥ a) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
Tactic: rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a,
    Metric.vadd_closedBall, vadd_eq_add, add_comm, add_comm δ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
rw : b +ᵥ cthickening δ (Metric.closedBall a ε) = Metric.closedBall (a + b) (ε + δ)
rw₁ : b +ᵥ Metric.closedBall a (δ + ε) = Metric.closedBall (a + b) (ε + δ)
rw₂ : Metric.closedBall (b +ᵥ a) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)
have rw₃ : Metric.closedBall (b + a) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
Tactic: rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a,
    Metric.vadd_closedBall, vadd_eq_add, add_comm, add_comm δ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
rw : b +ᵥ cthickening δ (Metric.closedBall a ε) = Metric.closedBall (a + b) (ε + δ)
rw₁ : b +ᵥ Metric.closedBall a (δ + ε) = Metric.closedBall (a + b) (ε + δ)
rw₂ : Metric.closedBall (b +ᵥ a) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
rw₃ : Metric.closedBall (b + a) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)
have rw₄ : Metric.closedBall (a + b) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
Tactic: rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a,
    Metric.vadd_closedBall, vadd_eq_add, add_comm, add_comm δ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
rw : b +ᵥ cthickening δ (Metric.closedBall a ε) = Metric.closedBall (a + b) (ε + δ)
rw₁ : b +ᵥ Metric.closedBall a (δ + ε) = Metric.closedBall (a + b) (ε + δ)
rw₂ : Metric.closedBall (b +ᵥ a) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
rw₃ : Metric.closedBall (b + a) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
rw₄ : Metric.closedBall (a + b) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)
have rw₅ : Metric.closedBall (a + b) (ε + δ) = Metric.closedBall (a + b) (ε + δ)
Tactic: rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a,
    Metric.vadd_closedBall, vadd_eq_add, add_comm, add_comm δ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
have rw : Metric.closedBall a ε + -Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
Tactic: rw [sub_eq_add_neg, neg_closedBall, closedBall_add_closedBall hε hδ, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
rw : Metric.closedBall a ε + -Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
⊢ Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
have rw₁ : Metric.closedBall a ε + Metric.closedBall (-b) δ = Metric.closedBall (a - b) (ε + δ)
Tactic: rw [sub_eq_add_neg, neg_closedBall, closedBall_add_closedBall hε hδ, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
rw : Metric.closedBall a ε + -Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
rw₁ : Metric.closedBall a ε + Metric.closedBall (-b) δ = Metric.closedBall (a - b) (ε + δ)
⊢ Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
have rw₂ : Metric.closedBall (a + -b) (ε + δ) = Metric.closedBall (a - b) (ε + δ)
Tactic: rw [sub_eq_add_neg, neg_closedBall, closedBall_add_closedBall hε hδ, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
rw : Metric.closedBall a ε + -Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
rw₁ : Metric.closedBall a ε + Metric.closedBall (-b) δ = Metric.closedBall (a - b) (ε + δ)
rw₂ : Metric.closedBall (a + -b) (ε + δ) = Metric.closedBall (a - b) (ε + δ)
⊢ Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
have rw₃ : Metric.closedBall (a + -b) (ε + δ) = Metric.closedBall (a + -b) (ε + δ)
Tactic: rw [sub_eq_add_neg, neg_closedBall, closedBall_add_closedBall hε hδ, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)
have inl : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (closedBall x r) =
  closedBall (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) (norm.{u_1} (E := 𝕜) 0 * r)
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
inl :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (closedBall x r) =
    closedBall (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) (norm.{u_1} (E := 𝕜) 0 * r)
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)
have inr : ∀ (hc : c ≠ 0), c • closedBall x r = closedBall (c • x) (‖c‖ * r)
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
⊢ HSMul.hSMul (β := Set E) c (closedBall 0 1) = closedBall 0 ‖c‖
have rw : closedBall (HSMul.hSMul (β := E) c 0) (‖c‖ * 1) = closedBall 0 ‖c‖
Tactic: rw [_root_.smul_closedBall _ _ zero_le_one, smul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
rw : closedBall (HSMul.hSMul (β := E) c 0) (‖c‖ * 1) = closedBall 0 ‖c‖
⊢ HSMul.hSMul (β := Set E) c (closedBall 0 1) = closedBall 0 ‖c‖
have rw₁ : Eq.{u_2 + 1} (α := Set E) (closedBall 0 (‖c‖ * 1)) (closedBall 0 ‖c‖)
Tactic: rw [_root_.smul_closedBall _ _ zero_le_one, smul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
rw : closedBall (HSMul.hSMul (β := E) c 0) (‖c‖ * 1) = closedBall 0 ‖c‖
rw₁ : Eq.{u_2 + 1} (α := Set E) (closedBall 0 (‖c‖ * 1)) (closedBall 0 ‖c‖)
⊢ HSMul.hSMul (β := Set E) c (closedBall 0 1) = closedBall 0 ‖c‖
have rw₂ : Eq.{u_2 + 1} (α := Set E) (closedBall 0 ‖c‖) (closedBall 0 ‖c‖)
Tactic: rw [_root_.smul_closedBall _ _ zero_le_one, smul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
⊢ HSMul.hSMul (β := Set E) r (closedBall 0 1) = closedBall 0 r
have rw : Eq.{u_2 + 1} (α := Set E) (closedBall 0 ‖r‖) (closedBall 0 r)
Tactic: rw [smul_unitClosedBall, Real.norm_of_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
rw : Eq.{u_2 + 1} (α := Set E) (closedBall 0 ‖r‖) (closedBall 0 r)
⊢ HSMul.hSMul (β := Set E) r (closedBall 0 1) = closedBall 0 r
have rw₁ : Eq.{u_2 + 1} (α := Set E) (closedBall 0 r) (closedBall 0 r)
Tactic: rw [smul_unitClosedBall, Real.norm_of_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)
have inl : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (sphere x r) =
  sphere (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) (norm.{u_1} (E := 𝕜) 0 * r)
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
inl :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (sphere x r) =
    sphere (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) (norm.{u_1} (E := 𝕜) 0 * r)
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)
have inr : ∀ (hc : c ≠ 0), c • sphere x r = sphere (c • x) (‖c‖ * r)
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
⊢ x +ᵥ HSMul.hSMul (β := Set E) r (ball 0 1) = ball x r
have rw : HVAdd.hVAdd (β := Set E) x (ball 0 r) = ball x r
Tactic: rw [smul_unitBall_of_pos hr, vadd_ball_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
rw : HVAdd.hVAdd (β := Set E) x (ball 0 r) = ball x r
⊢ x +ᵥ HSMul.hSMul (β := Set E) r (ball 0 1) = ball x r
have rw₁ : ball x r = ball x r
Tactic: rw [smul_unitBall_of_pos hr, vadd_ball_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
⊢ x +ᵥ HSMul.hSMul (β := Set E) r (closedBall 0 1) = closedBall x r
have rw : HVAdd.hVAdd (β := Set E) x (closedBall 0 ‖r‖) = closedBall x r
Tactic: rw [smul_unitClosedBall, Real.norm_of_nonneg hr, vadd_closedBall_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
rw : HVAdd.hVAdd (β := Set E) x (closedBall 0 ‖r‖) = closedBall x r
⊢ x +ᵥ HSMul.hSMul (β := Set E) r (closedBall 0 1) = closedBall x r
have rw₁ : HVAdd.hVAdd (β := Set E) x (closedBall 0 r) = closedBall x r
Tactic: rw [smul_unitClosedBall, Real.norm_of_nonneg hr, vadd_closedBall_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
rw : HVAdd.hVAdd (β := Set E) x (closedBall 0 ‖r‖) = closedBall x r
rw₁ : HVAdd.hVAdd (β := Set E) x (closedBall 0 r) = closedBall x r
⊢ x +ᵥ HSMul.hSMul (β := Set E) r (closedBall 0 1) = closedBall x r
have rw₂ : closedBall x r = closedBall x r
Tactic: rw [smul_unitClosedBall, Real.norm_of_nonneg hr, vadd_closedBall_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (hypothesis)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) {0}ᶜ x
⊢ (fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) ⋯ :
          { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
      ((fun (x : (↑{0}ᶜ : Type u_2)) ↦
          have this := ⋯;
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) ⋯,
            Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯))
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx)) =
    Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx
have this : 0 < ‖x‖
Tactic: have : 0 < ‖x‖ := by simpa using hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) {0}ᶜ x
this : 0 < ‖x‖
⊢ (fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) ⋯ :
          { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
      ((fun (x : (↑{0}ᶜ : Type u_2)) ↦
          have this := ⋯;
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) ⋯,
            Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯))
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx)) =
    Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx
have a : (↑((fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) sorry :
            { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
        ((fun (x : (↑{0}ᶜ : Type u_2)) ↦
            have this := sorry;
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) sorry,
              Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) sorry))
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx))) :
    E) =
  (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx) : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) {0}ᶜ x
this : 0 < ‖x‖
⊢ (↑((fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) ⋯ :
              { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
          ((fun (x : (↑{0}ᶜ : Type u_2)) ↦
              have this := ⋯;
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E))
                  ⋯,
                Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯))
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx))) :
      E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx) : E)
have a : (‖x‖ / r * (r * ‖x‖⁻¹)) • x = x
Tactic: simp only [smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) {0}ᶜ x
this : 0 < ‖x‖
⊢ (‖x‖ / r * (r * ‖x‖⁻¹)) • x = x
have a : HSMul.hSMul (α := ℝ) 1 x = x
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (hypothesis)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) (sphere 0 r) x
d : ℝ
hd : Membership.mem (γ := Set ℝ) (Ioi 0) d
⊢ (fun (x : (↑{0}ᶜ : Type u_2)) ↦
        have this := ⋯;
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) ⋯,
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯))
      ((fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) ⋯ :
            { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx,
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd)) =
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx,
      Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd)
have hd₁ : 0 < d
Tactic: rw [mem_Ioi] at hd
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) (sphere 0 r) x
d : ℝ
hd_1 : Membership.mem (γ := Set ℝ) (Ioi 0) d
hd : 0 < d
⊢ (fun (x : (↑{0}ᶜ : Type u_2)) ↦
        have this := ⋯;
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) ⋯,
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯))
      ((fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) ⋯ :
            { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx,
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd_1)) =
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx,
      Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd_1)
have rw : ∀ (hx_1 : ‖x‖ = r) (d : ℝ) (hd : Membership.mem (γ := Set ℝ) (Ioi 0) d) (hd_2 : 0 < d),
  (fun (x : (↑{0}ᶜ : Type u_2)) ↦
        have this := sorry;
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) sorry,
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) sorry))
      ((fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) sorry :
            { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx,
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd)) =
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx,
      Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd)
Tactic: rw [mem_sphere_zero_iff_norm] at hx
Cleared hypotheses: d, hd_1, hd
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun (x : (↑{0}ᶜ : Type u_2)) ↦
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) ⋯,
      Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯)
have funProp : ∀ (x : (↑{0}ᶜ : Type u_2)), ‖(↑x : E)‖ ≠ 0
Tactic: fun_prop (disch := simp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have rw : ∀ x ∈ U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V,
  U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V ∈ 𝓝 x
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have inr : ∀
  (this :
    ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
      Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
        (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V))
  (hx₀ : ¬0 < x),
  Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
Tactic: wlog hx₀ : 0 < x generalizing x U