awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Extend
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
⊢ norm (E := ℝ) ((fr : (a : F) → ℝ) x : ℝ) =
    norm (E := ℝ) ((re : (a : 𝕜) → ℝ) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : ContinuousAdd E
inst_3 : Nontrivial E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
x : E
⊢ (𝓝[≠] x).NeBot

Tactic:
Module.punctured_nhds_neBot ℝ E x

Premises used: Real, Module.punctured_nhds_neBot
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
⊢ Membership.mem (γ := Set E) (closedBall 0 1) (‖x‖⁻¹ • x)

Tactic:
simp only [mem_closedBall_zero_iff, norm_smul, norm_inv, norm_norm, ← div_eq_inv_mul,
    div_self_le_one]

Premises used: norm_smul, norm_norm, div_self_le_one, norm_inv, mem_closedBall_zero_iff, div_eq_inv_mul
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
ht : 0 ≤ t
x : E
rw : ‖t‖ * ‖x‖ = t * ‖x‖
rw₁ : |t| * ‖x‖ = t * ‖x‖
rw₂ rw₃ : t * ‖x‖ = t * ‖x‖
⊢ ‖t • x‖ = t * ‖x‖

Tactic:
rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]

Premises used: norm_smul, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
simp_rw : ‖x - (r • x + (1 - r) • y)‖ = ‖1 - r‖ * ‖x - y‖
simp_rw₁ : ‖x - (r • x + (1 - r) • y)‖ = ‖(1 - r) • (x - y)‖
simp_rw₂ : ‖x - (r • x + (HSMul.hSMul (α := ℝ) 1 y - r • y))‖ = ‖HSMul.hSMul (α := ℝ) 1 (x - y) - r • (x - y)‖
simp_rw₃ : ‖x - (r • x + (y - r • y))‖ = ‖x - y - r • (x - y)‖
simp_rw₄ : ‖x - (r • x + (y - r • y))‖ = ‖x - y - (r • x - r • y)‖
simp_rw₅ : ‖x - r • x - (y - r • y)‖ = ‖x - y - (r • x - r • y)‖
simp_rw₆ : ‖x - r • x - y + r • y‖ = ‖x - y - r • x + r • y‖
⊢ dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖

Tactic:
simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add,
        sub_right_comm]

Premises used: sub_add, norm_smul, sub_smul, dist_eq_norm', sub_right_comm, one_smul, sub_sub, smul_sub
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
rw : |1 - r| * ‖x - y‖ = (1 - r) * dist y x
rw₁ : (1 - r) * ‖x - y‖ = (1 - r) * dist y x
rw₂ rw₃ : (1 - r) * ‖x - y‖ = (1 - r) * ‖x - y‖
⊢ ‖1 - r‖ * ‖x - y‖ = (1 - r) * dist y x

Tactic:
rw [Real.norm_eq_abs, abs_eq_self.mpr (sub_nonneg.mpr h.2), dist_eq_norm']

Premises used: Iff.mpr, dist_eq_norm', And.right, sub_nonneg, abs_eq_self, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
hbc : 0 ≤ r
⊢ (1 - r) * dist y x ≤ HSub.hSub (α := ℝ) 1 0 * dist y x

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
⊢ 0 ≤ r

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
⊢ 0 ≤ r

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
rw : 1 * dist y x = dist y x
rw₁ rw₂ : dist y x = dist y x
⊢ HSub.hSub (α := ℝ) 1 0 * dist y x = dist y x

Tactic:
rw [sub_zero, one_mul]

Premises used: sub_zero, one_mul
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r) = closedBall x r

Tactic:
Subset.antisymm closure_ball_subset_closedBall fun y hy => ?_

Premises used: Set.Subset.antisymm, Metric.closure_ball_subset_closedBall
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
refine :
  ∀ (y : E) (hy : y ∈ closedBall x r), y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r)
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r) = closedBall x r

Tactic:
refine Subset.antisymm closure_ball_subset_closedBall fun y hy => ?_

Premises used: Set.Subset.antisymm, Metric.closure_ball_subset_closedBall
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1

