awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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‖|
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
have rw₁ : (a - 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 _))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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‖|
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
have rw₂ : (a - 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 _))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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‖|
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
have rw₃ : (a - 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 _))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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‖|
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
have rw₄ : (a - b) * ‖u‖ = |(a - 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 _))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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‖|
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
have rw₅ : (a - b) * ‖u‖ = (a - 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 _))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
h : SameRay ℝ x y
⊢ ‖x‖ • y = ‖y‖ • x
have 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
Tactic: rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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)
⊢ ‖a • u‖ • b • u = ‖b • u‖ • a • u
have simp : a • ‖u‖ • b • u = b • ‖u‖ • a • u
Tactic: simp only [norm_smul_of_nonneg, *, mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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)
⊢ a • ‖u‖ • b • u = b • ‖u‖ • a • u
have rw : ‖u‖ • a • b • u = b • ‖u‖ • a • u
Tactic: rw [smul_comm, smul_comm b, smul_comm a b u]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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
⊢ a • ‖u‖ • b • u = b • ‖u‖ • a • u
have rw₁ : ‖u‖ • a • b • u = ‖u‖ • b • a • u
Tactic: rw [smul_comm, smul_comm b, smul_comm a b u]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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
⊢ a • ‖u‖ • b • u = b • ‖u‖ • a • u
have rw₂ : ‖u‖ • b • a • u = ‖u‖ • b • a • u
Tactic: rw [smul_comm, smul_comm b, smul_comm a b u]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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‖
⊢ y = z
have rcases : ∀ (r : ℝ) (hr : 0 ≤ r) (hy : Membership.mem (γ := Set F) {y : F | SameRay ℝ x y} (r • x)) (h : ‖r • x‖ = ‖z‖), r • x = z
Tactic: rcases hy.exists_nonneg_left hx with ⟨r, hr, rfl⟩
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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‖
⊢ r • x = z
have 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
Tactic: rcases hz.exists_nonneg_left hx with ⟨s, hs, rfl⟩
Cleared hypotheses: z, hz, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (hypothesis)
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 • x = s • x
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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
⊢ r • x = s • x
have rw : s • x = s • x
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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‖⁻¹ • x = ‖y‖⁻¹ • y
have ha : ‖y‖ ≠ 0
Tactic: rw [inv_smul_eq_iff₀, smul_comm, eq_comm, inv_smul_eq_iff₀, sameRay_iff_norm_smul_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
ha : ‖y‖ ≠ 0
⊢ SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
have ha₁ : ‖x‖ ≠ 0
Tactic: rw [inv_smul_eq_iff₀, smul_comm, eq_comm, inv_smul_eq_iff₀, sameRay_iff_norm_smul_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
have 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
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
have inr : ∀ (hx : x ≠ 0), SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
have 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
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
have inr₁ : ∀ (hy : y ≠ 0), SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
⊢ SameRay ℝ x y ↔ x = y
have inl : ∀ (h : ‖x‖ = Norm.norm.{u_2} (E := F) 0), SameRay ℝ x 0 ↔ x = 0
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (goal)
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
⊢ SameRay ℝ x y ↔ x = y
have inr : ∀ (hy : y ≠ 0), SameRay ℝ x y ↔ x = y
Tactic: obtain rfl | hy := eq_or_ne y 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ray (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
h : ‖x‖ = Norm.norm.{u_2} (E := F) 0
⊢ SameRay ℝ x 0 ↔ x = 0
have h₁ : x = 0
Tactic: rw [norm_zero, norm_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
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₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have obtain : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
Tactic: obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
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)
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have hFn : (↑F : Set E).Nonempty
Tactic: have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
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
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have hdp : 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
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
have simp : LT.lt (α := ℝ) 2⁻¹ 1
Tactic: simp only [r', max_lt_iff, hr, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
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⁻¹
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have hr' : r' < 1
Tactic: have hr' : r' < 1 := by
      simp only [r', max_lt_iff, hr, true_and]
      norm_num
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
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
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have hlt : 0 < r'
Tactic: have hlt : 0 < r' := lt_of_lt_of_le (by simp) (le_max_right r 2⁻¹)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
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'
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have hdlt : d < d / r'
Tactic: have hdlt : d < d / r' := (lt_div_iff₀ hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
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'
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have obtain : ∀ (y₀ : E) (hy₀F : y₀ ∈ F) (hxy₀ : dist x y₀ < d / r'), ∃ 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
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
⊢ False
have this : x - y₀ + y₀ ∈ F
Tactic: have : x - y₀ + y₀ ∈ F := F.add_mem h hy₀F
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
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
this : x - y₀ + y₀ ∈ F
⊢ False
have this₁ : x ∈ F
Tactic: simp only [neg_add_cancel_right, sub_eq_add_neg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
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'
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have x_ne_y₀ : x - y₀ ∉ F
Tactic: have x_ne_y₀ : x - y₀ ∉ F := by
      by_contra h
      have : x - y₀ + y₀ ∈ F := F.add_mem h hy₀F
      simp only [neg_add_cancel_right, sub_eq_add_neg] at this
      exact hx this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
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'
x_ne_y₀ : x - y₀ ∉ F
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have refine : ∀ (y : E) (hy : y ∈ F), r * ‖x - y₀‖ < ‖x - y₀ - y‖
Tactic: refine ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (hypothesis)
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'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
⊢ r * ‖x - y₀‖ < ‖x - y₀ - y‖
have hy₀y : y₀ + y ∈ F
Tactic: have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
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'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖
have hbc : r ≤ r'
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
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'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ r' * ‖x - y₀‖ < d
have rw : r' * dist x y₀ < d
Tactic: rw [← dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
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'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ dist x (y₀ + y) = ‖x - y₀ - y‖
have rw : dist x (y₀ + y) = ‖x - (y₀ + y)‖
Tactic: rw [sub_sub, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
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'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
rw : dist x (y₀ + y) = ‖x - (y₀ + y)‖
⊢ dist x (y₀ + y) = ‖x - y₀ - y‖
have rw₁ : ‖x - (y₀ + y)‖ = ‖x - (y₀ + y)‖
Tactic: rw [sub_sub, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
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'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ r * ‖x - y₀‖ < ‖x - y₀ - y‖
have r₁ : r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖
Tactic: calc
      r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖ := by gcongr; apply le_max_left
      _ < d := by
        rw [← dist_eq_norm]
        exact (lt_div_iff₀' hlt).1 hxy₀
      _ ≤ dist x (y₀ + y) := Metric.infDist_le_dist_of_mem hy₀y
      _ = ‖x - y₀ - y‖ := by rw [sub_sub, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
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'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
r₁ : r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖
⊢ r * ‖x - y₀‖ < ‖x - y₀ - y‖
have r₂ : r' * ‖x - y₀‖ < d
Tactic: calc
      r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖ := by gcongr; apply le_max_left
      _ < d := by
        rw [← dist_eq_norm]
        exact (lt_div_iff₀' hlt).1 hxy₀
      _ ≤ dist x (y₀ + y) := Metric.infDist_le_dist_of_mem hy₀y
      _ = ‖x - y₀ - y‖ := by rw [sub_sub, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RieszLemma (goal)
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'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
r₁ : r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖
r₂ : r' * ‖x - y₀‖ < d
⊢ r * ‖x - y₀‖ < ‖x - y₀ - y‖
have r₃ : dist x (y₀ + y) = ‖x - y₀ - y‖
Tactic: calc
      r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖ := by gcongr; apply le_max_left
      _ < d := by
        rw [← dist_eq_norm]
        exact (lt_div_iff₀' hlt).1 hxy₀
      _ ≤ dist x (y₀ + y) := Metric.infDist_le_dist_of_mem hy₀y
      _ = ‖x - y₀ - y‖ := by rw [sub_sub, dist_eq_norm]