awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
ginv : G →L[R] F
hginv : RightInverse.{u_4 + 1, u_6 + 1} (α := F) (β := G) (⇑ginv : (a : G) → F) (⇑g : (a : F) → G)
x : G
⊢ (g : (a : F) → G) ((f : (a : E) → F) ((finv : (a : F) → E) ((ginv : (a : G) → F) x : F) : E) : F) = x
have rw : (g : (a : F) → G) ((ginv : (a : G) → F) x : F) = x
Tactic: rw [hfinv, hginv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
ginv : G →L[R] F
hginv : RightInverse.{u_4 + 1, u_6 + 1} (α := F) (β := G) (⇑ginv : (a : G) → F) (⇑g : (a : F) → G)
x : G
rw : (g : (a : F) → G) ((ginv : (a : G) → F) x : F) = x
⊢ (g : (a : F) → G) ((f : (a : E) → F) ((finv : (a : F) → E) ((ginv : (a : G) → F) x : F) : E) : F) = x
have rw₁ : x = x
Tactic: rw [hfinv, hginv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
hfg : (g ∘SL f).HasRightInverse
⊢ g.HasRightInverse
have obtain : ∀ (fginv : G →L[R] E)
  (hfginv : RightInverse.{u_2 + 1, u_6 + 1} (α := E) (β := G) (⇑fginv : (a : G) → E) (⇑(g ∘SL f) : (a : E) → G)),
  g.HasRightInverse
Tactic: obtain ⟨fginv, hfginv⟩ := hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace F
inst_2 : AddCommMonoid F
inst_3 : Module R F
inst_4 : TopologicalSpace G
inst_5 : AddCommMonoid G
inst_6 : Module R G
⊢ ContinuousLinearMap.HasRightInverse (fst R F G)
have h : RightInverse (α := F × G) (β := F) (⇑(ContinuousLinearMap.prod (ContinuousLinearMap.id R F) 0) : (a : F) → F × G)
  (⇑(fst R F G) : (a : F × G) → F)
Tactic: use (ContinuousLinearMap.id _ _).prod 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace F
inst_2 : AddCommMonoid F
inst_3 : Module R F
inst_4 : TopologicalSpace G
inst_5 : AddCommMonoid G
inst_6 : Module R G
⊢ ContinuousLinearMap.HasRightInverse (snd R F G)
have h : RightInverse (α := F × G) (β := G) (⇑(ContinuousLinearMap.prod 0 (ContinuousLinearMap.id R G)) : (a : G) → F × G)
  (⇑(snd R F G) : (a : F × G) → G)
Tactic: use ContinuousLinearMap.prod 0 (.id R G)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
𝕜 : Type u_7
inst : NontriviallyNormedField 𝕜
E : Type u_8
F : Type u_9
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
f : E →L[𝕜] F
inst_12 : CompleteSpace 𝕜
inst_13 : FiniteDimensional 𝕜 F
hf : Surjective.{u_8 + 1, u_9 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ f.HasRightInverse
have obtain : ∀ (g : F →ₗ[𝕜] E) (hg : (↑f : E →ₗ[𝕜] F) ∘ₗ g = LinearMap.id), f.HasRightInverse
Tactic: obtain ⟨g, hg⟩ :=
    f.toLinearMap.exists_rightInverse_of_surjective (f.range_eq_top_of_surjective hf)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
h : x ∈ s
y : E
h_1 : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
⊢ ‖a • x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖
have rw : ‖a‖ * ‖x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖
Tactic: rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
h : x ∈ s
y : E
h_1 : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw : ‖a‖ * ‖x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖
⊢ ‖a • x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖
have rw₁ : ‖a‖ * ‖x‖ + ‖b‖ * ‖y‖ = a * ‖x‖ + b * ‖y‖
Tactic: rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
h : x ∈ s
y : E
h_1 : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw : ‖a‖ * ‖x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖
rw₁ : ‖a‖ * ‖x‖ + ‖b‖ * ‖y‖ = a * ‖x‖ + b * ‖y‖
⊢ ‖a • x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖
have rw₂ : a * ‖x‖ + ‖b‖ * ‖y‖ = a * ‖x‖ + b * ‖y‖
Tactic: rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
h : x ∈ s
y : E
h_1 : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw : ‖a‖ * ‖x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖
rw₁ : ‖a‖ * ‖x‖ + ‖b‖ * ‖y‖ = a * ‖x‖ + b * ‖y‖
rw₂ : a * ‖x‖ + ‖b‖ * ‖y‖ = a * ‖x‖ + b * ‖y‖
⊢ ‖a • x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖
have rw₃ : a * ‖x‖ + b * ‖y‖ = a * ‖x‖ + b * ‖y‖
Tactic: rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
r : ENNReal
⊢ Convex ℝ (eball a r)
have top : Convex ℝ (eball a ⊤)
Tactic: cases r with
  | top => simp [convex_univ]
  | coe r => simp [eball_coe, convex_ball]
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
r : ENNReal
top : Convex ℝ (eball a ⊤)
⊢ Convex ℝ (eball a r)
have coe : ∀ (r : NNReal), Convex ℝ (eball a (↑r : ENNReal))
Tactic: cases r with
  | top => simp [convex_univ]
  | coe r => simp [eball_coe, convex_ball]
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
⊢ segment ℝ x y ⊆ closedBall y (dist x y)
have rw : segment ℝ y x ⊆ closedBall y (dist x y)
Tactic: rw [segment_symm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
r : ENNReal
⊢ Convex ℝ (closedEBall a r)
have top : Convex ℝ (closedEBall a ⊤)
Tactic: cases r with
  | top => simp [convex_univ]
  | coe r => simp [closedEBall_coe, convex_closedBall]
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
r : ENNReal
top : Convex ℝ (closedEBall a ⊤)
⊢ Convex ℝ (closedEBall a r)
have coe : ∀ (r : NNReal), Convex ℝ (closedEBall a (↑r : ENNReal))
Tactic: cases r with
  | top => simp [convex_univ]
  | coe r => simp [closedEBall_coe, convex_closedBall]
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
this : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) (closedBall 0 r : Set F)
⊢ (convexHull ℝ : (a : Set F) → Set F) (sphere x r) = closedBall x r
have rw : (convexHull ℝ : (a : Set F) → Set F) (sphere (x + 0) r) = closedBall (x + 0) r
Tactic: rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
this : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) (closedBall 0 r : Set F)
rw : (convexHull ℝ : (a : Set F) → Set F) (sphere (x + 0) r) = closedBall (x + 0) r
⊢ (convexHull ℝ : (a : Set F) → Set F) (sphere x r) = closedBall x r
have rw₁ : (convexHull ℝ : (a : Set F) → Set F) (sphere (HVAdd.hVAdd (β := F) x 0) r) = closedBall (HVAdd.hVAdd (β := F) x 0) r
Tactic: rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
this : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) (closedBall 0 r : Set F)
rw : (convexHull ℝ : (a : Set F) → Set F) (sphere (x + 0) r) = closedBall (x + 0) r
rw₁ :
  (convexHull ℝ : (a : Set F) → Set F) (sphere (HVAdd.hVAdd (β := F) x 0) r) = closedBall (HVAdd.hVAdd (β := F) x 0) r
⊢ (convexHull ℝ : (a : Set F) → Set F) (sphere x r) = closedBall x r
have rw₂ : (convexHull ℝ : (a : Set F) → Set F) (HVAdd.hVAdd (β := Set F) x (sphere 0 r)) = closedBall (HVAdd.hVAdd (β := F) x 0) r
Tactic: rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
this : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) (closedBall 0 r : Set F)
rw : (convexHull ℝ : (a : Set F) → Set F) (sphere (x + 0) r) = closedBall (x + 0) r
rw₁ :
  (convexHull ℝ : (a : Set F) → Set F) (sphere (HVAdd.hVAdd (β := F) x 0) r) = closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₂ :
  (convexHull ℝ : (a : Set F) → Set F) (HVAdd.hVAdd (β := Set F) x (sphere 0 r)) =
    closedBall (HVAdd.hVAdd (β := F) x 0) r
