awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ
ε0 : 0 < ε
hε : Subset.{u_4} (α := Set E) (Set.preimage.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (ball 0 ε)) (ball 0 1)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)
have hε₁ : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < ε → ‖x‖ < 1
Tactic: simp only [Set.subset_def, Set.mem_preimage, mem_ball_zero_iff] at hε
Cleared hypotheses: hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ
ε0 : 0 < ε
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < ε → ‖x‖ < 1
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)
have lift : ∀ (ε : ℝ≥0) (ε0 : 0 < (↑ε : ℝ)) (hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1),
  ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)
Tactic: lift ε to ℝ≥0 using ε0.le
Cleared hypotheses: ε, ε0, hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)
have rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)
Tactic: rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)
have refine : ∀ (x : E), ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: refine ⟨ε⁻¹ * ‖c‖₊, AddMonoidHomClass.antilipschitz_of_bound f fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have pos : ∀ (hx : Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)),
  ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: by_cases hx : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
pos :
  ∀ (hx : Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)),
    ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have neg : ∀ (hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)),
  ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: by_cases hx : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have hf₁ : LE.le.{u_4} (α := Filter E)
  (Filter.comap.{u_4, u_5} (β := F) ((⇑f : (a : E) → F) : (a : E) → F) (𝓝 ((f : (a : E) → F) x) : Filter F)) (𝓝 0)
Tactic: rw [← hx] at hf
Cleared hypotheses: hf, hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hf :
  LE.le.{u_4} (α := Filter E)
    (Filter.comap.{u_4, u_5} (β := F) ((⇑f : (a : E) → F) : (a : E) → F) (𝓝 ((f : (a : E) → F) x) : Filter F)) (𝓝 0)
hx : Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have pos : ∀
  (hf :
    LE.le.{u_4} (α := Filter E)
      (Filter.comap.{u_4, u_5} (β := F) ((⇑f : (a : E) → F) : (a : E) → F) (𝓝 ((f : (a : E) → F) 0) : Filter F)) (𝓝 0))
  (hx : Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) 0 : F) (0 : F)),
  norm.{u_4} (E := E) 0 ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) 0 : F)
Tactic: obtain rfl : x = 0 := Specializes.eq (specializes_iff_pure.2 <|
      ((Filter.tendsto_pure_pure _ _).mono_right (pure_le_nhds _)).le_comap.trans hf)
Cleared hypotheses: x, hf, hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have hc₀ : c ≠ 0
Tactic: have hc₀ : c ≠ 0 := norm_pos_iff.1 (one_pos.trans hc)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have neg : ∀ (hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)) (x : E)
  (hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)) (hc₀ : c ≠ 0),
  ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: rw [← h.1] at hc
Cleared hypotheses: hc, x, hx, hc₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have neg : ∀ (n : ℤ)
  (hlt :
    ‖HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂) n) ((f : (a : E) → F) x : F)‖ < (↑ε : ℝ))
  (hle :
    ‖HPow.hPow (α := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂) n‖⁻¹ ≤
      (↑ε : ℝ)⁻¹ * norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)),
  ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: rcases rescale_to_shell_zpow hc ε0 hx with ⟨n, -, hlt, -, hle⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
n : ℤ
hlt : ‖HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂) n) ((f : (a : E) → F) x : F)‖ < (↑ε : ℝ)
hle :
  ‖HPow.hPow (α := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂) n‖⁻¹ ≤
    (↑ε : ℝ)⁻¹ * norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have hlt₁ : norm.{u_5} (E := F) ((f : (a : E) → F) (c ^ n • x) : F) < (↑ε : ℝ)
Tactic: simp only [← map_zpow₀, h.1, ← map_smulₛₗ] at hlt hle
Cleared hypotheses: hlt, hle
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
n : ℤ
hlt : ‖HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂) n) ((f : (a : E) → F) x : F)‖ < (↑ε : ℝ)
hle :
  ‖HPow.hPow (α := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂) n‖⁻¹ ≤
    (↑ε : ℝ)⁻¹ * norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
