awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ι : Type u_9
inst_3 : Fintype ι
M : ι → Type u_10
inst_4 : (i : ι) → SeminormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_10} 𝕜 (M i)
C : ℝ
L : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_10} (RingHom.id 𝕜) E (M i)
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
x : E
⊢ norm (E := (i : ι) → M i) ((pi (φ := M) L : (a : E) → (i : ι) → M i) x : (i : ι) → M i) ≤ C * ‖x‖
have refine : ∀ (i : ι), norm.{u_10} (E := M i) ((pi (φ := M) L : (a : E) → (i : ι) → M i) x i : M i) ≤ C * ‖x‖
Tactic: refine (pi_norm_le_iff_of_nonneg (by positivity)).mpr (fun i ↦ ?_)
-- 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
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →ₛₗ[σ₁₂] F
C : ℝ
h : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
x : E
⊢ C * ‖x‖ ≤ max C 0 * ‖x‖
have hbc : C ≤ max C 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) = Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G)
x : E
⊢ Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ ‖g‖ * ‖x‖
have rw : Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G) ≤ ‖g‖ * ‖x‖
Tactic: rw [h x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) = Norm.norm.{u_8} (E := G) ((g : (a : E) → G) x : G)
c : ℝ
hc : c ≥ 0
h₂ : ∀ (x : E), Norm.norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖
z : E
⊢ Norm.norm.{u_8} (E := G) ((g : (a : E) → G) z : G) ≤ c * ‖z‖
have rw : Norm.norm.{u_6} (E := F) ((f : (a : E) → F) z : F) ≤ c * ‖z‖
Tactic: rw [← h z]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
C : ℝ
h :
  ∀ (x : E) (y : F),
    norm.{u_8} (E := G) ((((f : (a : E) → F →ₛₗ[σ₂₃] G) x : F →ₛₗ[σ₂₃] G) : (a : F) → G) y : G) ≤ C * ‖x‖ * ‖y‖
x : E
⊢ max (C * ‖x‖) 0 = max C 0 * ‖x‖
have rw : max (C * ‖x‖) 0 = max (C * ‖x‖) (0 * ‖x‖)
Tactic: rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
C : ℝ
h :
  ∀ (x : E) (y : F),
    norm.{u_8} (E := G) ((((f : (a : E) → F →ₛₗ[σ₂₃] G) x : F →ₛₗ[σ₂₃] G) : (a : F) → G) y : G) ≤ C * ‖x‖ * ‖y‖
x : E
rw : max (C * ‖x‖) 0 = max (C * ‖x‖) (0 * ‖x‖)
⊢ max (C * ‖x‖) 0 = max C 0 * ‖x‖
have rw₁ : max (C * ‖x‖) 0 = max (C * ‖x‖) 0
Tactic: rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Fₗ
inst_4 : SeminormedAddCommGroup G
inst_5 : SeminormedAddCommGroup Gₗ
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NontriviallyNormedField 𝕜₂
inst_8 : NontriviallyNormedField 𝕜₃
inst_9 : NormedSpace 𝕜 E
inst_10 : NormedSpace 𝕜 Eₗ
inst_11 : NormedSpace 𝕜₂ F
inst_12 : NormedSpace 𝕜 Fₗ
inst_13 : NormedSpace 𝕜₃ G
inst_14 : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : FunLike 𝓕 E F
inst_17 : RingHomIsometric σ₂₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
h :
  ∃ (C : ℝ),
    ∀ (x : E) (y : F),
      norm.{u_8} (E := G) ((((f : (a : E) → F →ₛₗ[σ₂₃] G) x : F →ₛₗ[σ₂₃] G) : (a : F) → G) y : G) ≤ C * ‖x‖ * ‖y‖
x y : E
⊢ mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) (x + y)) ⋯ =
    HAdd.hAdd (α := F →SL[σ₂₃] G) (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) x) ⋯)
      (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) y) ⋯)
have h₁ : ∀ (z : F),
  Eq.{u_8 + 1} (α := G) ((mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) (x + y)) sorry : (a : F) → G) z : G)
    ((HAdd.hAdd (α := F →SL[σ₂₃] G) (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) x) sorry)
            (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) y) sorry) :
          (a : F) → G)
        z :
      G)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Fₗ