⊢ (convexHull ℝ : (a : Set F) → Set F) (sphere x r) = closedBall x r
have rw₃ : HVAdd.hVAdd (β := Set F) x ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) =
  closedBall (HVAdd.hVAdd (β := F) x 0) r
Tactic: rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
this : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) (closedBall 0 r : Set F)
rw : (convexHull ℝ : (a : Set F) → Set F) (sphere (x + 0) r) = closedBall (x + 0) r
rw₁ :
  (convexHull ℝ : (a : Set F) → Set F) (sphere (HVAdd.hVAdd (β := F) x 0) r) = closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₂ :
  (convexHull ℝ : (a : Set F) → Set F) (HVAdd.hVAdd (β := Set F) x (sphere 0 r)) =
    closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₃ :
  HVAdd.hVAdd (β := Set F) x ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) =
    closedBall (HVAdd.hVAdd (β := F) x 0) r
⊢ (convexHull ℝ : (a : Set F) → Set F) (sphere x r) = closedBall x r
have rw₄ : HVAdd.hVAdd (β := Set F) x (closedBall 0 r) = closedBall (HVAdd.hVAdd (β := F) x 0) r
Tactic: rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
this : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) (closedBall 0 r : Set F)
rw : (convexHull ℝ : (a : Set F) → Set F) (sphere (x + 0) r) = closedBall (x + 0) r
rw₁ :
  (convexHull ℝ : (a : Set F) → Set F) (sphere (HVAdd.hVAdd (β := F) x 0) r) = closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₂ :
  (convexHull ℝ : (a : Set F) → Set F) (HVAdd.hVAdd (β := Set F) x (sphere 0 r)) =
    closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₃ :
  HVAdd.hVAdd (β := Set F) x ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) =
    closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₄ : HVAdd.hVAdd (β := Set F) x (closedBall 0 r) = closedBall (HVAdd.hVAdd (β := F) x 0) r