hlt₁ : norm.{u_5} (E := F) ((f : (a : E) → F) (c ^ n • x) : F) < (↑ε : ℝ)
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have hle₁ : ‖c ^ n‖⁻¹ ≤ (↑ε : ℝ)⁻¹ * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: simp only [← map_zpow₀, h.1, ← map_smulₛₗ] at hlt hle
Cleared hypotheses: hlt, hle
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
n : ℤ
hlt : norm.{u_5} (E := F) ((f : (a : E) → F) (c ^ n • x) : F) < (↑ε : ℝ)
hle : ‖c ^ n‖⁻¹ ≤ (↑ε : ℝ)⁻¹ * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖
have rwa : ‖x‖ = ‖(c ^ n)⁻¹‖ * ‖c ^ n • x‖
Tactic: rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
n : ℤ
hlt : norm.{u_5} (E := F) ((f : (a : E) → F) (c ^ n • x) : F) < (↑ε : ℝ)
hle : ‖c ^ n‖⁻¹ ≤ (↑ε : ℝ)⁻¹ * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
rwa : ‖x‖ = ‖(c ^ n)⁻¹‖ * ‖c ^ n • x‖
⊢ ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖
have rwa₁ : ‖x‖ = ‖(c ^ n)⁻¹ • c ^ n • x‖
Tactic: rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
n : ℤ
hlt : norm.{u_5} (E := F) ((f : (a : E) → F) (c ^ n • x) : F) < (↑ε : ℝ)
hle : ‖c ^ n‖⁻¹ ≤ (↑ε : ℝ)⁻¹ * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
rwa : ‖x‖ = ‖(c ^ n)⁻¹‖ * ‖c ^ n • x‖
rwa₁ : ‖x‖ = ‖(c ^ n)⁻¹ • c ^ n • x‖
⊢ ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖
have rwa₂ : ‖x‖ = ‖x‖
Tactic: rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
n : ℤ
hlt : norm.{u_5} (E := F) ((f : (a : E) → F) (c ^ n • x) : F) < (↑ε : ℝ)
hle : ‖c ^ n‖⁻¹ ≤ (↑ε : ℝ)⁻¹ * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ‖c ^ n‖⁻¹ * ‖c ^ n • x‖ ≤ ‖c ^ n‖⁻¹ * 1
have hbc : ‖c ^ n • x‖ ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
n : ℤ
hlt : norm.{u_5} (E := F) ((f : (a : E) → F) (c ^ n • x) : F) < (↑ε : ℝ)
hle : ‖c ^ n‖⁻¹ ≤ (↑ε : ℝ)⁻¹ * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ‖c ^ n‖⁻¹ * 1 ≤ (↑ε⁻¹ : ℝ) * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have rwa : ‖c ^ n‖⁻¹ ≤ (↑ε⁻¹ : ℝ) * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: rwa [mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
n : ℤ
hlt : norm.{u_5} (E := F) ((f : (a : E) → F) (c ^ n • x) : F) < (↑ε : ℝ)
hle : ‖c ^ n‖⁻¹ ≤ (↑ε : ℝ)⁻¹ * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have n₁ : ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖
Tactic: calc
    ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖ := by
      rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]
    _ ≤ ‖c ^ n‖⁻¹ * 1 := by gcongr; exact (hε _ hlt).le
    _ ≤ ε⁻¹ * ‖c‖ * ‖f x‖ := by rwa [mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
n : ℤ
hlt : norm.{u_5} (E := F) ((f : (a : E) → F) (c ^ n • x) : F) < (↑ε : ℝ)
hle : ‖c ^ n‖⁻¹ ≤ (↑ε : ℝ)⁻¹ * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
n₁ : ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have n₂ : ‖c ^ n‖⁻¹ * ‖c ^ n • x‖ ≤ ‖c ^ n‖⁻¹ * 1
Tactic: calc
    ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖ := by
      rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]
    _ ≤ ‖c ^ n‖⁻¹ * 1 := by gcongr; exact (hε _ hlt).le
    _ ≤ ε⁻¹ * ‖c‖ * ‖f x‖ := by rwa [mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
c : 𝕜
hc : 1 < norm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) c : 𝕜₂)
x : E
hx : ¬Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)
hc₀ : c ≠ 0
n : ℤ
hlt : norm.{u_5} (E := F) ((f : (a : E) → F) (c ^ n • x) : F) < (↑ε : ℝ)
hle : ‖c ^ n‖⁻¹ ≤ (↑ε : ℝ)⁻¹ * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
n₁ : ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖
n₂ : ‖c ^ n‖⁻¹ * ‖c ^ n • x‖ ≤ ‖c ^ n‖⁻¹ * 1
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have n₃ : ‖c ^ n‖⁻¹ * 1 ≤ (↑ε⁻¹ : ℝ) * ‖c‖ * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: calc
    ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖ := by
      rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]
    _ ≤ ‖c ^ n‖⁻¹ * 1 := by gcongr; exact (hε _ hlt).le
    _ ≤ ε⁻¹ * ‖c‖ * ‖f x‖ := by rwa [mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst_6 : RingHomIsometric σ₁₂
hn : ‖f‖ = 0
x : E
⊢ ‖f‖ * ‖x‖ = 0
have rw : 0 * ‖x‖ = 0
Tactic: rw [hn, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst_6 : RingHomIsometric σ₁₂
hn : ‖f‖ = 0
x : E
rw : 0 * ‖x‖ = 0
⊢ ‖f‖ * ‖x‖ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [hn, zero_mul]