awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
this : Continuous (Y := ℝ) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹
funProp : ∀ (x : E), Membership.mem (γ := Set E) univ x → √(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ≠ 0
funProp₁ : ∀ (x : ℝ), x ≠ 0
⊢ ContinuousOn (Y := E) (fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x) univ
have funProp₂ : ∀ (x : E), √(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ ContinuousOn (Y := E) (fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x) univ
have suffices : Continuous (Y := ℝ) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹
Tactic: suffices Continuous fun (x : E) => (√(1 + ‖x‖ ^ 2))⁻¹ by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
⊢ √(1 - HPow.hPow (β := ℕ) ‖y‖ 2) ≠ 0
have rw : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: rw [Real.sqrt_ne_zero']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ ContinuousOn (Y := E) (fun (y : E) ↦ (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y) (ball 0 1)
have this : ∀ (y : E), Membership.mem (γ := Set E) (ball 0 1) y → √(1 - HPow.hPow (β := ℕ) ‖y‖ 2) ≠ 0
Tactic: have : ∀ y ∈ ball (0 : E) 1, √(1 - ‖(y : E)‖ ^ 2) ≠ 0 := fun y hy ↦ by
      rw [Real.sqrt_ne_zero']
      nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ image.{u_1, u_2} (α := E)
      (⇑(Homeomorph.trans (Homeomorph.smulOfNeZero r ⋯) (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) :
        (a : E) → P)
      (ball 0 1) =
    ball c r
have change : image.{u_1, u_2} (α := E) (Function.comp (β := E) (⇑(IsometryEquiv.vaddConst c) : (a : E) → P) fun (x : E) ↦ r • x)
    (ball 0 1) =
  ball c r
Tactic: change (IsometryEquiv.vaddConst c) ∘ (r • ·) '' ball (0 : E) 1 = ball c r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ image.{u_1, u_2} (α := E) (Function.comp (β := E) (⇑(IsometryEquiv.vaddConst c) : (a : E) → P) fun (x : E) ↦ r • x)
      (ball 0 1) =
    ball c r
have rw : ball ((IsometryEquiv.vaddConst c : (a : E) → P) 0) ‖r‖ = ball c r
Tactic: rw [image_comp, image_smul, smul_unitBall hr.ne', IsometryEquiv.image_ball]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
⊢ Eq.{u_1 + 1} (α := Set E)
    (PartialEquiv.source.{u_1, u_2} (β := P)
      (toPartialEquiv
        (if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯
        else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))))
    univ
have pos : ∀ (h : 0 < r), (toPartialEquiv (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) sorry)).source = univ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
pos : ∀ (h : 0 < r), (toPartialEquiv (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯)).source = univ
⊢ Eq.{u_1 + 1} (α := Set E)
    (PartialEquiv.source.{u_1, u_2} (β := P)
      (toPartialEquiv
        (if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯
        else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))))
    univ
have neg : ¬0 < r →
  (toPartialEquiv
        (Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))).source =
    univ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (toPartialEquiv (univBall c r)).target = ball c r
have rw : (toPartialEquiv (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r hr) sorry)).target = ball c r
Tactic: rw [univBall, dif_pos hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
⊢ ball c r ⊆ (toPartialEquiv (univBall c r)).target
have pos : ∀ (hr : 0 < r), ball c r ⊆ (toPartialEquiv (univBall c r)).target
Tactic: by_cases hr : 0 < r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
pos : ∀ (hr : 0 < r), ball c r ⊆ (toPartialEquiv (univBall c r)).target
⊢ ball c r ⊆ (toPartialEquiv (univBall c r)).target
have neg : ∀ (hr : ¬0 < r), ball c r ⊆ (toPartialEquiv (univBall c r)).target
Tactic: by_cases hr : 0 < r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ball c r ⊆ (toPartialEquiv (univBall c r)).target
have pos : ball c r ⊆ ball c r
Tactic: rw [univBall_target c hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆ (toPartialEquiv (univBall c r)).target
have neg : ball c r ⊆
  (toPartialEquiv (Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))).target
Tactic: rw [univBall, dif_neg hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
⊢ (↑(if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯
          else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) :
        E → P)
      0 =
    c
have pos : ∀ (h : 0 < r), (↑(OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) sorry) : E → P) 0 = c
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
pos : ∀ (h : 0 < r), (↑(OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯) : E → P) 0 = c
⊢ (↑(if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯
          else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) :
        E → P)
      0 =
    c
have neg : ¬0 < r → (↑(Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) : E → P) 0 = c
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
⊢ (↑(OpenPartialHomeomorph.symm (univBall c r)) : P → E) c = 0
have this : 0 ∈ (toPartialEquiv (univBall c r)).source
Tactic: have : 0 ∈ (univBall c r).source := by simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
⊢ ediam (c • s) = ‖c‖₊ • ediam s
have refine : ‖c‖₊ • ediam s ≤ ediam (c • s)
Tactic: refine le_antisymm (ediam_smul_le c s) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
have inl : nnnorm.{u_1} (E := 𝕜) 0 • ediam s ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
inl : nnnorm.{u_1} (E := 𝕜) 0 • ediam s ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
have inr : ∀ (hc : c ≠ 0), ‖c‖₊ • ediam s ≤ ediam (c • s)
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
s : Set E
⊢ nnnorm.{u_1} (E := 𝕜) 0 • ediam s ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)
have inl : nnnorm.{u_1} (E := 𝕜) 0 • ediam.{u_2} (X := E) ∅ ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := Set E) 0 ∅)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
s : Set E
inl : nnnorm.{u_1} (E := 𝕜) 0 • ediam.{u_2} (X := E) ∅ ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := Set E) 0 ∅)
⊢ nnnorm.{u_1} (E := 𝕜) 0 • ediam s ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)
have inl₁ : ∀ (hs : s.Nonempty), nnnorm.{u_1} (E := 𝕜) 0 • ediam s ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
have this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) * ediam (c • s)
Tactic: have := (lipschitzWith_smul c⁻¹).ediam_image_le (c • s)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) * ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
have inr : ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) • ediam (c • s)),
  ‖c‖₊ • ediam s ≤ ediam (c • s)
