awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
E : Type u_6
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) (k • e)
inr :
  Membership.mem (γ := Set E) (ball 0 ‖e‖)
      (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) :
        E) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
inr₁ :
  ‖(↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) :
          E)‖ <
      ‖e‖ ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
inr₂ :
  ‖k • e‖ < ‖e‖ ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
inr₃ :
  ‖k • e‖ < ‖e‖ ↔
    Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx = 0
inr₄ :
  ‖k • e‖ < ‖e‖ ↔
    (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) :
        E) =
      (↑0 : E)
inr₅ : ‖k • e‖ < ‖e‖ ↔ k • e = (↑0 : E)
inr₆ : ‖k • e‖ < ‖e‖ ↔ k • e = 0
inr₇ : norm (E := ℚ) (↑k : ℚ) * ‖e‖ < ‖e‖ ↔ k • e = 0
inr₈ : ‖k‖ * ‖e‖ < ‖e‖ ↔ k • e = 0
inr₉ : |(↑k : ℝ)| * ‖e‖ < ‖e‖ ↔ k • e = 0
inr₁₀ : LT.lt (α := ℝ) |(↑k : ℝ)| 1 ↔ k • e = 0
inr₁₁ : LT.lt (α := ℝ) |(↑k : ℝ)| (↑1 : ℝ) ↔ k • e = 0
inr₁₂ : LT.lt (α := ℝ) (↑|k| : ℝ) (↑1 : ℝ) ↔ k • e = 0
inr₁₃ : |k| < 1 ↔ k • e = 0
inr₁₄ : k = 0 ↔ k • e = 0
⊢ Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' ball 0 ‖e‖)
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
have inr₁₅ : k = 0 ↔ k = 0 ∨ e = 0
Tactic: rw [mem_preimage, mem_ball_zero_iff, AddSubgroup.coe_mk, mem_singleton_iff, Subtype.ext_iff,
      AddSubgroup.coe_mk, AddSubgroup.coe_zero, norm_zsmul ℚ k e, Int.norm_cast_rat,
      Int.norm_eq_abs, mul_lt_iff_lt_one_left (norm_pos_iff.mpr he), ← @Int.cast_one ℝ _,
      ← Int.cast_abs, Int.cast_lt, Int.abs_lt_one_iff, smul_eq_zero, or_iff_left he]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
E : Type u_6
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) (k • e)
inr :
  Membership.mem (γ := Set E) (ball 0 ‖e‖)
      (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) :
        E) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
inr₁ :
  ‖(↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) :
          E)‖ <
      ‖e‖ ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
inr₂ :
  ‖k • e‖ < ‖e‖ ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
inr₃ :
  ‖k • e‖ < ‖e‖ ↔
    Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx = 0
inr₄ :
  ‖k • e‖ < ‖e‖ ↔
    (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) :
        E) =
      (↑0 : E)
inr₅ : ‖k • e‖ < ‖e‖ ↔ k • e = (↑0 : E)
inr₆ : ‖k • e‖ < ‖e‖ ↔ k • e = 0
inr₇ : norm (E := ℚ) (↑k : ℚ) * ‖e‖ < ‖e‖ ↔ k • e = 0
inr₈ : ‖k‖ * ‖e‖ < ‖e‖ ↔ k • e = 0
inr₉ : |(↑k : ℝ)| * ‖e‖ < ‖e‖ ↔ k • e = 0
inr₁₀ : LT.lt (α := ℝ) |(↑k : ℝ)| 1 ↔ k • e = 0
inr₁₁ : LT.lt (α := ℝ) |(↑k : ℝ)| (↑1 : ℝ) ↔ k • e = 0
inr₁₂ : LT.lt (α := ℝ) (↑|k| : ℝ) (↑1 : ℝ) ↔ k • e = 0
inr₁₃ : |k| < 1 ↔ k • e = 0
inr₁₄ : k = 0 ↔ k • e = 0
inr₁₅ : k = 0 ↔ k = 0 ∨ e = 0
⊢ Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' ball 0 ‖e‖)
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
have inr₁₆ : k = 0 ↔ k = 0
Tactic: rw [mem_preimage, mem_ball_zero_iff, AddSubgroup.coe_mk, mem_singleton_iff, Subtype.ext_iff,
      AddSubgroup.coe_mk, AddSubgroup.coe_zero, norm_zsmul ℚ k e, Int.norm_cast_rat,
      Int.norm_eq_abs, mul_lt_iff_lt_one_left (norm_pos_iff.mpr he), ← @Int.cast_one ℝ _,
      ← Int.cast_abs, Int.cast_lt, Int.abs_lt_one_iff, smul_eq_zero, or_iff_left he]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ diam (sphere x r) = 2 * r