inst_4 : SeminormedAddCommGroup G
inst_5 : SeminormedAddCommGroup Gₗ
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NontriviallyNormedField 𝕜₂
inst_8 : NontriviallyNormedField 𝕜₃
inst_9 : NormedSpace 𝕜 E
inst_10 : NormedSpace 𝕜 Eₗ
inst_11 : NormedSpace 𝕜₂ F
inst_12 : NormedSpace 𝕜 Fₗ
inst_13 : NormedSpace 𝕜₃ G
inst_14 : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : FunLike 𝓕 E F
inst_17 : RingHomIsometric σ₂₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
h :
  ∃ (C : ℝ),
    ∀ (x : E) (y : F),
      norm.{u_8} (E := G) ((((f : (a : E) → F →ₛₗ[σ₂₃] G) x : F →ₛₗ[σ₂₃] G) : (a : F) → G) y : G) ≤ C * ‖x‖ * ‖y‖
c : 𝕜
x : E
⊢ mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) (c • x)) ⋯ =
    HSMul.hSMul (α := 𝕜₃) (β := F →SL[σ₂₃] G) ((σ₁₃ : (a : 𝕜) → 𝕜₃) c : 𝕜₃)
      (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) x) ⋯)
have h₁ : ∀ (z : F),
  Eq.{u_8 + 1} (α := G) ((mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) (c • x)) sorry : (a : F) → G) z : G)
    ((HSMul.hSMul (α := 𝕜₃) (β := F →SL[σ₂₃] G) ((σ₁₃ : (a : 𝕜) → 𝕜₃) c : 𝕜₃)
            (mkContinuousOfExistsBound ((f : (a : E) → F →ₛₗ[σ₂₃] G) x) sorry) :
          (a : F) → G)
        z :
      G)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
