awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
ι : Type u_8
inst : Fintype ι
inst_1 : DecidableEq ι
𝕜 : Type u_9
inst_2 : NontriviallyNormedField 𝕜
E : ι → Type u_10
inst_3 : (i : ι) → SeminormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_9, u_10} 𝕜 (E i)
i : ι
inst_5 : NontrivialTopology.{u_10} (E i)
⊢ norm (E := E i →L[𝕜] (i : ι) → E i) (single 𝕜 E i : E i →L[𝕜] (i : ι) → E i) = 1

Tactic:
(LinearIsometry.single 𝕜 E i).norm_toContinuousLinearMap

Premises used: ContinuousLinearMap.single, LinearIsometry.norm_toContinuousLinearMap, LinearMap.single, LinearIsometry.single, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
E : Type u_9
F : Type u_10
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
⊢ Eq (α := E × F) ((LinearIsometry.inl 𝕜 E F : (a : E) → E × F) x : E × F) ((x, 0) : E × F)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
E : Type u_9
F : Type u_10
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
y : F
⊢ Eq (α := E × F) ((LinearIsometry.inr 𝕜 E F : (a : F) → E × F) y : E × F) ((0, y) : E × F)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
E : Type u_9
F : Type u_10
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ norm (E := E →L[𝕜] E × F) (inl 𝕜 E F) ≤ 1

Tactic:
(LinearIsometry.inl 𝕜 E F).norm_toContinuousLinearMap_le

Premises used: LinearMap.inl, setOf, LinearIsometry.inl, ContinuousLinearMap.prod, LinearMap.prod, LinearIsometry.norm_toContinuousLinearMap_le, ContinuousLinearMap.inl, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
E : Type u_9
F : Type u_10
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ norm (E := F →L[𝕜] E × F) (inr 𝕜 E F) ≤ 1

Tactic:
(LinearIsometry.inr 𝕜 E F).norm_toContinuousLinearMap_le

Premises used: setOf, ContinuousLinearMap.inr, LinearIsometry.inr, ContinuousLinearMap.prod, LinearMap.prod, LinearIsometry.norm_toContinuousLinearMap_le, LinearMap.inr, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
E : Type u_9
F : Type u_10
inst_1 : SeminormedAddCommGroup E
inst_2 : NontrivialTopology E
inst_3 : NormedSpace 𝕜 E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
⊢ norm (E := E →L[𝕜] E × F) (inl 𝕜 E F) = 1

Tactic:
(LinearIsometry.inl 𝕜 E F).norm_toContinuousLinearMap

Premises used: LinearMap.inl, LinearIsometry.norm_toContinuousLinearMap, setOf, LinearIsometry.inl, ContinuousLinearMap.prod, LinearMap.prod, ContinuousLinearMap.inl, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
E : Type u_9
F : Type u_10
inst_1 : SeminormedAddCommGroup E
inst_2 : NontrivialTopology E
inst_3 : NormedSpace 𝕜 E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : NontrivialTopology F
⊢ norm (E := F →L[𝕜] E × F) (inr 𝕜 E F) = 1

Tactic:
(LinearIsometry.inr 𝕜 E F).norm_toContinuousLinearMap

Premises used: LinearIsometry.norm_toContinuousLinearMap, setOf, ContinuousLinearMap.inr, LinearIsometry.inr, ContinuousLinearMap.prod, LinearMap.prod, LinearMap.inr, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
x : E × F
e : E
f : F
⊢ Norm.norm.{u_2} (E := E) (((fst 𝕜 E F : E × F →L[𝕜] E) : (a : E × F) → E) (e, f) : E) ≤ 1 * ‖(e, f)‖

Tactic:
simpa only [one_mul] using le_max_left ‖e‖ ‖f‖

Premises used: Norm.norm, le_max_left, one_mul
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
x : E × F
e : E
f : F
⊢ Norm.norm.{u_3} (E := F) (((snd 𝕜 E F : E × F →L[𝕜] F) : (a : E × F) → F) (e, f) : F) ≤ 1 * ‖(e, f)‖