⊢ (convexHull ℝ : (a : Set F) → Set F) (sphere x r) = closedBall x r
have rw₅ : closedBall x r = closedBall (HVAdd.hVAdd (β := F) x 0) r
Tactic: rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
this : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) (closedBall 0 r : Set F)
rw : (convexHull ℝ : (a : Set F) → Set F) (sphere (x + 0) r) = closedBall (x + 0) r
rw₁ :
  (convexHull ℝ : (a : Set F) → Set F) (sphere (HVAdd.hVAdd (β := F) x 0) r) = closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₂ :
  (convexHull ℝ : (a : Set F) → Set F) (HVAdd.hVAdd (β := Set F) x (sphere 0 r)) =
    closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₃ :
  HVAdd.hVAdd (β := Set F) x ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) =
    closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₄ : HVAdd.hVAdd (β := Set F) x (closedBall 0 r) = closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₅ : closedBall x r = closedBall (HVAdd.hVAdd (β := F) x 0) r
⊢ (convexHull ℝ : (a : Set F) → Set F) (sphere x r) = closedBall x r
have rw₆ : closedBall x r = closedBall (x + 0) r
Tactic: rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
this : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) (closedBall 0 r : Set F)
rw : (convexHull ℝ : (a : Set F) → Set F) (sphere (x + 0) r) = closedBall (x + 0) r
rw₁ :
  (convexHull ℝ : (a : Set F) → Set F) (sphere (HVAdd.hVAdd (β := F) x 0) r) = closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₂ :
  (convexHull ℝ : (a : Set F) → Set F) (HVAdd.hVAdd (β := Set F) x (sphere 0 r)) =
    closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₃ :
  HVAdd.hVAdd (β := Set F) x ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) =
    closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₄ : HVAdd.hVAdd (β := Set F) x (closedBall 0 r) = closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₅ : closedBall x r = closedBall (HVAdd.hVAdd (β := F) x 0) r
rw₆ : closedBall x r = closedBall (x + 0) r
⊢ (convexHull ℝ : (a : Set F) → Set F) (sphere x r) = closedBall x r
have rw₇ : closedBall x r = closedBall x r
Tactic: rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
⊢ (convexHull ℝ : (a : Set F) → Set F) (sphere x r) = closedBall x r
have suffices : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) (closedBall 0 r : Set F)
Tactic: suffices convexHull ℝ (sphere (0 : F) r) = closedBall 0 r by
    rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
⊢ Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) (closedBall 0 r : Set F)
have refine : ∀ (x : F) (h : Membership.mem (γ := Set F) (closedBall 0 r) x) (U : Set F) (hU_sub : sphere 0 r ⊆ U) (hU : Convex ℝ U),
  x ∈ U
