awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
rw₁ rw₂ : x = x
⊢ (g : (a : F) → G) ((f : (a : E) → F) ((finv : (a : F) → E) ((ginv : (a : G) → F) x : F) : E) : F) = x

Tactic:
rw [hfinv, hginv]
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
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
⊢ g.HasRightInverse

Tactic:
obtain ⟨fginv, hfginv⟩ := hfg
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
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)
y : G
⊢ (g : (a : F) → G) ((f ∘SL fginv : (a : G) → F) y : F) = y

Tactic:
simpa using hfginv y
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
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:
exact ⟨f.comp fginv, fun y ↦ by simpa using hfginv y⟩
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
F' : Type u_5
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
inst_7 : TopologicalSpace F'
inst_8 : AddCommMonoid F'
inst_9 : Module R F'
f : E →L[R] F
f₀ : F' ≃L[R] E
hf : f.HasRightInverse
⊢ (f ∘SL (↑f₀ : F' →L[R] E)).HasRightInverse

Tactic:
hf.comp f₀.hasRightInverse

Premises used: ContinuousLinearEquiv.hasRightInverse, ContinuousLinearMap.HasRightInverse.comp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
F' : Type u_5
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
inst_7 : TopologicalSpace F'
inst_8 : AddCommMonoid F'
inst_9 : Module R F'
f : E →L[R] F
g : F ≃L[R] F'
hf : f.HasRightInverse
⊢ ((↑g : F →L[R] F') ∘SL f).HasRightInverse

Tactic:
g.hasRightInverse.comp hf

Premises used: ContinuousLinearEquiv.hasRightInverse, ContinuousLinearMap.HasRightInverse.comp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
h :
  RightInverse (α := F × G) (β := F) (⇑(ContinuousLinearMap.prod (ContinuousLinearMap.id R F) 0) : (a : F) → F × G)
    (⇑(fst R F G) : (a : F × G) → F)
⊢ ContinuousLinearMap.HasRightInverse (fst R F G)

Tactic:
use (ContinuousLinearMap.id _ _).prod 0

Premises used: ContinuousLinearMap.id, ContinuousLinearMap.prod, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
x : F
⊢ (fst R F G : (a : F × G) → F)
      ((ContinuousLinearMap.prod (ContinuousLinearMap.id R F) 0 : (a : F) → F × G) x : F × G) =
    x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
h :
  RightInverse (α := F × G) (β := G) (⇑(ContinuousLinearMap.prod 0 (ContinuousLinearMap.id R G)) : (a : G) → F × G)
    (⇑(snd R F G) : (a : F × G) → G)
⊢ ContinuousLinearMap.HasRightInverse (snd R F G)

Tactic:
use ContinuousLinearMap.prod 0 (.id R G)

Premises used: ContinuousLinearMap.id, ContinuousLinearMap.prod, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
x : G
⊢ (snd R F G : (a : F × G) → G)
      ((ContinuousLinearMap.prod 0 (ContinuousLinearMap.id R G) : (a : G) → F × G) x : F × G) =
    x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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)
obtain : ∀ (g : F →ₗ[𝕜] E) (hg : (↑f : E →ₗ[𝕜] F) ∘ₗ g = LinearMap.id), f.HasRightInverse
⊢ f.HasRightInverse

Tactic:
obtain ⟨g, hg⟩ :=
    f.toLinearMap.exists_rightInverse_of_surjective (f.range_eq_top_of_surjective hf)

Premises used: LinearMap.range_eq_top_of_surjective, LinearMap.exists_rightInverse_of_surjective, ContinuousLinearMap.toLinearMap
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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)
g : F →ₗ[𝕜] E
hg : (↑f : E →ₗ[𝕜] F) ∘ₗ g = LinearMap.id
⊢ f.HasRightInverse

Tactic:
⟨⟨g, g.continuous_of_finiteDimensional⟩, fun x ↦ congr($hg x)⟩

Premises used: ContinuousLinearMap.HasRightInverse, congrArg, ContinuousLinearMap.mk, id, LinearMap.continuous_of_finiteDimensional, Exists.intro, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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)
g : F →ₗ[𝕜] E
hg : (↑f : E →ₗ[𝕜] F) ∘ₗ g = LinearMap.id
⊢ f.HasRightInverse

Tactic:
exact ⟨⟨g, g.continuous_of_finiteDimensional⟩, fun x ↦ congr($hg x)⟩
-- Module: Mathlib.Analysis.Normed.Module.Convex
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‖
rw₃ rw₄ : a * ‖x‖ + b * ‖y‖ = a * ‖x‖ + b * ‖y‖
⊢ ‖a • x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖

Tactic:
rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]

