awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x y : E
simp_rw : ‖HSub.hSub (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)‖ ≤ ‖f‖ * ‖x - y‖
⊢ dist.{u_5} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F) ≤ ‖f‖ * dist x y
have simp_rw₁ : Norm.norm.{u_5} (E := F) ((f : (a : E) → F) (x - y) : F) ≤ ‖f‖ * ‖x - y‖
Tactic: simp_rw [dist_eq_norm, ← map_sub, f.le_opNorm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
a b : ℝ
hf : ‖f‖ ≤ a
hx : ‖x‖ ≤ b
⊢ ‖f‖ * ‖x‖ ≤ a * b
have b0 : 0 ≤ a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup Fₗ
inst_3 : SeminormedAddCommGroup G
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NontriviallyNormedField 𝕜₂
inst_6 : NontriviallyNormedField 𝕜₃
inst_7 : NormedSpace 𝕜 E
inst_8 : NormedSpace 𝕜₂ F
inst_9 : NormedSpace 𝕜 Fₗ
inst_10 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_12 : FunLike 𝓕 E F
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
⊢ comap (⇑ℓ : (a : E) → F) (cobounded F) ≤ cobounded E
have rw : ∀ ⦃s : Set E⦄, Bornology.IsBounded s → Bornology.IsBounded.{u_5} (α := F) ((⇑ℓ : (a : E) → F) '' s)
Tactic: rw [Bornology.comap_cobounded_le_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup Fₗ
inst_3 : SeminormedAddCommGroup G
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NontriviallyNormedField 𝕜₂
inst_6 : NontriviallyNormedField 𝕜₃
inst_7 : NormedSpace 𝕜 E
inst_8 : NormedSpace 𝕜₂ F
inst_9 : NormedSpace 𝕜 Fₗ
inst_10 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_12 : FunLike 𝓕 E F
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
⊢ Bornology.IsBounded.{u_5} (α := F) ((⇑ℓ : (a : E) → F) '' s)
have obtain : ∀ (M : ℝ) (hM : ∀ x ∈ s, ‖x‖ ≤ M), Bornology.IsBounded.{u_5} (α := F) ((⇑ℓ : (a : E) → F) '' s)
Tactic: obtain ⟨M, hM⟩ := hs.exists_norm_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup Fₗ
inst_3 : SeminormedAddCommGroup G
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NontriviallyNormedField 𝕜₂
inst_6 : NontriviallyNormedField 𝕜₃
inst_7 : NormedSpace 𝕜 E
inst_8 : NormedSpace 𝕜₂ F
inst_9 : NormedSpace 𝕜 Fₗ
inst_10 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_12 : FunLike 𝓕 E F
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
⊢ Bornology.IsBounded.{u_5} (α := F) ((⇑ℓ : (a : E) → F) '' s)
have rw : ∃ (C : ℝ), ∀ (x : F), Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) x → ‖x‖ ≤ C
Tactic: rw [isBounded_iff_forall_norm_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup Fₗ
inst_3 : SeminormedAddCommGroup G
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NontriviallyNormedField 𝕜₂
inst_6 : NontriviallyNormedField 𝕜₃
inst_7 : NormedSpace 𝕜 E
inst_8 : NormedSpace 𝕜₂ F
inst_9 : NormedSpace 𝕜 Fₗ
inst_10 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_12 : FunLike 𝓕 E F
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
⊢ ∃ (C : ℝ), ∀ (x : F), Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) x → ‖x‖ ≤ C
have h₁ : ∀ (x : F), Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) x → ‖x‖ ≤ ‖ℓ‖ * M
Tactic: use ‖ℓ‖ * M
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup Fₗ
inst_3 : SeminormedAddCommGroup G
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NontriviallyNormedField 𝕜₂
inst_6 : NontriviallyNormedField 𝕜₃
inst_7 : NormedSpace 𝕜 E
inst_8 : NormedSpace 𝕜₂ F
inst_9 : NormedSpace 𝕜 Fₗ
inst_10 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_12 : FunLike 𝓕 E F
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) y
⊢ ‖y‖ ≤ ‖ℓ‖ * M
have h₁ : ∀ (σ : E) (hσ : σ ∈ s ∧ (ℓ : (a : E) → F) σ = y), ‖y‖ ≤ ‖ℓ‖ * M
Tactic: obtain ⟨σ, hσ⟩ := (mem_image _ _ _).1 hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup Fₗ
inst_3 : SeminormedAddCommGroup G
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NontriviallyNormedField 𝕜₂
inst_6 : NontriviallyNormedField 𝕜₃
inst_7 : NormedSpace 𝕜 E
inst_8 : NormedSpace 𝕜₂ F
inst_9 : NormedSpace 𝕜 Fₗ
inst_10 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_12 : FunLike 𝓕 E F
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) y
σ : E
hσ : σ ∈ s ∧ (ℓ : (a : E) → F) σ = y
⊢ ‖y‖ ≤ Norm.norm.{u_5} (E := F) ((ℓ : (a : E) → F) σ : F)
have rw : ‖y‖ ≤ ‖y‖
Tactic: rw [hσ.2]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup Fₗ
inst_3 : SeminormedAddCommGroup G
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NontriviallyNormedField 𝕜₂
inst_6 : NontriviallyNormedField 𝕜₃
inst_7 : NormedSpace 𝕜 E
inst_8 : NormedSpace 𝕜₂ F
inst_9 : NormedSpace 𝕜 Fₗ
inst_10 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_12 : FunLike 𝓕 E F
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) y
σ : E
hσ : σ ∈ s ∧ (ℓ : (a : E) → F) σ = y
⊢ ‖y‖ ≤ ‖ℓ‖ * M
have calc : ‖y‖ ≤ Norm.norm.{u_5} (E := F) ((ℓ : (a : E) → F) σ : F)
Tactic: calc ‖y‖
      _ ≤ ‖ℓ σ‖ := by rw [hσ.2]
      _ ≤ ‖ℓ‖ * ‖σ‖ := ContinuousLinearMap.le_opNorm ℓ σ
      _ ≤ ‖ℓ‖ * M := mul_le_mul (by rfl) (hM σ hσ.1) (norm_nonneg σ) (opNorm_nonneg ℓ)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ (x : E), Membership.mem (γ := Set E) (ball 0 ε) x → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ‖f‖ ≤ C
have rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ‖f‖ ≤ C
Tactic: rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ (x : E), Membership.mem (γ := Set E) (ball 0 ε) x → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
c : 𝕜
hc : 1 < ‖c‖
⊢ ‖f‖ ≤ C
have refine : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ∀ (hx : ‖x‖ < ε), Membership.mem (γ := Set E) (ball 0 ε) x
Tactic: refine opNorm_le_of_shell ε_pos hC hc fun x _ hx => hf x ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ (x : E), Membership.mem (γ := Set E) (ball 0 ε) x → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
c : 𝕜
hc : 1 < ‖c‖
x : E
h : ε / ‖c‖ ≤ ‖x‖
hx : ‖x‖ < ε
⊢ Membership.mem (γ := Set E) (ball 0 ε) x
have rwa : Membership.mem (γ := Set E) {x : E | ‖x‖ < ε} x
Tactic: rwa [ball_zero_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ‖f‖ ≤ C
have pos : ∀ (h0 : c = 0), ‖f‖ ≤ C
Tactic: by_cases h0 : c = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
pos : ∀ (h0 : c = 0), ‖f‖ ≤ C
⊢ ‖f‖ ≤ C
have neg : ∀ (h0 : ¬c = 0), ‖f‖ ≤ C
Tactic: by_cases h0 : c = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : c = 0
⊢ ‖f‖ ≤ C
have pos : ∀ (x : E) (hx : Membership.mem (γ := Set E) (ball 0 ε) x), ε * ‖c‖ ≤ ‖x‖
Tactic: refine opNorm_le_of_ball ε_pos hC fun x hx => hf x ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : c = 0
pos : ∀ (x : E) (hx : Membership.mem (γ := Set E) (ball 0 ε) x), ε * ‖c‖ ≤ ‖x‖
⊢ ‖f‖ ≤ C
have pos₁ : ∀ (x : E) (hx : Membership.mem (γ := Set E) (ball 0 ε) x), ‖x‖ < ε
Tactic: refine opNorm_le_of_ball ε_pos hC fun x hx => hf x ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : c = 0
x : E
hx : Membership.mem (γ := Set E) (ball 0 ε) x
⊢ ‖x‖ < ε
have pos : ∀ (hx : Membership.mem (γ := Set E) {x : E | ‖x‖ < ε} x), ‖x‖ < ε
Tactic: rwa [ball_zero_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C
have hc₁ : 1 < ‖c⁻¹‖
Tactic: rw [← inv_inv c, norm_inv, inv_lt_one₀ (norm_pos_iff.2 <| inv_ne_zero h0)] at hc
Cleared hypotheses: hc, hf, h0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C
have neg : ∀ (x : E), ε / ‖c⁻¹‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
Tactic: refine opNorm_le_of_shell ε_pos hC hc ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ∀ (x : E), ε / ‖c⁻¹‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
have neg : ∀ (x : E), ε / ‖c‖⁻¹ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
Tactic: rwa [norm_inv, div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : ¬c = 0
neg : ∀ (x : E), ε / ‖c‖⁻¹ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ∀ (x : E), ε / ‖c⁻¹‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
have neg₁ : ∀ (x : E), ε * ‖c‖⁻¹⁻¹ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
Tactic: rwa [norm_inv, div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
⊢ ‖f‖ ≤ C
have refine : ∀ (x : E) (hx : ‖x‖ ≠ 0), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
Tactic: refine opNorm_le_bound' f hC fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ ≠ 0
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
have H₁ : ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖ = 1
Tactic: have H₁ : ‖algebraMap _ 𝕜 ‖x‖⁻¹ • x‖ = 1 := by simp [norm_smul, inv_mul_cancel₀ hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖ = 1
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
have H₂ : ‖x‖⁻¹ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
Tactic: have H₂ : ‖x‖⁻¹ * ‖f x‖ ≤ C := by simpa [norm_smul] using hf _ H₁
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖ = 1
H₂ : ‖x‖⁻¹ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
have rwa : ∀ (H₂ : Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) / ‖x‖ ≤ C), 0 < ‖x‖
Tactic: rwa [← div_eq_inv_mul, div_le_iff₀] at H₂
Cleared hypotheses: H₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : NontrivialTopology E
⊢ 1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
have let : ∀ (x : E) (hx : ‖x‖ ≠ 0), 1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
Tactic: let ⟨x, hx⟩ := exists_norm_ne_zero E
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : NontrivialTopology E
x : E
hx : ‖x‖ ≠ 0
⊢ 1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
have this : Norm.norm (E := E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) x : E) / ‖x‖ ≤
  Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
Tactic: have := (ContinuousLinearMap.id 𝕜 E).ratio_le_opNorm x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : NontrivialTopology E
x : E
hx : ‖x‖ ≠ 0
this :
  Norm.norm (E := E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) x : E) / ‖x‖ ≤
    Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
⊢ 1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
have rwa : ∀ (this : ‖x‖ / ‖x‖ ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)),
  1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
Tactic: rwa [id_apply, div_self hx] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : NontrivialTopology E
x : E
hx : ‖x‖ ≠ 0
this :
  Norm.norm (E := E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) x : E) / ‖x‖ ≤
    Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
