awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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: classical
    obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
    let d := Metric.infDist x F
    have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
    have hdp : 0 < d :=
      lt_of_le_of_ne Metric.infDist_nonneg fun heq =>
        hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
    let r' := max r 2⁻¹
    have hr' : r' < 1 := by
      simp only [r', max_lt_iff, hr, true_and]
      norm_num
    have hlt : 0 < r' := lt_of_lt_of_le (by simp) (le_max_right r 2⁻¹)
    have hdlt : d < d / r' := (lt_div_iff₀ hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
    obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt
    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
    refine ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt ?_⟩
    have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
    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]
Cleared hypotheses: hF
-- 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
obtain : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₁ : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have obtain₂ : ∀ (x : E) (hx : x ∉ F) (hFn : (↑F : Set E).Nonempty), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
Tactic: classical
    obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
    let d := Metric.infDist x F
    have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
    have hdp : 0 < d :=
      lt_of_le_of_ne Metric.infDist_nonneg fun heq =>
        hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
    let r' := max r 2⁻¹
    have hr' : r' < 1 := by
      simp only [r', max_lt_iff, hr, true_and]
      norm_num
    have hlt : 0 < r' := lt_of_lt_of_le (by simp) (le_max_right r 2⁻¹)
    have hdlt : d < d / r' := (lt_div_iff₀ hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
    obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt
    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
    refine ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt ?_⟩
    have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
    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]
Cleared hypotheses: hF
-- 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
obtain : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₁ : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₂ : ∀ (x : E) (hx : x ∉ F) (hFn : (↑F : Set E).Nonempty), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have obtain₃ : ∀ (x : E) (hx : x ∉ F),
  let d := infDist x (↑F : Set E);
  ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
Tactic: classical
    obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
    let d := Metric.infDist x F
    have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
    have hdp : 0 < d :=
      lt_of_le_of_ne Metric.infDist_nonneg fun heq =>
        hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
    let r' := max r 2⁻¹
    have hr' : r' < 1 := by
      simp only [r', max_lt_iff, hr, true_and]
      norm_num
    have hlt : 0 < r' := lt_of_lt_of_le (by simp) (le_max_right r 2⁻¹)
    have hdlt : d < d / r' := (lt_div_iff₀ hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
    obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt
    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
    refine ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt ?_⟩
    have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
    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]
Cleared hypotheses: hF
-- 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
obtain : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₁ : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₂ : ∀ (x : E) (hx : x ∉ F) (hFn : (↑F : Set E).Nonempty), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₃ obtain₄ :
  ∀ (x : E) (hx : x ∉ F),
    let d := infDist x (↑F : Set E);
    ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have obtain₅ : ∀ (x : E) (hx : x ∉ F),
  let d := infDist x (↑F : Set E);
  ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d),
    let r' := max r 2⁻¹;
    ∀ (hr' : r' < 1), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
Tactic: classical
    obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
    let d := Metric.infDist x F
    have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
    have hdp : 0 < d :=
      lt_of_le_of_ne Metric.infDist_nonneg fun heq =>
        hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
    let r' := max r 2⁻¹
    have hr' : r' < 1 := by
      simp only [r', max_lt_iff, hr, true_and]
      norm_num
    have hlt : 0 < r' := lt_of_lt_of_le (by simp) (le_max_right r 2⁻¹)
    have hdlt : d < d / r' := (lt_div_iff₀ hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
    obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt
    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
    refine ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt ?_⟩
    have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
    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]
