awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 𝕜
rw : ‖HSMul.hSMul (β := ℝ) q 1 • x‖ ≤ ‖q‖ * ‖x‖
⊢ ‖q • x‖ ≤ ‖q‖ * ‖x‖
have rw₁ : ‖HSMul.hSMul (α := ℝ) (↑q : ℝ) x‖ ≤ ‖q‖ * ‖x‖
Tactic: rw [← smul_one_smul ℝ q x, Rat.smul_one_eq_cast, norm_smul, Rat.norm_cast_real]
-- 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 : 𝕜
rw : ‖HSMul.hSMul (β := ℝ) q 1 • x‖ ≤ ‖q‖ * ‖x‖
rw₁ : ‖HSMul.hSMul (α := ℝ) (↑q : ℝ) x‖ ≤ ‖q‖ * ‖x‖
⊢ ‖q • x‖ ≤ ‖q‖ * ‖x‖
have rw₂ : norm (E := ℝ) (↑q : ℝ) * ‖x‖ ≤ ‖q‖ * ‖x‖
Tactic: rw [← smul_one_smul ℝ q x, Rat.smul_one_eq_cast, norm_smul, Rat.norm_cast_real]
-- 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 : 𝕜
rw : ‖HSMul.hSMul (β := ℝ) q 1 • x‖ ≤ ‖q‖ * ‖x‖
rw₁ : ‖HSMul.hSMul (α := ℝ) (↑q : ℝ) x‖ ≤ ‖q‖ * ‖x‖
rw₂ : norm (E := ℝ) (↑q : ℝ) * ‖x‖ ≤ ‖q‖ * ‖x‖
⊢ ‖q • x‖ ≤ ‖q‖ * ‖x‖
have rw₃ : ‖q‖ * ‖x‖ ≤ ‖q‖ * ‖x‖
Tactic: rw [← smul_one_smul ℝ q x, Rat.smul_one_eq_cast, norm_smul, Rat.norm_cast_real]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : SeminormedAddCommGroup E
inst_4 : NormedSpace 𝕜' E
c : 𝕜
x : E
⊢ norm.{u_2} (E := 𝕜') ((algebraMap 𝕜 𝕜' : (a : 𝕜) → 𝕜') c : 𝕜') * ‖x‖ = ‖c‖ * ‖x‖
have rw : ‖c‖ * ‖x‖ = ‖c‖ * ‖x‖
Tactic: rw [norm_algebraMap']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_6
inst_3 : SeminormedAddCommGroup E
h : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
inst_5 : IsScalarTower 𝕜 𝕜' E
⊢ restrictScalars 𝕜 𝕜' E = h
have smul : ∀ (x : 𝕜) (x_1 : E), SMul.smul x x_1 = SMul.smul x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
⊢ ‖-x + x‖ = 0
have simp : norm.{u_7} (E := E) 0 = 0
Tactic: simp only [add_comm, ← sub_eq_add_neg, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (hypothesis)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
⊢ norm.{u_7} (E := E) 0 = 0
have this : 0 = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (β := E) 0 0
Tactic: have : (0 : E) = (0 : 𝕜) • (0 : E) := by simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
this : 0 = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (β := E) 0 0
⊢ norm.{u_7} (E := E) 0 = 0
have rw : norm.{u_6} (E := 𝕜) 0 * norm.{u_7} (E := E) 0 = 0
Tactic: rw [this, core.norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
⊢ -y + x = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (-1) (-x + y)
have simp : -y + x = x + -y
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (hypothesis)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
⊢ ‖-x + y‖ = ‖-y + x‖
have this : -y + x = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (-1) (-x + y)
Tactic: have : -y + x = (-1 : 𝕜) • (-x + y) := by simp; abel
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
this : -y + x = HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (-1) (-x + y)
⊢ ‖-x + y‖ = ‖-y + x‖
have rw : ‖-x + y‖ = norm.{u_6} (E := 𝕜) (-1) * ‖-x + y‖
Tactic: rw [this, core.norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (hypothesis)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
⊢ ‖-x + z‖ ≤ ‖-x + y‖ + ‖-y + z‖
have this : -x + z = -x + y + (-y + z)
Tactic: have : -x + z = (-x + y) + (-y + z) := by abel
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Norm E
inst_3 : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
this : -x + z = -x + y + (-y + z)
⊢ ‖-x + z‖ ≤ ‖-x + y‖ + ‖-y + z‖
have rw : ‖-x + y + (-y + z)‖ ≤ ‖-x + y‖ + ‖-y + z‖
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
core : NormedSpace.Core 𝕜 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ x = y
have rw : ‖-x + y‖ = 0
Tactic: rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ x = y
have rw : ‖-x + y‖ = 0
Tactic: rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
T : TopologicalSpace E
core : NormedSpace.Core 𝕜 E
H : T = UniformSpace.toTopologicalSpace
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ x = y
have rw : ‖-x + y‖ = 0
Tactic: rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Norm E
U : UniformSpace E
B : Bornology E
core : NormedSpace.Core 𝕜 E
HU : 𝓤 E = 𝓤 E
HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ x = y
have rw : ‖-x + y‖ = 0
Tactic: rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜_2 : Type u_6
E_2 : Type u_7
inst : NormedField 𝕜_2
inst_1 : AddCommGroup E_2
inst_2 : Module 𝕜_2 E_2
inst_3 : Norm E_2
𝕜 : Type u_8
E : Type u_9
inst_4 : NormedField 𝕜
inst_5 : SeminormedAddCommGroup E
inst_6 : Module 𝕜 E
core : Core 𝕜 E
r : 𝕜
x : E
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
have rw : ‖r‖ * ‖x‖ ≤ ‖r‖ * ‖x‖
Tactic: rw [core.norm_smul r x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : G) → H)
have obtain : ∀ (δ : ℝ) (hδ : δ > 0) (hUε : ball 0 δ ⊆ s),
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : G) → H)
Tactic: obtain ⟨δ, hδ, hUε⟩ := Metric.mem_nhds_iff.mp hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : G) → H)
have obtain : ∀ (C : ℝ) (hC : Subset.{u_7} (α := Set H) (image.{u_6, u_7} (α := G) (⇑f : (a : G) → H) (ball 0 δ)) (ball 0 C)),
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : G) → H)
Tactic: obtain ⟨C, hC⟩ := (isBounded_iff_subset_ball 0).1 (hbounded.subset <| image_mono hUε)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C : ℝ
hC : Subset.{u_7} (α := Set H) (image.{u_6, u_7} (α := G) (⇑f : (a : G) → H) (ball 0 δ)) (ball 0 C)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : G) → H)
have refine : ∀ (ε : ℝ) (hε : 0 < ε),
  ∃ δ > 0, ∀ ⦃x : G⦄, dist x 0 < δ → dist.{u_7} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) 0 : H) < ε