inst_10 : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ norm.{u_8} (E := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) ≤ ‖f.flip‖ * ‖x‖ * ‖y‖
have rw : norm.{u_8} (E := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) ≤ ‖f.flip‖ * ‖y‖ * ‖x‖
Tactic: rw [mul_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomIsometric σ₂₃
inst_10 : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
⊢ f.flip.flip = f
have h : ∀ (x : E) (x_1 : F),
  Eq.{u_8 + 1} (α := G) ((((f.flip.flip : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) x_1 : G)
    ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) x_1 : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Fₗ
inst_4 : SeminormedAddCommGroup G
inst_5 : SeminormedAddCommGroup Gₗ
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NontriviallyNormedField 𝕜₂
inst_8 : NontriviallyNormedField 𝕜₃
inst_9 : NormedSpace 𝕜 E
inst_10 : NormedSpace 𝕜 Eₗ
inst_11 : NormedSpace 𝕜₂ F
inst_12 : NormedSpace 𝕜 Fₗ
inst_13 : NormedSpace 𝕜₃ G
inst_14 : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : FunLike 𝓕 E F
inst_17 : RingHomIsometric σ₂₃
inst_18 : RingHomIsometric σ₁₃
inst_19 : RingHomIsometric σ₁₂
c : 𝕜₂
f : F →SL[σ₂₃] G
g : E →SL[σ₁₂] F
⊢ f ∘SL (c • g) = HSMul.hSMul (α := 𝕜₃) ((σ₂₃ : (a : 𝕜₂) → 𝕜₃) c : 𝕜₃) (f ∘SL g)
have h : ∀ (x : E),
  Eq.{u_8 + 1} (α := G) ((f ∘SL (c • g) : (a : E) → G) x : G)
    ((HSMul.hSMul (α := 𝕜₃) ((σ₂₃ : (a : 𝕜₂) → 𝕜₃) c : 𝕜₃) (f ∘SL g) : (a : E) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : SeminormedAddCommGroup Gₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
⊢ sorry * ‖L‖ ≤ 1 * ‖L‖
have hbc : LE.le (α := ℝ) sorry 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : SeminormedAddCommGroup Gₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
⊢ 1 * ‖L‖ = ‖L‖
have rw : ‖L‖ = ‖L‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst_9 : SeminormedAddCommGroup E'
inst_10 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_11 : NontriviallyNormedField 𝕜₁'
inst_12 : NontriviallyNormedField 𝕜₂'
inst_13 : NormedSpace 𝕜₁' E'
inst_14 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_17 : RingHomIsometric σ₂₃
inst_18 : RingHomIsometric σ₁₃'
inst_19 : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gF : F' →SL[σ₂'] F
⊢ Eq (α := E' →SL[σ₁₃'] F' →SL[σ₂₃'] G) (f.bilinearComp (σ₁' := σ₁') 0 gF) 0
have h : ∀ (x : E') (x_1 : F'),
  Eq.{u_8 + 1} (α := G)
    ((((f.bilinearComp (σ₁' := σ₁') 0 gF : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : G)
    ((((0 : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst_9 : SeminormedAddCommGroup E'
inst_10 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_11 : NontriviallyNormedField 𝕜₁'
inst_12 : NontriviallyNormedField 𝕜₂'
inst_13 : NormedSpace 𝕜₁' E'
inst_14 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_17 : RingHomIsometric σ₂₃
inst_18 : RingHomIsometric σ₁₃'
inst_19 : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gE : E' →SL[σ₁'] E
⊢ Eq (α := E' →SL[σ₁₃'] F' →SL[σ₂₃'] G) (f.bilinearComp (σ₂' := σ₂') gE 0) 0
have h : ∀ (x : E') (x_1 : F'),
  Eq.{u_8 + 1} (α := G)
    ((((f.bilinearComp (σ₂' := σ₂') gE 0 : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : G)
    ((((0 : (a : E') → F' →SL[σ₂₃'] G) x : F' →SL[σ₂₃'] G) : (a : F') → G) x_1 : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : SeminormedAddCommGroup Gₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 Fₗ
inst_6 : NormedSpace 𝕜 Gₗ
f : E →L[𝕜] Fₗ →L[𝕜] Gₗ
x x' : E
y y' : Fₗ
⊢ (((f : (a : E) → Fₗ →L[𝕜] Gₗ) (x + x') : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) (y + y') =
    HAdd.hAdd (β := Gₗ)
      (HAdd.hAdd (α := Gₗ) (β := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
        ((((f.deriv₂ : (a : E × Fₗ) → E × Fₗ →L[𝕜] Gₗ) (x, y) : E × Fₗ →L[𝕜] Gₗ) : (a : E × Fₗ) → Gₗ) (x', y') : Gₗ))
      ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ)
have simp : HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
    (HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
      (HAdd.hAdd (α := Gₗ) (β := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ)
        ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ))) =
  HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
    (HAdd.hAdd (α := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ)
      (HAdd.hAdd (α := Gₗ) (β := Gₗ) ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y : Gₗ)
        ((((f : (a : E) → Fₗ →L[𝕜] Gₗ) x' : Fₗ →L[𝕜] Gₗ) : (a : Fₗ) → Gₗ) y' : Gₗ)))
Tactic: simp only [map_add, add_apply, coe_deriv₂, add_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
⊢ norm (E := E →L[𝕜] Fₗ) (smulRight c f) = ‖c‖ * ‖f‖
have refine_1 : norm (E := E →L[𝕜] Fₗ) (smulRight c f) ≤ ‖c‖ * ‖f‖
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
refine_1 : norm (E := E →L[𝕜] Fₗ) (smulRight c f) ≤ ‖c‖ * ‖f‖
⊢ norm (E := E →L[𝕜] Fₗ) (smulRight c f) = ‖c‖ * ‖f‖
have refine_2 : ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
⊢ norm (E := E →L[𝕜] Fₗ) (smulRight c f) ≤ ‖c‖ * ‖f‖
have refine_1 : ∀ (x : E), norm.{u_7} (E := Fₗ) ((smulRight c f : (a : E) → Fₗ) x : Fₗ) ≤ ‖c‖ * ‖f‖ * ‖x‖
Tactic: refine opNorm_le_bound _ (by positivity) fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
x : E
⊢ norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) * ‖f‖ ≤ ‖c‖ * ‖x‖ * ‖f‖
have hbc : norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) ≤ ‖c‖ * ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
x : E
⊢ norm.{u_7} (E := Fₗ) ((smulRight c f : (a : E) → Fₗ) x : Fₗ) ≤ ‖c‖ * ‖f‖ * ‖x‖
have x₁ : norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) * ‖f‖ ≤ ‖c‖ * ‖x‖ * ‖f‖
Tactic: calc
      ‖c x • f‖ = ‖c x‖ * ‖f‖ := norm_smul _ _
      _ ≤ ‖c‖ * ‖x‖ * ‖f‖ := by gcongr; apply le_opNorm
      _ = ‖c‖ * ‖f‖ * ‖x‖ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
x : E
x₁ : norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) * ‖f‖ ≤ ‖c‖ * ‖x‖ * ‖f‖
⊢ norm.{u_7} (E := Fₗ) ((smulRight c f : (a : E) → Fₗ) x : Fₗ) ≤ ‖c‖ * ‖f‖ * ‖x‖
have x₂ : ‖c‖ * ‖x‖ * ‖f‖ = ‖c‖ * ‖f‖ * ‖x‖
Tactic: calc
      ‖c x • f‖ = ‖c x‖ * ‖f‖ := norm_smul _ _
      _ ≤ ‖c‖ * ‖x‖ * ‖f‖ := by gcongr; apply le_opNorm
      _ = ‖c‖ * ‖f‖ * ‖x‖ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
⊢ ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)
have refine_2 : ∀ (hf : ‖f‖ = 0), ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)
Tactic: obtain hf | hf := (norm_nonneg f).eq_or_lt'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
refine_2 : ∀ (hf : ‖f‖ = 0), ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)
⊢ ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)
have refine_2₁ : ∀ (hf : 0 < ‖f‖), ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)
Tactic: obtain hf | hf := (norm_nonneg f).eq_or_lt'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
hf : 0 < ‖f‖
⊢ ‖c‖ * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f)
have refine_2 : ‖c‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) / ‖f‖
Tactic: rw [← le_div_iff₀ hf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
hf : 0 < ‖f‖
⊢ ‖c‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) / ‖f‖
have refine_2 : ∀ (x : E), norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) / ‖f‖ * ‖x‖
Tactic: refine opNorm_le_bound _ (by positivity) fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
hf : 0 < ‖f‖
x : E
⊢ norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) / ‖f‖ * ‖x‖
have refine_2 : norm.{u_1} (E := 𝕜) ((c : (a : E) → 𝕜) x : 𝕜) * ‖f‖ ≤ norm (E := E →L[𝕜] Fₗ) (smulRight c f) * ‖x‖
Tactic: rw [div_mul_eq_mul_div, le_div_iff₀ hf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Fₗ
inst_4 : SeminormedAddCommGroup G
inst_5 : SeminormedAddCommGroup Gₗ
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NontriviallyNormedField 𝕜₂
inst_8 : NontriviallyNormedField 𝕜₃
inst_9 : NormedSpace 𝕜 E
inst_10 : NormedSpace 𝕜 Eₗ
inst_11 : NormedSpace 𝕜₂ F
inst_12 : NormedSpace 𝕜 Fₗ
inst_13 : NormedSpace 𝕜₃ G
inst_14 : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : FunLike 𝓕 E F
σ₂₁ : 𝕜₂ →+* 𝕜
inst_17 : RingHomInvPair σ₁₂ σ₂₁
inst_18 : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst_19 : SeminormedAddCommGroup E'
inst_20 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_21 : NontriviallyNormedField 𝕜₁'
inst_22 : NontriviallyNormedField 𝕜₂'
inst_23 : NormedSpace 𝕜₁' E'
inst_24 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_25 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_26 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_27 : RingHomIsometric σ₂₃
inst_28 : RingHomIsometric σ₁₃'
inst_29 : RingHomIsometric σ₂₃'
inst_30 : RingHomIsometric σ₁₃
inst_31 : RingHomIsometric σ₁'
inst_32 : RingHomIsometric σ₂'
c₁ c₂ : StrongDual 𝕜 E
⊢ smulRightₗ (c₁ + c₂) = HAdd.hAdd (α := Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) (smulRightₗ c₁) (smulRightₗ c₂)
have h : ∀ (x : Fₗ) (x_1 : E),
  Eq.{u_7 + 1} (α := Fₗ) ((((smulRightₗ (c₁ + c₂) : (a : Fₗ) → E →L[𝕜] Fₗ) x : E →L[𝕜] Fₗ) : (a : E) → Fₗ) x_1 : Fₗ)
    ((((HAdd.hAdd (α := Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) (smulRightₗ c₁) (smulRightₗ c₂) : (a : Fₗ) → E →L[𝕜] Fₗ) x : E →L[𝕜] Fₗ) :
          (a : E) → Fₗ)
        x_1 :
      Fₗ)
Tactic: ext x