Cleared hypotheses: hF
-- 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
obtain : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₁ : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₂ : ∀ (x : E) (hx : x ∉ F) (hFn : (↑F : Set E).Nonempty), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₃ obtain₄ :
  ∀ (x : E) (hx : x ∉ F),
    let d := infDist x (↑F : Set E);
    ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₅ :
  ∀ (x : E) (hx : x ∉ F),
    let d := infDist x (↑F : Set E);
    ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d),
      let r' := max r 2⁻¹;
      ∀ (hr' : r' < 1), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have obtain₆ : ∀ (x : E) (hx : x ∉ F),
  let d := infDist x (↑F : Set E);
  ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d),
    let r' := max r 2⁻¹;
    ∀ (hr' : r' < 1) (hlt : 0 < r'), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
Tactic: classical
    obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
    let d := Metric.infDist x F
    have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
    have hdp : 0 < d :=
      lt_of_le_of_ne Metric.infDist_nonneg fun heq =>
        hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
    let r' := max r 2⁻¹
    have hr' : r' < 1 := by
      simp only [r', max_lt_iff, hr, true_and]
      norm_num
    have hlt : 0 < r' := lt_of_lt_of_le (by simp) (le_max_right r 2⁻¹)
    have hdlt : d < d / r' := (lt_div_iff₀ hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
    obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt
    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
    refine ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt ?_⟩
    have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
    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]
Cleared hypotheses: hF
-- 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
obtain : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₁ : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₂ : ∀ (x : E) (hx : x ∉ F) (hFn : (↑F : Set E).Nonempty), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₃ obtain₄ :
  ∀ (x : E) (hx : x ∉ F),
    let d := infDist x (↑F : Set E);
    ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₅ :
  ∀ (x : E) (hx : x ∉ F),
    let d := infDist x (↑F : Set E);
    ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d),
      let r' := max r 2⁻¹;
      ∀ (hr' : r' < 1), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₆ :
  ∀ (x : E) (hx : x ∉ F),
    let d := infDist x (↑F : Set E);
    ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d),
      let r' := max r 2⁻¹;
      ∀ (hr' : r' < 1) (hlt : 0 < r'), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have obtain₇ : ∀ (x : E) (hx : x ∉ F),
  let d := infDist x (↑F : Set E);
  ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d),
    let r' := max r 2⁻¹;
    ∀ (hr' : r' < 1) (hlt : 0 < r') (hdlt : d < d / r'), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
Tactic: classical
    obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
    let d := Metric.infDist x F
    have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
    have hdp : 0 < d :=
      lt_of_le_of_ne Metric.infDist_nonneg fun heq =>
        hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
    let r' := max r 2⁻¹
    have hr' : r' < 1 := by
      simp only [r', max_lt_iff, hr, true_and]
      norm_num
    have hlt : 0 < r' := lt_of_lt_of_le (by simp) (le_max_right r 2⁻¹)
    have hdlt : d < d / r' := (lt_div_iff₀ hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
    obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt
    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
    refine ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt ?_⟩
    have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
    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]
Cleared hypotheses: hF
-- 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
obtain : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₁ : ∀ (x : E) (hx : x ∉ F), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₂ : ∀ (x : E) (hx : x ∉ F) (hFn : (↑F : Set E).Nonempty), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₃ obtain₄ :
  ∀ (x : E) (hx : x ∉ F),
    let d := infDist x (↑F : Set E);
    ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₅ :
  ∀ (x : E) (hx : x ∉ F),
    let d := infDist x (↑F : Set E);
    ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d),
      let r' := max r 2⁻¹;
      ∀ (hr' : r' < 1), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₆ :
  ∀ (x : E) (hx : x ∉ F),
    let d := infDist x (↑F : Set E);
    ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d),
      let r' := max r 2⁻¹;
      ∀ (hr' : r' < 1) (hlt : 0 < r'), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
obtain₇ :
  ∀ (x : E) (hx : x ∉ F),
    let d := infDist x (↑F : Set E);
    ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d),
      let r' := max r 2⁻¹;
      ∀ (hr' : r' < 1) (hlt : 0 < r') (hdlt : d < d / r'), ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
⊢ ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
have obtain₈ : ∀ (x : E) (hx : x ∉ F),
  let d := infDist x (↑F : Set E);
  ∀ (hFn : (↑F : Set E).Nonempty) (hdp : 0 < d),
    let 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‖