Tactic:
have : ContinuousWithinAt (fun c : ℝ => c • (y - x) + x) (Ico 0 1) 1 := by fun_prop
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
⊢ HSMul.hSMul (α := ℝ) 1 (y - x) + x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r)

Tactic:
this.mem_closure _ _

Premises used: ContinuousWithinAt.mem_closure
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
h : y = HSMul.hSMul (α := ℝ) 1 (y - x) + x
convert_2 : Membership.mem (γ := Set ℝ) (closure (Ico 0 1)) 1
convert_3 : MapsTo (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) (ball x r)
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r)

Tactic:
convert! this.mem_closure _ _

Premises used: ContinuousWithinAt.mem_closure
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
h : y = y - x + x
h₁ h₂ : y = y
⊢ y = HSMul.hSMul (α := ℝ) 1 (y - x) + x

Tactic:
rw [one_smul, sub_add_cancel]

Premises used: one_smul, sub_add_cancel
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
⊢ Membership.mem (γ := Set ℝ) (closure (Ico 0 1)) 1

Tactic:
simp [closure_Ico zero_ne_one, zero_le_one]

Premises used: zero_ne_one, zero_le_one, closure_Ico
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
convert_3 : ‖y - x‖ * c < r * 1
⊢ (fun (c : ℝ) ↦ c • (y - x) + x) c ∈ ball x r

Tactic:
rw [mem_ball, dist_eq_norm, add_sub_cancel_right, norm_smul, Real.norm_eq_abs,
      abs_of_nonneg hc0, mul_comm, ← mul_one r]

Premises used: dist_eq_norm, norm_smul, Metric.mem_ball, mul_comm, abs_of_nonneg, add_sub_cancel_right, mul_one, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
convert_3 :
  ∀ (hy : ‖y - x‖ ≤ r) (this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1) ⦃c : ℝ⦄
    (hc0 : 0 ≤ c) (hc1 : c < 1), ‖y - x‖ * c < r * 1
⊢ ‖y - x‖ * c < r * 1

Tactic:
rw [mem_closedBall, dist_eq_norm] at hy

Premises used: dist_eq_norm, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ 0 < r

Tactic:
replace hr : 0 < r := ((norm_nonneg _).trans hy).lt_of_ne hr.symm
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
convert_3 : ‖y - x‖ ≤ r
convert_3₁ : c < 1
convert_3₂ : 0 ≤ c
convert_3₃ : 0 < r
⊢ ‖y - x‖ * c < r * 1

Tactic:
apply mul_lt_mul'

Premises used: mul_lt_mul'
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ ‖y - x‖ ≤ r

Tactic:
assumption
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ c < 1

Tactic:
assumption
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ 0 ≤ c

Tactic:
assumption
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ 0 < r

Tactic:
assumption
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r) \ interior (ball x r) = sphere x r
rw₁ : closedBall x r \ interior (ball x r) = sphere x r
rw₂ : closedBall x r \ ball x r = sphere x r
rw₃ rw₄ : sphere x r = sphere x r
⊢ frontier (ball x r) = sphere x r

Tactic:
rw [frontier, closure_ball x hr, isOpen_ball.interior_eq, closedBall_diff_ball]

Premises used: frontier, Metric.isOpen_ball, Metric.closedBall_diff_ball, closure_ball, IsOpen.interior_eq
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
inl : ∀ (hr : r < 0), interior (closedBall x r) = ball x r
inr : ∀ (hr : 0 < r), interior (closedBall x r) = ball x r
⊢ interior (closedBall x r) = ball x r

Tactic:
rcases hr.lt_or_gt with hr | hr

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr : r < 0
inl : interior ∅ = ball x r
inl₁ : Eq.{u_1 + 1} (α := Set E) (interior ∅) ∅
inl₂ inl₃ : Eq.{u_1 + 1} (α := Set E) ∅ ∅
⊢ interior (closedBall x r) = ball x r

Tactic:
rw [closedBall_eq_empty.2 hr, ball_eq_empty.2 hr.le, interior_empty]

