awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
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 r, closedBall_diff_ball]

Premises used: frontier, Metric.closure_closedBall, Metric.closedBall_diff_ball, 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 : ℝ
rw : interior (frontier (closedBall x r)) = ∅
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set E) ∅ ∅
⊢ interior (sphere x r) = ∅

Tactic:
rw [← frontier_closedBall' x, 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 : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
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, diff_empty]

Premises used: IsClosed.frontier_eq, Set.diff_empty, Metric.isClosed_sphere, interior_sphere'
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
h : SameRay ℝ x y
rcases :
  ∀ (u : E) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)), ‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖
⊢ ‖x + y‖ = ‖x‖ + ‖y‖

Tactic:
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩

Premises used: SameRay.exists_eq_smul, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
rw : ‖(a + b) • u‖ = ‖a • u‖ + ‖b • u‖
rw₁ : (a + b) * ‖u‖ = ‖a • u‖ + ‖b • u‖
rw₂ : (a + b) * ‖u‖ = a * ‖u‖ + ‖b • u‖
rw₃ : (a + b) * ‖u‖ = a * ‖u‖ + b * ‖u‖
rw₄ rw₅ : a * ‖u‖ + b * ‖u‖ = a * ‖u‖ + b * ‖u‖
⊢ ‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖

Tactic:
rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha,
    norm_smul_of_nonneg hb, add_mul]

Premises used: add_mul, norm_smul_of_nonneg, add_nonneg, add_smul
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
h : SameRay ℝ x y
rcases :
  ∀ (u : E) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)), ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
⊢ ‖x - y‖ = |‖x‖ - ‖y‖|

Tactic:
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩

Premises used: SameRay.exists_eq_smul, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
inr :
  ∀
    (H :
      ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
        ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|)
    (hab : ¬b ≤ a), ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
wlog :
  ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
    ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Tactic:
wlog hab : b ≤ a generalizing a b with H
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
H :
  ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
    ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ SameRay ℝ (b • u) (a • u)

Tactic:
rw [SameRay.sameRay_comm] at h

Premises used: SameRay.sameRay_comm
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
H :
  ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
    ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
h₁ : SameRay ℝ (b • u) (a • u)
⊢ ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
    ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Tactic:
rw [SameRay.sameRay_comm] at h

Premises used: SameRay.sameRay_comm
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
H :
  ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
    ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
h₁ : SameRay ℝ (b • u) (a • u)
H₁ :
  ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
    ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
⊢ ¬b ≤ a

Tactic:
rw [SameRay.sameRay_comm] at h

Premises used: SameRay.sameRay_comm
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
    ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
inr : ‖b • u - a • u‖ = |‖b • u‖ - ‖a • u‖|
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Tactic:
rw [norm_sub_rev, abs_sub_comm]

Premises used: abs_sub_comm, norm_sub_rev
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
    ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖b • u - a • u‖ = |‖b • u‖ - ‖a • u‖|

Tactic:
H b a hb ha h (le_of_not_ge hab)

Premises used: le_of_not_ge
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)) (hab : b ≤ a),
    ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖b • u - a • u‖ = |‖b • u‖ - ‖a • u‖|

Tactic:
exact H b a hb ha h (le_of_not_ge hab)

Premises used: le_of_not_ge
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : b ≤ a
⊢ 0 ≤ a - b

Tactic:
rw [← sub_nonneg] at hab

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : 0 ≤ a - b
rw : ‖(a - b) • u‖ = |‖a • u‖ - ‖b • u‖|
rw₁ : (a - b) * ‖u‖ = |‖a • u‖ - ‖b • u‖|
rw₂ : (a - b) * ‖u‖ = |a * ‖u‖ - ‖b • u‖|
rw₃ : (a - b) * ‖u‖ = |a * ‖u‖ - b * ‖u‖|
rw₄ : (a - b) * ‖u‖ = |(a - b) * ‖u‖|
rw₅ rw₆ : (a - b) * ‖u‖ = (a - b) * ‖u‖
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Tactic:
rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha, norm_smul_of_nonneg hb, ←
    sub_mul, abs_of_nonneg (mul_nonneg hab (norm_nonneg _))]