Tactic: classical
    obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
    let d := Metric.infDist x F
    have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
    have hdp : 0 < d :=
      lt_of_le_of_ne Metric.infDist_nonneg fun heq =>
        hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
    let r' := max r 2⁻¹
    have hr' : r' < 1 := by
      simp only [r', max_lt_iff, hr, true_and]
      norm_num
    have hlt : 0 < r' := lt_of_lt_of_le (by simp) (le_max_right r 2⁻¹)
    have hdlt : d < d / r' := (lt_div_iff₀ hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
    obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt
    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
    refine ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt ?_⟩
    have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
    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]
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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
⊢ ∃ (x₀ : E), ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
have Rpos : 0 < R
Tactic: have Rpos : 0 < R := (norm_nonneg _).trans_lt 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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
⊢ ‖c‖ / R < 1
have rw : ‖c‖ < 1 * R
Tactic: rw [div_lt_iff₀ Rpos]
-- 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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
⊢ ∃ (x₀ : E), ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
have this : ‖c‖ / R < 1
Tactic: have : ‖c‖ / R < 1 := by
    rw [div_lt_iff₀ Rpos]
    simpa using 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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
⊢ ∃ (x₀ : E), ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
have rcases : ∀ (x : E) (xF : x ∉ F) (hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖), ∃ (x₀ : E), ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
Tactic: rcases riesz_lemma hFc hF this with ⟨x, xF, hx⟩
-- 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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
⊢ ∃ (x₀ : E), ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
have x0 : x ≠ 0
Tactic: have x0 : x ≠ 0 := fun H => by simp [H] at xF
-- 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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
⊢ ∃ (x₀ : E), ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
have obtain : ∀ (d : 𝕜) (d0 : d ≠ 0) (dxlt : ‖d • x‖ < R) (ledx : R / ‖c‖ ≤ ‖d • x‖), ∃ (x₀ : E), ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
Tactic: obtain ⟨d, d0, dxlt, ledx, -⟩ :
    ∃ d : 𝕜, d ≠ 0 ∧ ‖d • x‖ < R ∧ R / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ R⁻¹ * ‖c‖ * ‖x‖ :=
    rescale_to_shell hc Rpos x0
-- 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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
⊢ ∃ (x₀ : E), ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
have refine : ∀ (y : E) (hy : y ∈ F), 1 ≤ ‖d • x - y‖
Tactic: refine ⟨d • x, dxlt.le, fun y hy => ?_⟩
-- 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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
⊢ 1 ≤ ‖d • x - y‖
have yy' : y = d • y'
Tactic: have yy' : y = d • y' := by simp [y', smul_smul, mul_inv_cancel₀ d0]
-- 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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * (R / ‖c‖) ≤ ‖c‖ / R * ‖d • x‖
have ha : 0 ≤ ‖c‖ / 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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * ‖d • x‖ = ‖d‖ * (‖c‖ / R * ‖x‖)
have simp : ‖c‖ / R * (‖d‖ * ‖x‖) = ‖d‖ * (‖c‖ / R * ‖x‖)
Tactic: simp only [norm_smul]
-- 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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖d‖ * (‖c‖ / R * ‖x‖) ≤ ‖d‖ * ‖x - y'‖
have hbc : ‖c‖ / R * ‖x‖ ≤ ‖x - y'‖
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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖d‖ * ‖x - y'‖ = ‖d • x - y‖
have rw : ‖d‖ * ‖x - y'‖ = ‖d • x - d • y'‖
Tactic: rw [yy', ← smul_sub, norm_smul]
-- 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
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
hF : ∃ (x : E), x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
rw : ‖d‖ * ‖x - y'‖ = ‖d • x - d • y'‖
⊢ ‖d‖ * ‖x - y'‖ = ‖d • x - y‖
have rw₁ : ‖d‖ * ‖x - y'‖ = ‖d • (x - y')‖
Tactic: rw [yy', ← smul_sub, norm_smul]