awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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)

Tactic:
⟨ε⁻¹ * ‖c‖₊, AddMonoidHomClass.antilipschitz_of_bound f fun x => ?_⟩

Premises used: HMul.hMul, NNNorm.nnnorm, AddMonoidHomClass.antilipschitz_of_bound, Inv.inv, Exists.intro
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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‖
refine : ∀ (x : E), ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
refine ⟨ε⁻¹ * ‖c‖₊, AddMonoidHomClass.antilipschitz_of_bound f fun x => ?_⟩
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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)
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)
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
by_cases hx : f x = 0

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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)
⊢ 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
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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)
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)
⊢ Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F) (0 : F)

Tactic:
rw [← hx] at hf
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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 = 0

Tactic:
Specializes.eq (specializes_iff_pure.2 <|
      ((Filter.tendsto_pure_pure _ _).mono_right (pure_le_nhds _)).le_comap.trans hf)

Premises used: Iff.mpr, Filter.Tendsto.le_comap, pure_le_nhds, Filter.tendsto_pure_pure, Specializes.eq, specializes_iff_pure, Filter.Tendsto.mono_right, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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)
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)
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : 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)

Premises used: Iff.mpr, Filter.Tendsto.le_comap, pure_le_nhds, Filter.tendsto_pure_pure, Specializes.eq, specializes_iff_pure, Filter.Tendsto.mono_right, LE.le.trans, rfl
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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‖
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:
norm_zero.trans_le (mul_nonneg (NNReal.coe_nonneg _) (norm_nonneg _))

Premises used: mul_nonneg, norm_zero, Eq.trans_le, NNReal.coe_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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‖
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:
exact norm_zero.trans_le (mul_nonneg (NNReal.coe_nonneg _) (norm_nonneg _))

Premises used: mul_nonneg, norm_zero, Eq.trans_le, NNReal.coe_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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)
⊢ c ≠ 0

Tactic:
have hc₀ : c ≠ 0 := norm_pos_iff.1 (one_pos.trans hc)
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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
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)
⊢ ‖x‖ ≤ (↑(ε⁻¹ * ‖c‖₊) : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
rw [← h.1] at hc

Premises used: RingHomIsometric.norm_map
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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
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)
⊢ ‖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⟩

Premises used: rescale_to_shell_zpow
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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)
⊢ 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

Premises used: MulActionSemiHomClass.map_smulₛₗ, RingHomIsometric.norm_map, map_zpow₀
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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) < (↑ε : ℝ)
⊢ ‖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

Premises used: MulActionSemiHomClass.map_smulₛₗ, RingHomIsometric.norm_map, map_zpow₀
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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‖
rwa₂ : ‖x‖ = ‖x‖
rwa₃ : c ≠ 0
rwa₄ : ‖x‖ = ‖x‖
rwa₅ rwa₆ rwa₇ : c ≠ 0
⊢ ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖

Tactic:
rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]

Premises used: inv_smul_smul₀, norm_smul, norm_inv, zpow_ne_zero
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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)
hbc : ‖c ^ n • x‖ ≤ 1
⊢ ‖c ^ n‖⁻¹ * ‖c ^ n • x‖ ≤ ‖c ^ n‖⁻¹ * 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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 • x‖ ≤ 1

Tactic:
(hε _ hlt).le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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 • x‖ ≤ 1

Tactic:
exact (hε _ hlt).le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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 rwa₁ rwa₂ rwa₃ : ‖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)

Tactic:
rwa [mul_one]

Premises used: mul_one
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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
n₃ : ‖c ^ n‖⁻¹ * 1 ≤ (↑ε⁻¹ : ℝ) * ‖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:
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]

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ‖f‖ * ‖x‖ = 0

Tactic:
rw [hn, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
⊢ Norm.norm (E := E →SL[σ₁₂] F) 0 = 0

Tactic:
opNorm_zero

Premises used: ContinuousLinearMap.opNorm_zero
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
⊢ Norm.norm (E := E →SL[σ₁₂] F) 0 = 0

Tactic:
exact opNorm_zero

Premises used: ContinuousLinearMap.opNorm_zero
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
f : E →L[𝕜] Fₗ
hf : IsEmbedding.{u_4, u_6} (X := E) (Y := Fₗ) (⇑f : (a : E) → Fₗ)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_6} (α := E) (β := Fₗ) K (⇑f : (a : E) → Fₗ)

Tactic:
f.toLinearMap.antilipschitz_of_comap_nhds_le <| map_zero f ▸ (hf.nhds_eq_comap 0).ge

Premises used: Topology.IsInducing.nhds_eq_comap, Eq.ge, Eq.rec, map_zero, ContinuousLinearMap.toLinearMap, Topology.IsEmbedding.toIsInducing, LinearMap.antilipschitz_of_comap_nhds_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
inl : Subsingleton F' → ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖
inr : Nontrivial F' → ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖
⊢ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖

Tactic:
cases subsingleton_or_nontrivial F'

Premises used: subsingleton_or_nontrivial