have apply : 2 * r ≤ diam (sphere x r)
Tactic: apply le_antisymm
    (diam_mono sphere_subset_closedBall isBounded_closedBall |>.trans <| diam_closedBall hr)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 2 * r ≤ diam (sphere x r)
have obtain : ∀ (y : E) (hy : y ≠ 0), 2 * r ≤ diam (sphere x r)
Tactic: obtain ⟨y, hy⟩ := exists_ne (0 : E)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) ≤ diam (sphere x r)
have hx : x + r • ‖y‖⁻¹ • y ∈ sphere x r
Tactic: apply dist_le_diam_of_mem isBounded_sphere
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
hx : x + r • ‖y‖⁻¹ • y ∈ sphere x r
⊢ dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) ≤ diam (sphere x r)
have hy₁ : x - r • ‖y‖⁻¹ • y ∈ sphere x r
Tactic: apply dist_le_diam_of_mem isBounded_sphere
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ 2 * r ≤ diam (sphere x r)
have r₁ : 2 * r = dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y)
Tactic: calc
    2 * r = dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) := by
      simp [dist_eq_norm, ← two_nsmul, ← smul_assoc, norm_smul, abs_of_nonneg hr, hy, mul_assoc]
    _ ≤ diam (sphere x r) := by
      apply dist_le_diam_of_mem isBounded_sphere <;> simp [norm_smul, hy, abs_of_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
r₁ : 2 * r = dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y)
⊢ 2 * r ≤ diam (sphere x r)
have r₂ : dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) ≤ diam (sphere x r)
Tactic: calc
    2 * r = dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) := by
      simp [dist_eq_norm, ← two_nsmul, ← smul_assoc, norm_smul, abs_of_nonneg hr, hy, mul_assoc]
    _ ≤ diam (sphere x r) := by
      apply dist_le_diam_of_mem isBounded_sphere <;> simp [norm_smul, hy, abs_of_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ diam (ball x r) = 2 * r
have refine : ∀ (a : ℝ) (ha : a ≥ 0) (ha' : a < 2) (r' : ℝ) (hr' : r' ≥ 0) (hr'' : r' < r), a * r' ≤ diam (ball x r)
Tactic: refine le_antisymm (diam_ball hr) <|
    mul_le_of_forall_lt_of_nonneg (by positivity) diam_nonneg fun a ha ha' r' hr' hr'' ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
⊢ a * r' ≤ 2 * r'
have ha₁ : 0 ≤ r'
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
⊢ a * r' ≤ diam (ball x r)
have calc : a * r' ≤ 2 * r'
Tactic: calc a * r' ≤ 2 * r' := by gcongr
    _ ≤ _ := by simpa only [← Metric.diam_sphere_eq x hr'.le]
      using diam_mono (sphere_subset_ball hr'') isBounded_ball
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
calc : a * r' ≤ 2 * r'
⊢ a * r' ≤ diam (ball x r)
have calc₁ : 2 * r' ≤ diam (ball x r)
Tactic: calc a * r' ≤ 2 * r' := by gcongr
    _ ≤ _ := by simpa only [← Metric.diam_sphere_eq x hr'.le]
      using diam_mono (sphere_subset_ball hr'') isBounded_ball
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
ι : Type u_6
E : ι → Type u_7
inst_5 : Fintype ι
inst_6 : (i : ι) → SeminormedAddCommGroup (E i)
inst_7 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (E i)
a : 𝕜
f : (i : ι) → E i
⊢ ‖a • f‖ ≤ ‖a‖ * ‖f‖
have simp_rw : LE.le (α := ℝ≥0) (Finset.sup Finset.univ fun (b : ι) ↦ ‖(a • f) b‖₊)
  (Finset.sup Finset.univ fun (a_1 : ι) ↦ ‖a‖₊ * ‖f a_1‖₊)
Tactic: simp_rw [← coe_nnnorm, ← NNReal.coe_mul, NNReal.coe_le_coe, Pi.nnnorm_def,
      NNReal.mul_finset_sup]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
c : ℝ
⊢ ∃ (x : E), c < ‖x‖
have rcases : ∀ (x : E) (hx : x ≠ 0), ∃ (x : E), c < ‖x‖
Tactic: rcases exists_ne (0 : E) with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
⊢ ∃ (x : E), c < ‖x‖
have rcases : ∀ (r : 𝕜) (hr : c / ‖x‖ < ‖r‖), ∃ (x : E), c < ‖x‖
Tactic: rcases NormedField.exists_lt_norm 𝕜 (c / ‖x‖) with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ ∃ (x : E), c < ‖x‖
have h : c < ‖r • x‖
Tactic: use r • x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ c < ‖r • x‖
have h : 0 < ‖x‖
Tactic: rwa [norm_smul, ← div_lt_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
⊢ (cobounded E).NeBot
have rw : ¬Bornology.IsBounded.{u_3} (α := E) univ
Tactic: rw [neBot_iff, Ne, cobounded_eq_bot_iff, ← isBounded_univ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
⊢ NoncompactSpace E
have pos : ∀ (H : ∃ (c : 𝕜), c ≠ 0 ∧ ‖c‖ ≠ 1), NoncompactSpace E
Tactic: by_cases! H : ∃ c : 𝕜, c ≠ 0 ∧ ‖c‖ ≠ 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
pos : ∀ (H : ∃ (c : 𝕜), c ≠ 0 ∧ ‖c‖ ≠ 1), NoncompactSpace E
⊢ NoncompactSpace E
have neg : ∀ (H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1), NoncompactSpace E
Tactic: by_cases! H : ∃ c : 𝕜, c ≠ 0 ∧ ‖c‖ ≠ 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
⊢ NoncompactSpace E
have neg : ∀ (x : E) (hx : x ≠ 0), NoncompactSpace E
Tactic: rcases exists_ne (0 : E) with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
x : E
hx : x ≠ 0
⊢ NoncompactSpace E
have neg : IsClosedEmbedding.{0, u_3} (Y := E) fun (x_1 : ℕ) ↦
  HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) x_1 : 𝕜) x
Tactic: suffices IsClosedEmbedding (Infinite.natEmbedding 𝕜 · • x) from this.noncompactSpace
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
x : E
hx : x ≠ 0
⊢ IsClosedEmbedding.{0, u_3} (Y := E) fun (x_1 : ℕ) ↦
    HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) x_1 : 𝕜) x
have neg : ∀ (k n : ℕ) (hne : k ≠ n),
  (fun (x_1 y : ℕ) ↦
      ‖x‖ ≤
        dist (HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) x_1 : 𝕜) x)
          (HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) y : 𝕜) x))
    k n