rwa :
  ∀ (this : ‖x‖ / ‖x‖ ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)),
    1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
⊢ 1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
have rwa₁ : ∀ (this : 1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)),
  1 ≤ Norm.norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
Tactic: rwa [id_apply, div_self hx] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst_7 : DistribSMul 𝕜' F
inst_8 : SMulCommClass 𝕜₂ 𝕜' F
inst_9 : SeminormedAddCommGroup 𝕜'
inst_10 : IsBoundedSMul 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x : E
⊢ Norm.norm.{u_5} (E := F) ((c • f : (a : E) → F) x : F) ≤ ‖c‖ * ‖f‖ * ‖x‖
have grw : ‖HSMul.hSMul (β := F) c ((f : (a : E) → F) x : F)‖ ≤ ‖c‖ * ‖f‖ * ‖x‖
Tactic: grw [smul_apply, norm_smul_le, mul_assoc, le_opNorm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst_7 : DistribSMul 𝕜' F
inst_8 : SMulCommClass 𝕜₂ 𝕜' F
inst_9 : SeminormedAddCommGroup 𝕜'
inst_10 : IsBoundedSMul 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x : E
grw : ‖HSMul.hSMul (β := F) c ((f : (a : E) → F) x : F)‖ ≤ ‖c‖ * ‖f‖ * ‖x‖
⊢ Norm.norm.{u_5} (E := F) ((c • f : (a : E) → F) x : F) ≤ ‖c‖ * ‖f‖ * ‖x‖
have grw₁ : ‖c‖ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖c‖ * ‖f‖ * ‖x‖
Tactic: grw [smul_apply, norm_smul_le, mul_assoc, le_opNorm]