Tactic:
simpa only [one_mul] using le_max_right ‖e‖ ‖f‖

Premises used: le_max_right, Norm.norm, one_mul
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F
g : E →L[𝕜] G
x : E
⊢ Norm.norm (E := F × G) ((f.prod g : (a : E) → F × G) x : F × G) ≤ ‖(f, g)‖ * ‖x‖

Tactic:
simpa only [prod_apply, Prod.norm_def, max_mul_of_nonneg, norm_nonneg] using
          max_le_max (le_opNorm f x) (le_opNorm g x)

Premises used: ContinuousLinearMap.le_opNorm, max_mul_of_nonneg, Prod.norm_def, max_le_max, ContinuousLinearMap.prod_apply, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F
g : E →L[𝕜] G
⊢ ‖f.prod g‖₊ = ‖(f, g)‖₊

Tactic:
Subtype.ext <| opNorm_prod f g

Premises used: ContinuousLinearMap.opNorm_prod, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst_7 : SeminormedAddCommGroup M₁
inst_8 : NormedSpace 𝕜 M₁
inst_9 : SeminormedAddCommGroup M₂
inst_10 : NormedSpace 𝕜 M₂
inst_11 : SeminormedAddCommGroup M₃
inst_12 : NormedSpace 𝕜 M₃
inst_13 : SeminormedAddCommGroup M₄
inst_14 : NormedSpace 𝕜 M₄
h :
  ∀ (x : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)),
    x.1.prodMap x.2 =
      (have Φ₁ : (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄ :=
            (compL 𝕜 M₁ M₂ (M₂ × M₄) : (a : M₂ →L[𝕜] M₂ × M₄) → (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄) (inl 𝕜 M₂ M₄);
          have Φ₂ : (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄ :=
            (compL 𝕜 M₃ M₄ (M₂ × M₄) : (a : M₄ →L[𝕜] M₂ × M₄) → (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄) (inr 𝕜 M₂ M₄);
          have Φ₁' : (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
            (flip (compL 𝕜 (M₁ × M₃) M₁ (M₂ × M₄)) :
                (a : M₁ × M₃ →L[𝕜] M₁) → (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
              (fst 𝕜 M₁ M₃);
          have Φ₂' : (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
            (flip (compL 𝕜 (M₁ × M₃) M₃ (M₂ × M₄)) :
                (a : M₁ × M₃ →L[𝕜] M₃) → (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
              (snd 𝕜 M₁ M₃);
          have Ψ₁ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ →L[𝕜] M₂ := fst 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
          have Ψ₂ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₄ := snd 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
          Φ₁' ∘SL Φ₁ ∘SL Ψ₁ + Φ₂' ∘SL Φ₂ ∘SL Ψ₂ :
          (a : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) → M₁ × M₃ →L[𝕜] M₂ × M₄)
        x
⊢ Eq (α := (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) → M₁ × M₃ →L[𝕜] M₂ × M₄)
    (fun (p : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) ↦ p.1.prodMap p.2)
    (⇑(have Φ₁ : (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄ :=
          (compL 𝕜 M₁ M₂ (M₂ × M₄) : (a : M₂ →L[𝕜] M₂ × M₄) → (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄) (inl 𝕜 M₂ M₄);
        have Φ₂ : (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄ :=
          (compL 𝕜 M₃ M₄ (M₂ × M₄) : (a : M₄ →L[𝕜] M₂ × M₄) → (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄) (inr 𝕜 M₂ M₄);
        have Φ₁' : (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
          (flip (compL 𝕜 (M₁ × M₃) M₁ (M₂ × M₄)) :
              (a : M₁ × M₃ →L[𝕜] M₁) → (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
            (fst 𝕜 M₁ M₃);
        have Φ₂' : (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
          (flip (compL 𝕜 (M₁ × M₃) M₃ (M₂ × M₄)) :
              (a : M₁ × M₃ →L[𝕜] M₃) → (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
            (snd 𝕜 M₁ M₃);
        have Ψ₁ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ →L[𝕜] M₂ := fst 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
        have Ψ₂ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₄ := snd 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
        Φ₁' ∘SL Φ₁ ∘SL Ψ₁ + Φ₂' ∘SL Φ₂ ∘SL Ψ₂) :
      (a : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) → M₁ × M₃ →L[𝕜] M₂ × M₄)

Tactic:
apply funext

Premises used: funext
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst_7 : SeminormedAddCommGroup M₁
inst_8 : NormedSpace 𝕜 M₁
inst_9 : SeminormedAddCommGroup M₂
inst_10 : NormedSpace 𝕜 M₂
inst_11 : SeminormedAddCommGroup M₃
inst_12 : NormedSpace 𝕜 M₃
inst_13 : SeminormedAddCommGroup M₄
inst_14 : NormedSpace 𝕜 M₄
φ : M₁ →L[𝕜] M₂
ψ : M₃ →L[𝕜] M₄
⊢ (φ, ψ).1.prodMap (φ, ψ).2 =
    (have Φ₁ : (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄ :=
          (compL 𝕜 M₁ M₂ (M₂ × M₄) : (a : M₂ →L[𝕜] M₂ × M₄) → (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄) (inl 𝕜 M₂ M₄);
        have Φ₂ : (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄ :=
          (compL 𝕜 M₃ M₄ (M₂ × M₄) : (a : M₄ →L[𝕜] M₂ × M₄) → (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄) (inr 𝕜 M₂ M₄);
        have Φ₁' : (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
          (flip (compL 𝕜 (M₁ × M₃) M₁ (M₂ × M₄)) :
              (a : M₁ × M₃ →L[𝕜] M₁) → (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
            (fst 𝕜 M₁ M₃);
        have Φ₂' : (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
          (flip (compL 𝕜 (M₁ × M₃) M₃ (M₂ × M₄)) :
              (a : M₁ × M₃ →L[𝕜] M₃) → (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
            (snd 𝕜 M₁ M₃);
        have Ψ₁ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ →L[𝕜] M₂ := fst 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
        have Ψ₂ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₄ := snd 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
        Φ₁' ∘SL Φ₁ ∘SL Ψ₁ + Φ₂' ∘SL Φ₂ ∘SL Ψ₂ :
        (a : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) → M₁ × M₃ →L[𝕜] M₂ × M₄)
      (φ, ψ)

Tactic:
ContinuousLinearMap.ext fun ⟨x₁, x₂⟩ => ?_

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.prodMap, ContinuousLinearMap.compL, Prod.mk, ContinuousLinearMap.snd, Prod.fst, ContinuousLinearMap, ContinuousLinearMap.inr, HAdd.hAdd, ContinuousLinearMap.flip, ContinuousLinearMap.fst, ContinuousLinearMap.inl, Prod, RingHom.id, Eq, Prod.snd, DFunLike.coe, ContinuousLinearMap.ext, _private.0.ContinuousLinearMap.norm_fst_le.match_1
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst_7 : SeminormedAddCommGroup M₁
inst_8 : NormedSpace 𝕜 M₁
inst_9 : SeminormedAddCommGroup M₂
inst_10 : NormedSpace 𝕜 M₂
inst_11 : SeminormedAddCommGroup M₃
inst_12 : NormedSpace 𝕜 M₃
inst_13 : SeminormedAddCommGroup M₄
inst_14 : NormedSpace 𝕜 M₄
φ : M₁ →L[𝕜] M₂
ψ : M₃ →L[𝕜] M₄
x : M₁ × M₃
x₁ : M₁
x₂ : M₃
⊢ Eq (α := M₂ × M₄) (((φ, ψ).1.prodMap (φ, ψ).2 : (a : M₁ × M₃) → M₂ × M₄) (x₁, x₂) : M₂ × M₄)
    ((((have Φ₁ : (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄ :=
                  (compL 𝕜 M₁ M₂ (M₂ × M₄) : (a : M₂ →L[𝕜] M₂ × M₄) → (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄)
                    (inl 𝕜 M₂ M₄);
                have Φ₂ : (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄ :=
                  (compL 𝕜 M₃ M₄ (M₂ × M₄) : (a : M₄ →L[𝕜] M₂ × M₄) → (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄)
                    (inr 𝕜 M₂ M₄);
                have Φ₁' : (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
                  (flip (compL 𝕜 (M₁ × M₃) M₁ (M₂ × M₄)) :
                      (a : M₁ × M₃ →L[𝕜] M₁) → (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
                    (fst 𝕜 M₁ M₃);
                have Φ₂' : (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
                  (flip (compL 𝕜 (M₁ × M₃) M₃ (M₂ × M₄)) :
                      (a : M₁ × M₃ →L[𝕜] M₃) → (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
                    (snd 𝕜 M₁ M₃);
                have Ψ₁ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ →L[𝕜] M₂ := fst 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
                have Ψ₂ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₄ := snd 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
                Φ₁' ∘SL Φ₁ ∘SL Ψ₁ + Φ₂' ∘SL Φ₂ ∘SL Ψ₂ :
                (a : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) → M₁ × M₃ →L[𝕜] M₂ × M₄)
              (φ, ψ) :
            M₁ × M₃ →L[𝕜] M₂ × M₄) :
          (a : M₁ × M₃) → M₂ × M₄)
        (x₁, x₂) :
      M₂ × M₄)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst_1 : SeminormedAddCommGroup M₁
inst_2 : NormedSpace 𝕜 M₁
inst_3 : SeminormedAddCommGroup M₂
inst_4 : NormedSpace 𝕜 M₂
inst_5 : SeminormedAddCommGroup M₃
inst_6 : NormedSpace 𝕜 M₃
inst_7 : SeminormedAddCommGroup M₄
inst_8 : NormedSpace 𝕜 M₄
p : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)
⊢ (prodMapL 𝕜 M₁ M₂ M₃ M₄ : (a : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) → M₁ × M₃ →L[𝕜] M₂ × M₄) p = p.1.prodMap p.2

Tactic:
rfl

Premises used: ContinuousLinearMap.prodMap, ContinuousLinearMap.prod, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst_1 : SeminormedAddCommGroup M₁
inst_2 : NormedSpace 𝕜 M₁
inst_3 : SeminormedAddCommGroup M₂
inst_4 : NormedSpace 𝕜 M₂
inst_5 : SeminormedAddCommGroup M₃
inst_6 : NormedSpace 𝕜 M₃
inst_7 : SeminormedAddCommGroup M₄
inst_8 : NormedSpace 𝕜 M₄
X : Type u_9
inst_9 : TopologicalSpace X
f : X → M₁ →L[𝕜] M₂
g : X → M₃ →L[𝕜] M₄
hf : Continuous f
hg : Continuous g
⊢ Continuous (Y := M₁ × M₃ →L[𝕜] M₂ × M₄) fun (x : X) ↦ (f x).prodMap (g x)

Tactic:
(prodMapL 𝕜 M₁ M₂ M₃ M₄).continuous.comp (hf.prodMk hg)

Premises used: Continuous.comp, ContinuousLinearMap.prodMap, ContinuousLinearMap.continuous, ContinuousLinearMap.prod, ContinuousLinearMap.prodMapL, Continuous.prodMk
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst_1 : SeminormedAddCommGroup M₁
inst_2 : NormedSpace 𝕜 M₁
inst_3 : SeminormedAddCommGroup M₂
inst_4 : NormedSpace 𝕜 M₂
inst_5 : SeminormedAddCommGroup M₃
inst_6 : NormedSpace 𝕜 M₃
inst_7 : SeminormedAddCommGroup M₄
inst_8 : NormedSpace 𝕜 M₄
X : Type u_9
inst_9 : TopologicalSpace X
f : X → M₁ ≃L[𝕜] M₂
g : X → M₃ ≃L[𝕜] M₄
hf : Continuous (Y := M₁ →L[𝕜] M₂) fun (x : X) ↦ (↑(f x) : M₁ →L[𝕜] M₂)
hg : Continuous (Y := M₃ →L[𝕜] M₄) fun (x : X) ↦ (↑(g x) : M₃ →L[𝕜] M₄)
⊢ Continuous (Y := M₁ × M₃ →L[𝕜] M₂ × M₄) fun (x : X) ↦ (↑((f x).prodCongr (g x)) : M₁ × M₃ →L[𝕜] M₂ × M₄)

Tactic:
(prodMapL 𝕜 M₁ M₂ M₃ M₄).continuous.comp (hf.prodMk hg)

Premises used: Continuous.comp, ContinuousLinearMap.prodMap, Prod.map, ContinuousLinearMap.continuous, Function.prod, ContinuousLinearMap.prod, LinearMap.prod, ContinuousLinearMap.prodMapL, ContinuousLinearEquiv.toContinuousLinearMap, Continuous.prodMk
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst_1 : SeminormedAddCommGroup M₁
inst_2 : NormedSpace 𝕜 M₁
inst_3 : SeminormedAddCommGroup M₂
inst_4 : NormedSpace 𝕜 M₂
inst_5 : SeminormedAddCommGroup M₃
inst_6 : NormedSpace 𝕜 M₃
inst_7 : SeminormedAddCommGroup M₄
inst_8 : NormedSpace 𝕜 M₄
X : Type u_9
inst_9 : TopologicalSpace X
f : X → M₁ →L[𝕜] M₂
g : X → M₃ →L[𝕜] M₄
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn (Y := M₁ × M₃ →L[𝕜] M₂ × M₄) (fun (x : X) ↦ (f x).prodMap (g x)) s

Tactic:
((prodMapL 𝕜 M₁ M₂ M₃ M₄).continuous.comp_continuousOn (hf.prodMk hg) :)

Premises used: Continuous.comp_continuousOn, ContinuousLinearMap.prodMap, ContinuousLinearMap.continuous, ContinuousOn.prodMk, ContinuousLinearMap.prod, ContinuousLinearMap.prodMapL
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst_1 : SeminormedAddCommGroup M₁
inst_2 : NormedSpace 𝕜 M₁
inst_3 : SeminormedAddCommGroup M₂
inst_4 : NormedSpace 𝕜 M₂
inst_5 : SeminormedAddCommGroup M₃
inst_6 : NormedSpace 𝕜 M₃
inst_7 : SeminormedAddCommGroup M₄
inst_8 : NormedSpace 𝕜 M₄
X : Type u_9
inst_9 : TopologicalSpace X
f : X → M₁ ≃L[𝕜] M₂
g : X → M₃ ≃L[𝕜] M₄
s : Set X
hf : ContinuousOn (Y := M₁ →L[𝕜] M₂) (fun (x : X) ↦ (↑(f x) : M₁ →L[𝕜] M₂)) s
hg : ContinuousOn (Y := M₃ →L[𝕜] M₄) (fun (x : X) ↦ (↑(g x) : M₃ →L[𝕜] M₄)) s
⊢ ContinuousOn (Y := M₁ × M₃ →L[𝕜] M₂ × M₄) (fun (x : X) ↦ (↑((f x).prodCongr (g x)) : M₁ × M₃ →L[𝕜] M₂ × M₄)) s

Tactic:
hf.prod_mapL _ hg

Premises used: ContinuousLinearMap.prodMap, Prod.map, ContinuousOn.prod_mapL, Function.prod, ContinuousLinearMap.prod, LinearMap.prod, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial E
⊢ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F) = 1

Tactic:
le_antisymm (norm_fst_le ..) ?_

Premises used: ContinuousLinearMap.norm_fst_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial E
refine : 1 ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F)
⊢ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F) = 1

Tactic:
refine le_antisymm (norm_fst_le ..) ?_

Premises used: ContinuousLinearMap.norm_fst_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial E
let : ∀ (e : E) (he : e ≠ 0), 1 ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F)
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F)

Tactic:
let ⟨e, he⟩ := exists_ne (0 : E)
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial E
e : E
he : e ≠ 0
⊢ ‖e‖ ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F : E × F →L[𝕜] E) * max ‖e‖ (Norm.norm.{u_3} (E := F) 0)

Tactic:
have : ‖e‖ ≤ _ * max ‖e‖ ‖(0 : F)‖ := (fst 𝕜 E F).le_opNorm (e, 0)
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial E
e : E
he : e ≠ 0
this : ‖e‖ ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F : E × F →L[𝕜] E) * max ‖e‖ (Norm.norm.{u_3} (E := F) 0)
⊢ ‖e‖ ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F : E × F →L[𝕜] E) * ‖e‖

Tactic:
rw [norm_zero, max_eq_left (norm_nonneg e)] at this

Premises used: norm_zero, max_eq_left, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial E
e : E
he : e ≠ 0
this : ‖e‖ ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F : E × F →L[𝕜] E) * ‖e‖
rwa : 1 * ‖e‖ ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F) * ‖e‖
rwa₁ rwa₂ rwa₃ rwa₄ : ‖e‖ ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F) * ‖e‖
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F)

Tactic:
rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr he), one_mul]

Premises used: Iff.mpr, norm_pos_iff, mul_le_mul_iff_of_pos_right, one_mul
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial F
⊢ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F) = 1

Tactic:
le_antisymm (norm_snd_le ..) ?_

Premises used: le_antisymm, ContinuousLinearMap.norm_snd_le
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial F
refine : 1 ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F)
⊢ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F) = 1

Tactic:
refine le_antisymm (norm_snd_le ..) ?_

Premises used: le_antisymm, ContinuousLinearMap.norm_snd_le
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial F
let : ∀ (f : F) (hf : f ≠ 0), 1 ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F)
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F)

Tactic:
let ⟨f, hf⟩ := exists_ne (0 : F)
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial F
f : F
hf : f ≠ 0
⊢ ‖f‖ ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F : E × F →L[𝕜] F) * max (Norm.norm.{u_2} (E := E) 0) ‖f‖

Tactic:
have : ‖f‖ ≤ _ * max ‖(0 : E)‖ ‖f‖ := (snd 𝕜 E F).le_opNorm (0, f)
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial F
f : F
hf : f ≠ 0
this : ‖f‖ ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F : E × F →L[𝕜] F) * max (Norm.norm.{u_2} (E := E) 0) ‖f‖
⊢ ‖f‖ ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F : E × F →L[𝕜] F) * ‖f‖

Tactic:
rw [norm_zero, max_eq_right (norm_nonneg f)] at this

Premises used: norm_zero, max_eq_right, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial F
f : F
hf : f ≠ 0
this : ‖f‖ ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F : E × F →L[𝕜] F) * ‖f‖
rwa : 1 * ‖f‖ ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F) * ‖f‖
rwa₁ rwa₂ rwa₃ rwa₄ : ‖f‖ ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F) * ‖f‖
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F)

Tactic:
rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr hf), one_mul]

Premises used: Iff.mpr, norm_pos_iff, mul_le_mul_iff_of_pos_right, one_mul
-- Module: Mathlib.Analysis.Normed.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α ℝ
inst_1 : Group α
inst_2 : GroupSeminormClass F α ℝ
f : F
x : α
⊢ Eq (α := ℝ) ((f : (a : α) → ℝ) (x⁻¹ * x) : ℝ) (0 : ℝ)

Tactic:
simp