Premises used: mul_nonneg, norm_smul_of_nonneg, sub_smul, sub_mul, abs_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
h : SameRay ℝ x y
rcases :
  ∀ (u : E) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : SameRay ℝ (a • u) (b • u)), ‖a • u‖ • b • u = ‖b • u‖ • a • u
⊢ ‖x‖ • y = ‖y‖ • x

Tactic:
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩

Premises used: SameRay.exists_eq_smul, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
simp : a • ‖u‖ • b • u = b • ‖u‖ • a • u
⊢ ‖a • u‖ • b • u = ‖b • u‖ • a • u

Tactic:
simp only [norm_smul_of_nonneg, *, mul_smul]

Premises used: norm_smul_of_nonneg, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
rw : ‖u‖ • a • b • u = b • ‖u‖ • a • u
rw₁ : ‖u‖ • a • b • u = ‖u‖ • b • a • u
rw₂ rw₃ : ‖u‖ • b • a • u = ‖u‖ • b • a • u
⊢ a • ‖u‖ • b • u = b • ‖u‖ • a • u

Tactic:
rw [smul_comm, smul_comm b, smul_comm a b u]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
hx : x ≠ 0
y : F
hy : Membership.mem (γ := Set F) {y : F | SameRay ℝ x y} y
z : F
hz : Membership.mem (γ := Set F) {y : F | SameRay ℝ x y} z
h : ‖y‖ = ‖z‖
rcases :
  ∀ (r : ℝ) (hr : 0 ≤ r) (hy : Membership.mem (γ := Set F) {y : F | SameRay ℝ x y} (r • x)) (h : ‖r • x‖ = ‖z‖),
    r • x = z
⊢ y = z

Tactic:
rcases hy.exists_nonneg_left hx with ⟨r, hr, rfl⟩

Premises used: SameRay.exists_nonneg_left, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
hx : x ≠ 0
z : F
hz : Membership.mem (γ := Set F) {y : F | SameRay ℝ x y} z
r : ℝ
hr : 0 ≤ r
hy : Membership.mem (γ := Set F) {y : F | SameRay ℝ x y} (r • x)
h : ‖r • x‖ = ‖z‖
rcases :
  ∀ (s : ℝ) (hs : 0 ≤ s) (hz : Membership.mem (γ := Set F) {y : F | SameRay ℝ x y} (s • x)) (h : ‖r • x‖ = ‖s • x‖),
    r • x = s • x
⊢ r • x = z

Tactic:
rcases hz.exists_nonneg_left hx with ⟨s, hs, rfl⟩

Premises used: SameRay.exists_nonneg_left, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : Membership.mem (γ := Set F) {y : F | SameRay ℝ x y} (r • x)
s : ℝ
hs : 0 ≤ s
hz : Membership.mem (γ := Set F) {y : F | SameRay ℝ x y} (s • x)
h : ‖r • x‖ = ‖s • x‖
⊢ r = s

Tactic:
rw [norm_smul, norm_smul, mul_left_inj' (norm_ne_zero_iff.2 hx), norm_of_nonneg hr,
    norm_of_nonneg hs] at h

Premises used: Iff.mpr, norm_smul, norm_ne_zero_iff, mul_left_inj', Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : Membership.mem (γ := Set F) {y : F | SameRay ℝ x y} (r • x)
s : ℝ
hs : 0 ≤ s
hz : Membership.mem (γ := Set F) {y : F | SameRay ℝ x y} (s • x)
h : r = s
rw rw₁ : s • x = s • x
⊢ r • x = s • x

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
y : F
hy : y ≠ 0
⊢ Set.InjOn.{u_2, 0} (α := F) Norm.norm {x : F | SameRay ℝ x y}