Tactic: refine continuous_of_continuousAt_zero _ (continuousAt_iff.2 fun ε (hε : _ < _) => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C : ℝ
hC : Subset.{u_7} (α := Set H) (image.{u_6, u_7} (α := G) (⇑f : (a : G) → H) (ball 0 δ)) (ball 0 C)
ε : ℝ
hε : 0 < ε
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, dist x 0 < δ → dist.{u_7} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) 0 : H) < ε
have simp : ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
Tactic: simp only [dist_zero_right, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (hypothesis)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C : ℝ
hC : Subset.{u_7} (α := Set H) (image.{u_6, u_7} (α := G) (⇑f : (a : G) → H) (ball 0 δ)) (ball 0 C)
ε : ℝ
hε : 0 < ε
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
have hC₁ : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
Tactic: simp only [subset_def, mem_image, mem_ball, dist_zero_right, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂] at hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (hypothesis)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
have hC₀ : 0 < C
Tactic: have hC₀ : 0 < C := (norm_nonneg _).trans_lt <| hC 0 (by simpa)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
have obtain : ∀ (n : ℕ) (hn : C / ε < (↑n : ℝ)), ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
Tactic: obtain ⟨n, hn⟩ := exists_nat_gt (C / ε)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (hypothesis)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
have hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have hnpos : 0 < (n : ℝ) := (div_pos hC₀ hε).trans hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (hypothesis)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
have hn₀ : n ≠ 0
Tactic: have hn₀ : n ≠ 0 := by rintro rfl; simp at hnpos
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
have refine : ∀ {x : G} (hxδ : ‖x‖ < δ / (↑n : ℝ)), norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
Tactic: refine ⟨δ / n, div_pos hδ hnpos, fun {x} hxδ => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
⊢ norm (E := ℝ) (↑n : ℝ)⁻¹ * norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < norm (E := ℝ) (↑n : ℝ)⁻¹ * C
have ha : 0 < norm (E := ℝ) (↑n : ℝ)⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
ha : 0 < norm (E := ℝ) (↑n : ℝ)⁻¹
⊢ norm (E := ℝ) (↑n : ℝ)⁻¹ * norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < norm (E := ℝ) (↑n : ℝ)⁻¹ * C
have hbc : norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < C
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
⊢ norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < C
have hbc : (↑n : ℝ) * ‖x‖ < δ
Tactic: refine hC _ <| norm_nsmul_le.trans_lt ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
ha : 0 < C
⊢ (↑n : ℝ)⁻¹ * C < (C / ε)⁻¹ * C
have hbc : 0 < C / ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
⊢ norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
have _ : norm.{u_7} (E := H) ((f : (a : G) → H) x : H) =
  ‖HSMul.hSMul (α := ℝ) (β := H) (↑n : ℝ)⁻¹ ((f : (a : G) → H) (n • x) : H)‖
Tactic: calc
    ‖f x‖
    _ = ‖(n : ℝ)⁻¹ • f (n • x)‖ := by simp [← Nat.cast_smul_eq_nsmul ℝ, hn₀]
    _ ≤ ‖(n : ℝ)⁻¹‖ * ‖f (n • x)‖ := norm_smul_le ..
    _ < ‖(n : ℝ)⁻¹‖ * C := by
      gcongr
      · simpa [pos_iff_ne_zero]
      · refine hC _ <| norm_nsmul_le.trans_lt ?_
        simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ
    _ = (n : ℝ)⁻¹ * C := by simp
    _ < (C / ε : ℝ)⁻¹ * C := by gcongr
    _ = ε := by simp [hC₀.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
_ :
  norm.{u_7} (E := H) ((f : (a : G) → H) x : H) =
    ‖HSMul.hSMul (α := ℝ) (β := H) (↑n : ℝ)⁻¹ ((f : (a : G) → H) (n • x) : H)‖
⊢ norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
have _₁ : norm (E := ℝ) (↑n : ℝ)⁻¹ * norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < norm (E := ℝ) (↑n : ℝ)⁻¹ * C
Tactic: calc
    ‖f x‖
    _ = ‖(n : ℝ)⁻¹ • f (n • x)‖ := by simp [← Nat.cast_smul_eq_nsmul ℝ, hn₀]
    _ ≤ ‖(n : ℝ)⁻¹‖ * ‖f (n • x)‖ := norm_smul_le ..
    _ < ‖(n : ℝ)⁻¹‖ * C := by
      gcongr
      · simpa [pos_iff_ne_zero]
      · refine hC _ <| norm_nsmul_le.trans_lt ?_
        simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ
    _ = (n : ℝ)⁻¹ * C := by simp
    _ < (C / ε : ℝ)⁻¹ * C := by gcongr
    _ = ε := by simp [hC₀.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
_ :
  norm.{u_7} (E := H) ((f : (a : G) → H) x : H) =
    ‖HSMul.hSMul (α := ℝ) (β := H) (↑n : ℝ)⁻¹ ((f : (a : G) → H) (n • x) : H)‖
_₁ : norm (E := ℝ) (↑n : ℝ)⁻¹ * norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < norm (E := ℝ) (↑n : ℝ)⁻¹ * C
⊢ norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
have _₂ : norm (E := ℝ) (↑n : ℝ)⁻¹ * C = (↑n : ℝ)⁻¹ * C
Tactic: calc
    ‖f x‖
    _ = ‖(n : ℝ)⁻¹ • f (n • x)‖ := by simp [← Nat.cast_smul_eq_nsmul ℝ, hn₀]
    _ ≤ ‖(n : ℝ)⁻¹‖ * ‖f (n • x)‖ := norm_smul_le ..
    _ < ‖(n : ℝ)⁻¹‖ * C := by
      gcongr
      · simpa [pos_iff_ne_zero]
      · refine hC _ <| norm_nsmul_le.trans_lt ?_
        simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ
    _ = (n : ℝ)⁻¹ * C := by simp
    _ < (C / ε : ℝ)⁻¹ * C := by gcongr
    _ = ε := by simp [hC₀.ne']