Premises used: Iff.mpr, interior_empty, LT.lt.le, Metric.closedBall_eq_empty, Metric.ball_eq_empty
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) = ball x r

Tactic:
Subset.antisymm ?_ ball_subset_interior_closedBall

Premises used: Set.Subset.antisymm, Metric.ball_subset_interior_closedBall
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr : 0 < r
inr : interior (closedBall x r) ⊆ ball x r
⊢ interior (closedBall x r) = ball x r

Tactic:
refine Subset.antisymm ?_ ball_subset_interior_closedBall

Premises used: Set.Subset.antisymm, Metric.ball_subset_interior_closedBall
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
inr : ∀ (hr : dist y x < r), y ∈ ball x r
inr₁ : ∀ (hr : dist y x ≠ 0) (hr : 0 < dist y x) (hy : y ∈ interior (closedBall x (dist y x))), y ∈ ball x (dist y x)
⊢ y ∈ ball x r

Tactic:
rcases (mem_closedBall.1 <| interior_subset hy).lt_or_eq with (hr | rfl)

Premises used: interior_subset, LE.le.lt_or_eq, Iff.mp, Metric.mem_closedBall, rfl
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr_2 : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
hr : dist y x < r
⊢ y ∈ ball x r

Tactic:
hr

Premises used: Set.Mem, setOf, Metric.ball
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr_1 : r ≠ 0
hr_2 : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
hr : dist y x < r
⊢ y ∈ ball x r

Tactic:
exact hr
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
hr_1 : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun (c : ℝ) ↦ c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
hr_1 : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun (c : ℝ) ↦ c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
⊢ 1 ∈ f ⁻¹' interior (closedBall x (dist y x))

Tactic:
simpa [f]
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
hr_1 : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun (c : ℝ) ↦ c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
⊢ Membership.mem (γ := Set ℝ) (interior (Icc (-1) 1)) 1

Tactic:
have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) :=
      interior_mono this (preimage_interior_subset_interior_preimage (by fun_prop) (by simpa [f]))
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
hr_1 : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun (c : ℝ) ↦ c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
h1 : Membership.mem (γ := Set ℝ) (interior (Icc (-1) 1)) 1
⊢ y ∈ ball x (dist y x)

Tactic:
simp at h1
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
hr_1 : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun (c : ℝ) ↦ c • (y - x) + x
inr : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
⊢ y ∈ ball x (dist y x)

Tactic:
suffices f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1 by
    have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) :=
      interior_mono this (preimage_interior_subset_interior_preimage (by fun_prop) (by simpa [f]))
    simp at h1
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
hr_1 : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun (c : ℝ) ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
inr : ‖c‖ * dist y x ≤ 1 * dist y x
⊢ Membership.mem (γ := Set ℝ) (Icc (-1) 1) c

Tactic:
rw [mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← mul_le_mul_iff_left₀ hr]

Premises used: abs_le, Set.mem_Icc, mul_le_mul_iff_left₀, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
hr_1 : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun (c : ℝ) ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ ‖c‖ * dist y x ≤ 1 * dist y x

Tactic:
simpa [f, dist_eq_norm, norm_smul] using hc

Premises used: dist_eq_norm, norm_smul
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw :
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x r) \ interior (closedBall x r) = sphere x r
rw₁ : closedBall x r \ interior (closedBall x r) = sphere x r
rw₂ : closedBall x r \ ball x r = sphere x r
rw₃ rw₄ : sphere x r = sphere x r
⊢ frontier (closedBall x r) = sphere x r

Tactic:
rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball]

Premises used: frontier, interior_closedBall, Metric.closure_closedBall, Metric.closedBall_diff_ball
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw : interior (frontier (closedBall x r)) = ∅
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set E) ∅ ∅
⊢ interior (sphere x r) = ∅

Tactic:
rw [← frontier_closedBall x hr, interior_frontier isClosed_closedBall]

Premises used: Metric.isClosed_closedBall, interior_frontier, frontier_closedBall
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
rw : sphere x r \ interior (sphere x r) = sphere x r
rw₁ : sphere x r \ ∅ = sphere x r
rw₂ rw₃ : sphere x r = sphere x r
⊢ frontier (sphere x r) = sphere x r