Tactic:
simpa only [SameRay.sameRay_comm] using norm_injOn_ray_left hy

Premises used: SameRay.sameRay_comm, norm_injOn_ray_left
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
⊢ SameRay ℝ x y ↔ ‖x‖ • y = ‖y‖ • x

Tactic:
⟨SameRay.norm_smul_eq, fun h =>
    or_iff_not_imp_left.2 fun hx =>
      or_iff_not_imp_left.2 fun hy => ⟨‖y‖, ‖x‖, norm_pos_iff.2 hy, norm_pos_iff.2 hx, h.symm⟩⟩

Premises used: Iff.mpr, Norm.norm, norm_pos_iff, Classical.or_iff_not_imp_left, And.intro, Iff.intro, Exists.intro, SameRay.norm_smul_eq, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
ha : ‖y‖ ≠ 0
ha₁ : ‖x‖ ≠ 0
⊢ SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
rw [inv_smul_eq_iff₀, smul_comm, eq_comm, inv_smul_eq_iff₀, sameRay_iff_norm_smul_eq]

Premises used: eq_comm, inv_smul_eq_iff₀, SMulCommClass.smul_comm, sameRay_iff_norm_smul_eq
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
ha ha₁ ha₂ ha₃ : y ≠ 0
⊢ ‖y‖ ≠ 0

Tactic:
rwa [norm_ne_zero_iff]

Premises used: norm_ne_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
ha ha₁ ha₂ ha₃ : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
rwa [norm_ne_zero_iff]

Premises used: norm_ne_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
inl :
  SameRay ℝ 0 y ↔ Eq.{u_2 + 1} (α := F) 0 0 ∨ y = 0 ∨ HSMul.hSMul (β := F) (Norm.norm.{u_2} (E := F) 0)⁻¹ 0 = ‖y‖⁻¹ • y
inr : ∀ (hx : x ≠ 0), SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
y : F
⊢ SameRay ℝ 0 y ↔ Eq.{u_2 + 1} (α := F) 0 0 ∨ y = 0 ∨ HSMul.hSMul (β := F) (Norm.norm.{u_2} (E := F) 0)⁻¹ 0 = ‖y‖⁻¹ • y

Tactic:
simp [SameRay.zero_left]

Premises used: SameRay.zero_left
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
hx : x ≠ 0
inr :
  SameRay ℝ x 0 ↔ x = 0 ∨ Eq.{u_2 + 1} (α := F) 0 0 ∨ ‖x‖⁻¹ • x = HSMul.hSMul (β := F) (Norm.norm.{u_2} (E := F) 0)⁻¹ 0
inr₁ : ∀ (hy : y ≠ 0), SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ Eq.{u_2 + 1} (α := F) 0 0 ∨ ‖x‖⁻¹ • x = HSMul.hSMul (β := F) (Norm.norm.{u_2} (E := F) 0)⁻¹ 0

Tactic:
simp [SameRay.zero_right]

Premises used: SameRay.zero_right
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
simp only [sameRay_iff_inv_norm_smul_eq_of_ne hx hy, *, false_or]

Premises used: sameRay_iff_inv_norm_smul_eq_of_ne, false_or
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
inl : ∀ (h : ‖x‖ = Norm.norm.{u_2} (E := F) 0), SameRay ℝ x 0 ↔ x = 0
inr : ∀ (hy : y ≠ 0), SameRay ℝ x y ↔ x = y
⊢ SameRay ℝ x y ↔ x = y

Tactic:
obtain rfl | hy := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
h : ‖x‖ = Norm.norm.{u_2} (E := F) 0
⊢ x = 0

Tactic:
rw [norm_zero, norm_eq_zero] at h

Premises used: norm_eq_zero, norm_zero
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
h : x = 0
⊢ SameRay ℝ x 0 ↔ x = 0