Tactic: rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
      le_inv_smul_iff_of_pos (nnnorm_pos.2 hc)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) * ediam (c • s)
inr :
  ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) • ediam (c • s)),
    ‖c‖₊ • ediam s ≤ ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
have inr₁ : ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ ‖c⁻¹‖₊ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
Tactic: rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
      le_inv_smul_iff_of_pos (nnnorm_pos.2 hc)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) * ediam (c • s)
inr :
  ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) • ediam (c • s)),
    ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₁ :
  ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ ‖c⁻¹‖₊ • ediam (c • s)),
    ‖c‖₊ • ediam s ≤ ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
have inr₂ : ∀ (this : ediam (c⁻¹ • c • s) ≤ ‖c⁻¹‖₊ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
Tactic: rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
      le_inv_smul_iff_of_pos (nnnorm_pos.2 hc)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) * ediam (c • s)
inr :
  ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) • ediam (c • s)),
    ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₁ :
  ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ ‖c⁻¹‖₊ • ediam (c • s)),
    ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₂ : ∀ (this : ediam (c⁻¹ • c • s) ≤ ‖c⁻¹‖₊ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
have inr₃ : ∀ (this : ediam s ≤ ‖c⁻¹‖₊ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
Tactic: rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
      le_inv_smul_iff_of_pos (nnnorm_pos.2 hc)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) * ediam (c • s)
inr :
  ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) • ediam (c • s)),
    ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₁ :
  ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ ‖c⁻¹‖₊ • ediam (c • s)),
    ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₂ : ∀ (this : ediam (c⁻¹ • c • s) ≤ ‖c⁻¹‖₊ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₃ : ∀ (this : ediam s ≤ ‖c⁻¹‖₊ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
have inr₄ : ∀ (this : ediam s ≤ ‖c‖₊⁻¹ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
Tactic: rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
      le_inv_smul_iff_of_pos (nnnorm_pos.2 hc)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) * ediam (c • s)
inr :
  ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) • ediam (c • s)),
    ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₁ :
  ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ ‖c⁻¹‖₊ • ediam (c • s)),
    ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₂ : ∀ (this : ediam (c⁻¹ • c • s) ≤ ‖c⁻¹‖₊ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₃ : ∀ (this : ediam s ≤ ‖c⁻¹‖₊ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₄ : ∀ (this : ediam s ≤ ‖c‖₊⁻¹ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
have inr₅ : ∀ (this : ‖c‖₊ • ediam s ≤ ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
Tactic: rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
      le_inv_smul_iff_of_pos (nnnorm_pos.2 hc)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ diam (c • x) = ‖c‖ * diam x
have simp_rw : (ediam (c • x)).toReal = ‖c‖ * (ediam x).toReal
Tactic: simp_rw [diam, ediam_smul₀, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
simp_rw : (ediam (c • x)).toReal = ‖c‖ * (ediam x).toReal
⊢ diam (c • x) = ‖c‖ * diam x
have simp_rw₁ : (‖c‖₊ • ediam x).toReal = ‖c‖ * (ediam x).toReal
Tactic: simp_rw [diam, ediam_smul₀, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
simp_rw : (ediam (c • x)).toReal = ‖c‖ * (ediam x).toReal
simp_rw₁ : (‖c‖₊ • ediam x).toReal = ‖c‖ * (ediam x).toReal
⊢ diam (c • x) = ‖c‖ * diam x
have simp_rw₂ : ‖c‖₊ • (ediam x).toReal = ‖c‖ * (ediam x).toReal
Tactic: simp_rw [diam, ediam_smul₀, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
simp_rw : (ediam (c • x)).toReal = ‖c‖ * (ediam x).toReal
simp_rw₁ : (‖c‖₊ • ediam x).toReal = ‖c‖ * (ediam x).toReal
simp_rw₂ : ‖c‖₊ • (ediam x).toReal = ‖c‖ * (ediam x).toReal
⊢ diam (c • x) = ‖c‖ * diam x
have simp_rw₃ : (↑‖c‖₊ : ℝ) • (ediam x).toReal = ‖c‖ * (ediam x).toReal
Tactic: simp_rw [diam, ediam_smul₀, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
simp_rw : (ediam (c • x)).toReal = ‖c‖ * (ediam x).toReal
simp_rw₁ : (‖c‖₊ • ediam x).toReal = ‖c‖ * (ediam x).toReal
simp_rw₂ : ‖c‖₊ • (ediam x).toReal = ‖c‖ * (ediam x).toReal
simp_rw₃ : (↑‖c‖₊ : ℝ) • (ediam x).toReal = ‖c‖ * (ediam x).toReal
⊢ diam (c • x) = ‖c‖ * diam x
have simp_rw₄ : ‖c‖ • (ediam x).toReal = ‖c‖ * (ediam x).toReal
Tactic: simp_rw [diam, ediam_smul₀, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ⨅ y ∈ c • s, edist (c • x) y = HSMul.hSMul (β := ENNReal) ‖c‖₊ (⨅ y ∈ s, edist x y)
have this : Function.Surjective (β := E) fun (x : E) ↦ c • x
Tactic: have : Function.Surjective ((c • ·) : E → E) :=
    Function.RightInverse.surjective (smul_inv_smul₀ hc)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective (β := E) fun (x : E) ↦ c • x
⊢ ⨅ y ∈ c • s, edist (c • x) y = HSMul.hSMul (β := ENNReal) ‖c‖₊ (⨅ y ∈ s, edist x y)
have trans : Eq (α := ENNReal) (⨅ y ∈ c • s, edist (c • x) y) (⨅ y ∈ s, ‖c‖₊ • edist x y)
Tactic: trans ⨅ (y) (_ : y ∈ s), ‖c‖₊ • edist x y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective (β := E) fun (x : E) ↦ c • x
trans : Eq (α := ENNReal) (⨅ y ∈ c • s, edist (c • x) y) (⨅ y ∈ s, ‖c‖₊ • edist x y)
⊢ ⨅ y ∈ c • s, edist (c • x) y = HSMul.hSMul (β := ENNReal) ‖c‖₊ (⨅ y ∈ s, edist x y)
have trans₁ : ⨅ y ∈ s, ‖c‖₊ • edist x y = HSMul.hSMul (β := ENNReal) ‖c‖₊ (⨅ y ∈ s, edist x y)
Tactic: trans ⨅ (y) (_ : y ∈ s), ‖c‖₊ • edist x y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective (β := E) fun (x : E) ↦ c • x
⊢ Eq (α := ENNReal) (⨅ y ∈ c • s, edist (c • x) y) (⨅ y ∈ s, ‖c‖₊ • edist x y)
have refine : ∀ (y : E), Eq (α := ENNReal) (⨅ (_ : c • y ∈ c • s), edist (c • x) (c • y)) (⨅ (_ : y ∈ s), ‖c‖₊ • edist x y)
Tactic: refine (this.iInf_congr _ fun y => ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective (β := E) fun (x : E) ↦ c • x
y : E
⊢ Eq (α := ENNReal) (⨅ (_ : c • y ∈ c • s), edist (c • x) (c • y)) (⨅ (_ : y ∈ s), ‖c‖₊ • edist x y)
have simp_rw : Eq (α := ENNReal) (⨅ (_ : y ∈ s), edist (c • x) (c • y)) (⨅ (_ : y ∈ s), ‖c‖₊ • edist x y)
Tactic: simp_rw [smul_mem_smul_set_iff₀ hc, edist_smul₀]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective (β := E) fun (x : E) ↦ c • x
⊢ ⨅ y ∈ s, ‖c‖₊ • edist x y = HSMul.hSMul (β := ENNReal) ‖c‖₊ (⨅ y ∈ s, edist x y)
have this₁ : (↑‖c‖₊ : ENNReal) ≠ 0
Tactic: have : (‖c‖₊ : ENNReal) ≠ 0 := by simp [hc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this_1 : Function.Surjective (β := E) fun (x : E) ↦ c • x
this : (↑‖c‖₊ : ENNReal) ≠ 0
⊢ ⨅ y ∈ s, ‖c‖₊ • edist x y = HSMul.hSMul (β := ENNReal) ‖c‖₊ (⨅ y ∈ s, edist x y)
have simp_rw : ⨅ y ∈ s, (↑‖c‖₊ : ENNReal) • edist x y = HSMul.hSMul (β := ENNReal) (↑‖c‖₊ : ENNReal) (⨅ y ∈ s, edist x y)
Tactic: simp_rw [ENNReal.smul_def, smul_eq_mul, ENNReal.mul_iInf_of_ne this ENNReal.coe_ne_top]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this_1 : Function.Surjective (β := E) fun (x : E) ↦ c • x
this : (↑‖c‖₊ : ENNReal) ≠ 0
simp_rw : ⨅ y ∈ s, (↑‖c‖₊ : ENNReal) • edist x y = HSMul.hSMul (β := ENNReal) (↑‖c‖₊ : ENNReal) (⨅ y ∈ s, edist x y)
⊢ ⨅ y ∈ s, ‖c‖₊ • edist x y = HSMul.hSMul (β := ENNReal) ‖c‖₊ (⨅ y ∈ s, edist x y)
have simp_rw₁ : ⨅ y ∈ s, (↑‖c‖₊ : ENNReal) * edist x y = (↑‖c‖₊ : ENNReal) * ⨅ y ∈ s, edist x y
Tactic: simp_rw [ENNReal.smul_def, smul_eq_mul, ENNReal.mul_iInf_of_ne this ENNReal.coe_ne_top]