Premises used: norm_smul, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ ConvexOn.{0, u_1, 0} ℝ (E := E) univ norm

Tactic:
convexOn_norm convex_univ

Premises used: convex_univ, convexOn_norm
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
z : E
hs : Convex ℝ s
⊢ ConvexOn ℝ (β := ℝ) s fun (z' : E) ↦ dist z' z

Tactic:
simpa [dist_eq_norm, preimage_preimage] using
    (convexOn_norm (hs.translate (-z))).comp_affineMap (AffineMap.id ℝ E - AffineMap.const ℝ E z)

Premises used: Real, dist_eq_norm, Set.preimage_preimage, HSub.hSub, Convex.translate, AffineMap.const, AffineMap.id, ConvexOn.comp_affineMap, Neg.neg, convexOn_norm
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
z : E
⊢ ConvexOn ℝ (β := ℝ) univ fun (z' : E) ↦ dist z' z

Tactic:
convexOn_dist z convex_univ

Premises used: convexOn_dist, convex_univ
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
r : ℝ
⊢ Convex ℝ (ball a r)

Tactic:
simpa only [ball, sep_univ] using (convexOn_univ_dist a).convex_lt r

Premises used: Set.sep_univ, convexOn_univ_dist, Metric.ball, ConvexOn.convex_lt
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
⊢ Convex ℝ (eball a ⊤)

Tactic:
simp [convex_univ]

Premises used: convex_univ
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
r : NNReal
⊢ Convex ℝ (eball a (↑r : ENNReal))

Tactic:
simp [eball_coe, convex_ball]

Premises used: convex_ball, Metric.eball_coe
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
r : ENNReal
top : Convex ℝ (eball a ⊤)
coe : ∀ (r : NNReal), Convex ℝ (eball a (↑r : ENNReal))
⊢ Convex ℝ (eball a r)

Tactic:
cases r with
  | top => simp [convex_univ]
  | coe r => simp [eball_coe, convex_ball]

Premises used: convex_ball, convex_univ, Metric.eball_coe
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
r : ℝ
⊢ Convex ℝ (closedBall a r)

Tactic:
simpa only [closedBall, sep_univ] using (convexOn_univ_dist a).convex_le r

Premises used: Set.sep_univ, convexOn_univ_dist, ConvexOn.convex_le, Metric.closedBall
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
⊢ segment ℝ x y ⊆ closedBall x (dist x y)

Tactic:
(convex_closedBall x _).segment_subset (mem_closedBall_self dist_nonneg)
    (mem_closedBall.mpr (dist_comm y x ▸ le_refl _))

Premises used: Iff.mpr, le_refl, dist_nonneg, Eq.rec, dist_comm, Metric.mem_closedBall, Metric.mem_closedBall_self, convex_closedBall, Convex.segment_subset
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
rw : segment ℝ y x ⊆ closedBall y (dist x y)
⊢ segment ℝ x y ⊆ closedBall y (dist x y)

Tactic:
rw [segment_symm]

Premises used: segment_symm
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
⊢ segment ℝ y x ⊆ closedBall y (dist x y)

Tactic:
dist_comm x y ▸ segment_subset_closedBall_left y x

Premises used: Eq.rec, dist_comm, segment_subset_closedBall_left, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
⊢ segment ℝ y x ⊆ closedBall y (dist x y)

Tactic:
exact dist_comm x y ▸ segment_subset_closedBall_left y x
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
⊢ Convex ℝ (closedEBall a ⊤)

Tactic:
simp [convex_univ]

Premises used: convex_univ
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
r : NNReal
⊢ Convex ℝ (closedEBall a (↑r : ENNReal))

Tactic:
simp [closedEBall_coe, convex_closedBall]

Premises used: Metric.closedEBall_coe, convex_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
r : ENNReal
top : Convex ℝ (closedEBall a ⊤)
coe : ∀ (r : NNReal), Convex ℝ (closedEBall a (↑r : ENNReal))
⊢ Convex ℝ (closedEBall a r)

Tactic:
cases r with
  | top => simp [convex_univ]
  | coe r => simp [closedEBall_coe, convex_closedBall]

Premises used: convex_univ, Metric.closedEBall_coe, convex_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
rw₇ rw₈ : closedBall x r = closedBall x r
⊢ (convexHull ℝ : (a : Set F) → Set F) (sphere 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]

Premises used: convexHull_vadd, Metric.vadd_sphere, vadd_eq_add, vadd_closedBall_zero, add_zero
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
suffices :
  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

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]
-- Module: Mathlib.Analysis.Normed.Module.Convex
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)