Tactic:
iff_of_true (SameRay.zero_right _) h

Premises used: SameRay.zero_right, iff_of_true
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
h : x = 0
⊢ SameRay ℝ x 0 ↔ x = 0

Tactic:
exact iff_of_true (SameRay.zero_right _) h

Premises used: SameRay.zero_right, iff_of_true
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = y

Tactic:
⟨fun hxy => norm_injOn_ray_right hy hxy SameRay.rfl h, fun hxy => hxy ▸ SameRay.rfl⟩

Premises used: norm_injOn_ray_right, Eq.rec, Iff.intro, SameRay.rfl
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = y

Tactic:
exact ⟨fun hxy => norm_injOn_ray_right hy hxy SameRay.rfl h, fun hxy => hxy ▸ SameRay.rfl⟩
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
⊢ ¬SameRay ℝ x y ↔ x ≠ y

Tactic:
(sameRay_iff_of_norm_eq h).not

Premises used: sameRay_iff_of_norm_eq, Iff.not
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
h : SameRay ℝ x y
hn : ‖x‖ = ‖y‖
⊢ x = y

Tactic:
(sameRay_iff_of_norm_eq hn).mp h

Premises used: sameRay_iff_of_norm_eq, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.Ray
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
h : SameRay ℝ x y
⊢ ‖x‖ = ‖y‖ ↔ x = y

Tactic:
⟨h.eq_of_norm_eq, fun h => h ▸ rfl⟩

Premises used: SameRay.eq_of_norm_eq, Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
⊢ ∃ (x : E), x ∉ F

Tactic:
hF
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
r : ℝ
hr : r < 1
obtain : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖

Tactic:
obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
⊢ (↑F : Set E).Nonempty

Tactic:
have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
hFn : (↑F : Set E).Nonempty
⊢ 0 < d

Tactic:
have hdp : 0 < d :=
      lt_of_le_of_ne Metric.infDist_nonneg fun heq =>
        hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
hFn : (↑F : Set E).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
simp : LT.lt (α := ℝ) 2⁻¹ 1
⊢ r' < 1

Tactic:
simp only [r', max_lt_iff, hr, true_and]

Premises used: max_lt_iff, true_and
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
hFn : (↑F : Set E).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
⊢ LT.lt (α := ℝ) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
hFn : (↑F : Set E).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
⊢ r' < 1

Tactic:
have hr' : r' < 1 := by
      simp only [r', max_lt_iff, hr, true_and]
      norm_num
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
hFn : (↑F : Set E).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
⊢ LT.lt (α := ℝ) 0 2⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
hFn : (↑F : Set E).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
⊢ 0 < r'

Tactic:
have hlt : 0 < r' := lt_of_lt_of_le (by simp) (le_max_right r 2⁻¹)
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
hFn : (↑F : Set E).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
⊢ d < d / r'

Tactic:
have hdlt : d < d / r' := (lt_div_iff₀ hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
hFn : (↑F : Set E).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
⊢ ∃ y ∈ F, dist x y < d / r'

Tactic:
(Metric.infDist_lt_iff hFn).mp hdlt

Premises used: Metric.infDist_lt_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
hFn : (↑F : Set E).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
obtain : ∀ (y₀ : E) (hy₀F : y₀ ∈ F) (hxy₀ : dist x y₀ < d / r'), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖

Tactic:
obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt

Premises used: Metric.infDist_lt_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
hFn : (↑F : Set E).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
by_contra : ∀ (h : x - y₀ ∈ F), False
⊢ x - y₀ ∉ F

Tactic:
by_contra h
-- Module: Mathlib.Analysis.Normed.Module.RieszLemma
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x (↑F : Set E)
hFn : (↑F : Set E).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
h : x - y₀ ∈ F
⊢ x - y₀ + y₀ ∈ F

Tactic:
have : x - y₀ + y₀ ∈ F := F.add_mem h hy₀F