Tactic: refine subset_antisymm (convexHull_min sphere_subset_closedBall (convex_closedBall 0 r))
    (fun x h ↦ mem_convexHull_iff.mpr fun U hU_sub hU ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
⊢ Invertible (α := ℝ) 2
have invOf_mul_self : HMul.hMul (α := ℝ) 2⁻¹ 2 = 1
Tactic: use 2⁻¹
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
invOf_mul_self : HMul.hMul (α := ℝ) 2⁻¹ 2 = 1
⊢ Invertible (α := ℝ) 2
have mul_invOf_self : HMul.hMul (α := ℝ) 2 2⁻¹ = 1
Tactic: use 2⁻¹
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
⊢ 0 ∈ U
have have : ∀ (x : Invertible (α := ℝ) 2), 0 ∈ U
Tactic: have _ : Invertible (2 : ℝ) := by use 2⁻¹ <;> grind
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
x_2 : Invertible (α := ℝ) 2
⊢ 0 ∈ U
have obtain : ∀ (z : F) (hz : Membership.mem (γ := Set F) (sphere 0 r) z), 0 ∈ U
Tactic: obtain ⟨z, hz⟩ := NormedSpace.sphere_nonempty (E := F).mpr hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
x_2 : Invertible (α := ℝ) 2
z : F
hz : Membership.mem (γ := Set F) (sphere 0 r) z
⊢ 0 ∈ U
have rw : midpoint ℝ z (-z) ∈ U
Tactic: rw [← midpoint_self_neg (R := ℝ) (x := z)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
⊢ x ∈ U
have zero_mem : 0 ∈ U
Tactic: have zero_mem : (0 : F) ∈ U := by
    have _ : Invertible (2 : ℝ) := by use 2⁻¹ <;> grind
    obtain ⟨z, hz⟩ := NormedSpace.sphere_nonempty (E := F).mpr hr
    rw [← midpoint_self_neg (R := ℝ) (x := z)]
    exact Convex.midpoint_mem hU (hU_sub hz) <| hU_sub (by simp_all)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
⊢ x ∈ U
have pos : ∀ (hr₀ : r = 0), x ∈ U
Tactic: by_cases hr₀ : r = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
pos : ∀ (hr₀ : r = 0), x ∈ U
⊢ x ∈ U
have neg : ∀ (hr₀ : ¬r = 0), x ∈ U
Tactic: by_cases hr₀ : r = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
⊢ x ∈ U
have pos : ∀ (x_zero : x = 0), x ∈ U
Tactic: by_cases x_zero : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
pos : ∀ (x_zero : x = 0), x ∈ U
⊢ x ∈ U
have neg : ∀ (x_zero : ¬x = 0), x ∈ U
Tactic: by_cases x_zero : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
⊢ x ∈ U
have hz_def : let z := (r * ‖x‖⁻¹) • x;
z = (r * ‖x‖⁻¹) • x
Tactic: set z := (r * ‖x‖⁻¹) • x with hz_def
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
⊢ r⁻¹ * ‖x‖ ≤ 1
have h₁ : ‖x‖ ≤ r
Tactic: simp only [mem_closedBall, dist_zero_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
h : ‖x‖ ≤ r
⊢ r⁻¹ * ‖x‖ ≤ 1
have h₁ : 0 ≤ r⁻¹
Tactic: grw [h, inv_mul_le_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
h : ‖x‖ ≤ r
h₁ : 0 ≤ r⁻¹
⊢ r⁻¹ * ‖x‖ ≤ 1
have grw : r⁻¹ * r ≤ 1
Tactic: grw [h, inv_mul_le_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
h : ‖x‖ ≤ r
h₁ : 0 ≤ r⁻¹
grw : r⁻¹ * r ≤ 1
⊢ r⁻¹ * ‖x‖ ≤ 1
have grw₁ : LE.le (α := ℝ) 1 1
Tactic: grw [h, inv_mul_le_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
⊢ x ∈ U
have hr₁ : r⁻¹ * ‖x‖ ≤ 1
Tactic: have hr₁ : r⁻¹ * ‖x‖ ≤ 1 := by
    simp only [mem_closedBall, dist_zero_right] at h
    grw [h, inv_mul_le_one]