Tactic:
subset_antisymm (convexHull_min sphere_subset_closedBall (convex_closedBall 0 r))
    (fun x h ↦ mem_convexHull_iff.mpr fun U hU_sub hU ↦ ?_)

Premises used: Iff.mpr, subset_antisymm, convexHull_min, Metric.sphere_subset_closedBall, mem_convexHull_iff, OfNat.ofNat, convex_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
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
⊢ Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (sphere 0 r) : Set F) (closedBall 0 r : Set F)

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 ↦ ?_)

Premises used: Iff.mpr, subset_antisymm, convexHull_min, Metric.sphere_subset_closedBall, mem_convexHull_iff, OfNat.ofNat, convex_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
mul_invOf_self : HMul.hMul (α := ℝ) 2 2⁻¹ = 1
⊢ Invertible (α := ℝ) 2

Tactic:
use 2⁻¹
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
⊢ HMul.hMul (α := ℝ) 2⁻¹ 2 = 1

Tactic:
grind
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
⊢ HMul.hMul (α := ℝ) 2 2⁻¹ = 1

Tactic:
grind
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
have : ∀ (x : Invertible (α := ℝ) 2), 0 ∈ U
⊢ 0 ∈ U

Tactic:
have _ : Invertible (2 : ℝ) := by use 2⁻¹ <;> grind
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
obtain : ∀ (z : F) (hz : Membership.mem (γ := Set F) (sphere 0 r) z), 0 ∈ U
⊢ 0 ∈ U

Tactic:
obtain ⟨z, hz⟩ := NormedSpace.sphere_nonempty (E := F).mpr hr

Premises used: Iff.mpr, NormedSpace.sphere_nonempty
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
rw : midpoint ℝ z (-z) ∈ U
⊢ 0 ∈ U

Tactic:
rw [← midpoint_self_neg (R := ℝ) (x := z)]

Premises used: Real, midpoint_self_neg
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
⊢ Membership.mem (γ := Set F) (sphere 0 r) (-z)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
⊢ midpoint ℝ z (-z) ∈ U

Tactic:
exact Convex.midpoint_mem hU (hU_sub hz) <| hU_sub (by simp_all)

Premises used: Convex.midpoint_mem
-- Module: Mathlib.Analysis.Normed.Module.Convex
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

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)
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
neg : ∀ (hr₀ : ¬r = 0), x ∈ U
⊢ x ∈ U

Tactic:
by_cases hr₀ : r = 0
-- Module: Mathlib.Analysis.Normed.Module.Convex
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

Tactic:
simp_all
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
neg : ∀ (x_zero : ¬x = 0), x ∈ U
⊢ x ∈ U

Tactic:
by_cases x_zero : x = 0
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
pos pos₁ pos₂ pos₃ : 0 ∈ U
⊢ x ∈ U

Tactic:
rwa [x_zero]
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
⊢ let z := (r * ‖x‖⁻¹) • x;
  z = (r * ‖x‖⁻¹) • x

Tactic:
set z := (r * ‖x‖⁻¹) • x with hz_def

Premises used: Norm.norm, HMul.hMul, Inv.inv
-- Module: Mathlib.Analysis.Normed.Module.Convex
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‖ ≤ r

Tactic:
simp only [mem_closedBall, dist_zero_right] at h

Premises used: Metric.mem_closedBall, dist_zero_right
-- Module: Mathlib.Analysis.Normed.Module.Convex
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
grw₁ grw₂ : LE.le (α := ℝ) 1 1
⊢ r⁻¹ * ‖x‖ ≤ 1

Tactic:
grw [h, inv_mul_le_one]

Premises used: inv_mul_le_one
-- Module: Mathlib.Analysis.Normed.Module.Convex
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

Tactic:
have hr₁ : r⁻¹ * ‖x‖ ≤ 1 := by
    simp only [mem_closedBall, dist_zero_right] at h
    grw [h, inv_mul_le_one]