Tactic:
rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty]

Premises used: IsClosed.frontier_eq, Set.diff_empty, interior_sphere, Metric.isClosed_sphere
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
c : ℝ
hc : 0 ≤ c
rcases : ∀ (x : E) (hx : ‖x‖ ≠ 0), ∃ (x : E), ‖x‖ = c
⊢ ∃ (x : E), ‖x‖ = c

Tactic:
rcases exists_norm_ne_zero E with ⟨x, hx⟩

Premises used: exists_norm_ne_zero
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
h : ‖c • ‖x‖⁻¹ • x‖ = c
⊢ ∃ (x : E), ‖x‖ = c

Tactic:
use c • ‖x‖⁻¹ • x
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ‖c • ‖x‖⁻¹ • x‖ = c

Tactic:
simp [norm_smul, Real.norm_of_nonneg hc, inv_mul_cancel₀ hx]

Premises used: norm_smul, inv_mul_cancel₀, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
⊢ range.{0, u_1 + 1} (ι := E) norm = Ici 0

Tactic:
Subset.antisymm (range_subset_iff.2 norm_nonneg) fun _ => exists_norm_eq E

Premises used: Set.Subset.antisymm, Iff.mpr, exists_norm_eq, Set.range_subset_iff, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
⊢ Surjective.{u_1 + 1, 1} (α := E) nnnorm

Tactic:
fun c =>
  (exists_norm_eq E c.coe_nonneg).imp fun _ h => NNReal.eq h

Premises used: exists_norm_eq, NNReal.eq, Exists.imp, NNReal.coe_nonneg, Function.Surjective
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
⊢ range.{0, u_1 + 1} (ι := E) nnnorm = univ

Tactic:
(nnnorm_surjective E).range_eq

Premises used: nnnorm_surjective, Function.Surjective.range_eq
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
x : E
r : ℝ
⊢ (sphere x r).Nonempty ↔ 0 ≤ r

Tactic:
⟨fun h => nonempty_closedBall.1 (h.mono sphere_subset_closedBall), fun hr => ?_⟩

Premises used: Set.Nonempty.mono, Metric.nonempty_closedBall, Iff.intro, Iff.mp, Metric.sphere_subset_closedBall
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
x : E
r : ℝ
refine : ∀ (hr : 0 ≤ r), (sphere x r).Nonempty
⊢ (sphere x r).Nonempty ↔ 0 ≤ r

Tactic:
refine ⟨fun h => nonempty_closedBall.1 (h.mono sphere_subset_closedBall), fun hr => ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
x : E
r : ℝ
hr : 0 ≤ r
obtain : ∀ (y : E) (hy : ‖y‖ = r), (sphere x r).Nonempty
⊢ (sphere x r).Nonempty

Tactic:
obtain ⟨y, hy⟩ := exists_norm_eq E hr

Premises used: exists_norm_eq
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : ‖y‖ = r
⊢ x + y ∈ sphere x r

Tactic:
simpa using hy
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NontrivialTopology E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : ‖y‖ = r
⊢ (sphere x r).Nonempty

Tactic:
exact ⟨x + y, by simpa using hy⟩
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
inl : interior (closedBall x 0) = ball x 0
inr : ∀ (hr : r ≠ 0), interior (closedBall x r) = ball x r
⊢ interior (closedBall x r) = ball x r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
inl : interior {x} = ball x 0
inl₁ : Eq (α := Set E) (interior {x}) ∅
inl₂ inl₃ : Eq.{u_1 + 1} (α := Set E) ∅ ∅
⊢ interior (closedBall x 0) = ball x 0

Tactic:
rw [closedBall_zero, ball_zero, interior_singleton]

Premises used: interior_singleton, Metric.ball_zero, Metric.closedBall_zero
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r

Tactic:
interior_closedBall x hr

Premises used: interior_closedBall
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Real
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r

Tactic:
exact interior_closedBall x hr

Premises used: interior_closedBall