Tactic: refine isClosedEmbedding_of_pairwise_le_dist (norm_pos_iff.2 hx) fun k n hne ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (fun (x_1 y : ℕ) ↦
      ‖x‖ ≤
        dist (HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) x_1 : 𝕜) x)
          (HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) y : 𝕜) x))
    k n
have neg : ‖x‖ ≤
  ‖HSub.hSub (α := 𝕜) (β := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) k : 𝕜)
        ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) n : 𝕜)‖ *
    ‖x‖
Tactic: simp only [dist_eq_norm, ← sub_smul, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ ‖x‖ ≤
    ‖HSub.hSub (α := 𝕜) (β := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) k : 𝕜)
          ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) n : 𝕜)‖ *
      ‖x‖
have neg : HSub.hSub (α := 𝕜) (β := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) k : 𝕜)
    ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) n : 𝕜) ≠
  0
Tactic: rw [H, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ HSub.hSub (α := 𝕜) (β := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) k : 𝕜)
      ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) n : 𝕜) ≠
    0
have neg : Ne (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) k : 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) n : 𝕜)
Tactic: rwa [sub_ne_zero, (Embedding.injective _).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ norm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') = ‖x‖ * norm.{u_2} (E := 𝕜') 1
have rw : ‖HSMul.hSMul (β := 𝕜') x 1‖ = ‖x‖ * norm.{u_2} (E := 𝕜') 1
Tactic: rw [Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x : 𝕜
⊢ norm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') = ‖x‖
have rw : ‖x‖ * norm.{u_2} (E := 𝕜') 1 = ‖x‖
Tactic: rw [norm_algebraMap, norm_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x : 𝕜
rw : ‖x‖ * norm.{u_2} (E := 𝕜') 1 = ‖x‖
⊢ norm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') = ‖x‖
have rw₁ : ‖x‖ * 1 = ‖x‖
Tactic: rw [norm_algebraMap, norm_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x : 𝕜
rw : ‖x‖ * norm.{u_2} (E := 𝕜') 1 = ‖x‖
rw₁ : ‖x‖ * 1 = ‖x‖
⊢ norm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') = ‖x‖
have rw₂ : ‖x‖ = ‖x‖
Tactic: rw [norm_algebraMap, norm_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_6
𝕜' : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
c : Set 𝕜'
hc : c ∈ cobounded 𝕜'
⊢ Membership.mem (γ := Filter 𝕜') (map (⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') (cobounded 𝕜)) c
have rw : (⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c ∈ cobounded 𝕜
Tactic: rw [mem_map]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_6
𝕜' : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
c : Set 𝕜'
hc : c ∈ cobounded 𝕜'
⊢ (⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c ∈ cobounded 𝕜
have rw : ∀ (hc : ∃ (C : ℝ), ∀ x ∈ cᶜ, ‖x‖ ≤ C),
  ∃ (C : ℝ), ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ((⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c)ᶜ x → ‖x‖ ≤ C
Tactic: rw [← isCobounded_def, ← isBounded_compl_iff, isBounded_iff_forall_norm_le] at hc ⊢
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_6
𝕜' : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
c : Set 𝕜'
hc : ∃ (C : ℝ), ∀ x ∈ cᶜ, ‖x‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ((⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c)ᶜ x → ‖x‖ ≤ C
have obtain : ∀ (s : ℝ) (hs : ∀ x ∈ cᶜ, ‖x‖ ≤ s),
  ∃ (C : ℝ), ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ((⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜') ⁻¹' c)ᶜ x → ‖x‖ ≤ C
Tactic: obtain ⟨s, hs⟩ := hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
⊢ Isometry.{u_1, u_2} (α := 𝕜) (β := 𝕜') (⇑(algebraMap 𝕜 𝕜') : (a : 𝕜) → 𝕜')
have refine : ∀ (x y : 𝕜),
  dist.{u_2} (α := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜') = dist x y
Tactic: refine Isometry.of_dist_eq fun x y => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x y : 𝕜
⊢ dist.{u_2} (α := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜') = dist x y
have rw : ‖HSub.hSub (α := 𝕜') (β := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜')‖ =
  dist x y
Tactic: rw [dist_eq_norm, dist_eq_norm, ← map_sub, norm_algebraMap']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x y : 𝕜
rw :
  ‖HSub.hSub (α := 𝕜') (β := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜')‖ =
    dist x y
⊢ dist.{u_2} (α := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜') = dist x y
have rw₁ : ‖HSub.hSub (α := 𝕜') (β := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜')‖ =
  ‖x - y‖
Tactic: rw [dist_eq_norm, dist_eq_norm, ← map_sub, norm_algebraMap']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x y : 𝕜
rw :
  ‖HSub.hSub (α := 𝕜') (β := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜')‖ =
    dist x y
rw₁ :
  ‖HSub.hSub (α := 𝕜') (β := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜')‖ =
    ‖x - y‖
⊢ dist.{u_2} (α := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜') = dist x y
have rw₂ : norm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') (x - y) : 𝕜') = ‖x - y‖
Tactic: rw [dist_eq_norm, dist_eq_norm, ← map_sub, norm_algebraMap']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : NormOneClass 𝕜'
x y : 𝕜
rw :
  ‖HSub.hSub (α := 𝕜') (β := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜')‖ =
    dist x y
rw₁ :
  ‖HSub.hSub (α := 𝕜') (β := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜')‖ =
    ‖x - y‖
rw₂ : norm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') (x - y) : 𝕜') = ‖x - y‖
⊢ dist.{u_2} (α := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') x : 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') y : 𝕜') = dist x y
have rw₃ : ‖x - y‖ = ‖x - y‖
Tactic: rw [dist_eq_norm, dist_eq_norm, ← map_sub, norm_algebraMap']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜_1
inst_1 : SeminormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜_1 𝕜'
𝕜 : Type u_6
inst_3 : NormedDivisionRing 𝕜
inst_4 : CharZero 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
q : ℚ
x : 𝕜
⊢ ‖q • x‖ ≤ ‖q‖ * ‖x‖
have rw : ‖HSMul.hSMul (β := ℝ) q 1 • x‖ ≤ ‖q‖ * ‖x‖
Tactic: rw [← smul_one_smul ℝ q x, Rat.smul_one_eq_cast, norm_smul, Rat.norm_cast_real]