awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := (⇑isoE.symm : (a : E) → Eu) ∘ f ∘ (⇑isoD : (a : Du) → D)
gu : Du → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ g ∘ (⇑isoD : (a : Du) → D)
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G :=
  flip
    (comp (σ₂₃ := RingHom.id 𝕜) (B ∘SL (↑(↑isoE : Eu ≃L[𝕜] E) : Eu →L[𝕜] E)).flip (↑(↑isoF : Fu ≃L[𝕜] F) : Fu →L[𝕜] F))
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
  (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
            (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
          ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
            (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
        (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
      (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
    Bu₀
hBu :
  Bu =
    (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
              (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
            ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
              (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
          (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
        (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
      Bu₀
Bu_eq :
  Eq (α := (y : Du) → Gu) (fun (y : Du) ↦ (((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y))
    (Function.comp (β := G) (⇑isoG.symm : (a : G) → Gu)
      ((fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) ∘ (⇑isoD : (a : Du) → D)))
⊢ ‖Bu‖ ≤ ‖B‖

Tactic:
ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg B) fun y => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := (⇑isoE.symm : (a : E) → Eu) ∘ f ∘ (⇑isoD : (a : Du) → D)
gu : Du → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ g ∘ (⇑isoD : (a : Du) → D)
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G :=
  flip
    (comp (σ₂₃ := RingHom.id 𝕜) (B ∘SL (↑(↑isoE : Eu ≃L[𝕜] E) : Eu →L[𝕜] E)).flip (↑(↑isoF : Fu ≃L[𝕜] F) : Fu →L[𝕜] F))
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
  (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
            (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
          ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
            (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
        (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
      (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
    Bu₀
hBu :
  Bu =
    (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
              (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
            ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
              (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
          (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
        (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
      Bu₀
Bu_eq :
  Eq (α := (y : Du) → Gu) (fun (y : Du) ↦ (((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y))
    (Function.comp (β := G) (⇑isoG.symm : (a : G) → Gu)
      ((fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) ∘ (⇑isoD : (a : Du) → D)))
refine : ∀ (y : Eu), norm (E := Fu →L[𝕜] Gu) ((Bu : (a : Eu) → Fu →L[𝕜] Gu) y : Fu →L[𝕜] Gu) ≤ ‖B‖ * ‖y‖
⊢ ‖Bu‖ ≤ ‖B‖

Tactic:
refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg B) fun y => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := (⇑isoE.symm : (a : E) → Eu) ∘ f ∘ (⇑isoD : (a : Du) → D)
gu : Du → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ g ∘ (⇑isoD : (a : Du) → D)
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G :=
  flip
    (comp (σ₂₃ := RingHom.id 𝕜) (B ∘SL (↑(↑isoE : Eu ≃L[𝕜] E) : Eu →L[𝕜] E)).flip (↑(↑isoF : Fu ≃L[𝕜] F) : Fu →L[𝕜] F))
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
  (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
            (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
          ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
            (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
        (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
      (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
    Bu₀
hBu :
  Bu =
    (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
              (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
            ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
              (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
          (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
        (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
      Bu₀
Bu_eq :
  Eq (α := (y : Du) → Gu) (fun (y : Du) ↦ (((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y))
    (Function.comp (β := G) (⇑isoG.symm : (a : G) → Gu)
      ((fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) ∘ (⇑isoD : (a : Du) → D)))
y : Eu
⊢ 0 ≤ ‖B‖ * ‖y‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := (⇑isoE.symm : (a : E) → Eu) ∘ f ∘ (⇑isoD : (a : Du) → D)
gu : Du → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ g ∘ (⇑isoD : (a : Du) → D)
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G :=
  flip
    (comp (σ₂₃ := RingHom.id 𝕜) (B ∘SL (↑(↑isoE : Eu ≃L[𝕜] E) : Eu →L[𝕜] E)).flip (↑(↑isoF : Fu ≃L[𝕜] F) : Fu →L[𝕜] F))
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
  (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
            (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
          ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
            (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
        (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
      (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
    Bu₀
hBu :
  Bu =
    (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
              (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
            ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
              (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
          (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
        (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
      Bu₀
Bu_eq :
  Eq (α := (y : Du) → Gu) (fun (y : Du) ↦ (((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y))
    (Function.comp (β := G) (⇑isoG.symm : (a : G) → Gu)
      ((fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) ∘ (⇑isoD : (a : Du) → D)))
y : Eu
refine :
  ∀ (x : Fu),
    norm (E := Gu) ((((Bu : (a : Eu) → Fu →L[𝕜] Gu) y : Fu →L[𝕜] Gu) : (a : Fu) → Gu) x : Gu) ≤ ‖B‖ * ‖y‖ * ‖x‖
⊢ norm (E := Fu →L[𝕜] Gu) ((Bu : (a : Eu) → Fu →L[𝕜] Gu) y : Fu →L[𝕜] Gu) ≤ ‖B‖ * ‖y‖

Tactic:
refine ContinuousLinearMap.opNorm_le_bound _ (by positivity) fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x_1 : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x_1 ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := (⇑isoE.symm : (a : E) → Eu) ∘ f ∘ (⇑isoD : (a : Du) → D)
gu : Du → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ g ∘ (⇑isoD : (a : Du) → D)
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G :=
  flip
    (comp (σ₂₃ := RingHom.id 𝕜) (B ∘SL (↑(↑isoE : Eu ≃L[𝕜] E) : Eu →L[𝕜] E)).flip (↑(↑isoF : Fu ≃L[𝕜] F) : Fu →L[𝕜] F))
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
  (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
            (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
          ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
            (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
        (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
      (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
    Bu₀
hBu :
  Bu =
    (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
              (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
            ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
              (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
          (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
        (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
      Bu₀
Bu_eq :
  Eq (α := (y : Du) → Gu) (fun (y : Du) ↦ (((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y))
    (Function.comp (β := G) (⇑isoG.symm : (a : G) → Gu)
      ((fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) ∘ (⇑isoD : (a : Du) → D)))
y : Eu
x : Fu
simp :
  norm.{uG} (E := G)
      ((((B : (a : E) → F →L[𝕜] G) ((isoE : (a : ULift.{max uD uF uG, uE} E) → E) y) : F →L[𝕜] G) : (a : F) → G)
          ((isoF : (a : ULift.{max uD uE uG, uF} F) → F) x : F) :
        G) ≤
    ‖B‖ * ‖y‖ * ‖x‖
⊢ norm (E := Gu) ((((Bu : (a : Eu) → Fu →L[𝕜] Gu) y : Fu →L[𝕜] Gu) : (a : Fu) → Gu) x : Gu) ≤ ‖B‖ * ‖y‖ * ‖x‖

Tactic:
simp only [Eu, Fu, Gu, hBu, Bu₀, compL_apply, coe_comp', Function.comp_apply,
      ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe, flip_apply,
      LinearIsometryEquiv.norm_map]

Premises used: ContinuousLinearMap.coe_comp', LinearIsometryEquiv.norm_map, ContinuousLinearMap.compL_apply, ContinuousLinearMap.flip_apply, LinearIsometryEquiv.coe_coe, Function.comp_apply, ContinuousLinearEquiv.coe_coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x_1 : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x_1 ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := (⇑isoE.symm : (a : E) → Eu) ∘ f ∘ (⇑isoD : (a : Du) → D)
gu : Du → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ g ∘ (⇑isoD : (a : Du) → D)
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G :=
  flip
    (comp (σ₂₃ := RingHom.id 𝕜) (B ∘SL (↑(↑isoE : Eu ≃L[𝕜] E) : Eu →L[𝕜] E)).flip (↑(↑isoF : Fu ≃L[𝕜] F) : Fu →L[𝕜] F))
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
  (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
            (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
          ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
            (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
        (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
      (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
    Bu₀
hBu :
  Bu =
    (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
              (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
            ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
              (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
          (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
        (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
      Bu₀
Bu_eq :
  Eq (α := (y : Du) → Gu) (fun (y : Du) ↦ (((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y))
    (Function.comp (β := G) (⇑isoG.symm : (a : G) → Gu)
      ((fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) ∘ (⇑isoD : (a : Du) → D)))
y : Eu
x : Fu
⊢ norm.{uG} (E := G)
      ((((B : (a : E) → F →L[𝕜] G) ((isoE : (a : Eu) → E) y) : F →L[𝕜] G) : (a : F) → G) ((isoF : (a : Fu) → F) x : F) :
        G) ≤
    norm (E := F →L[𝕜] G) ((B : (a : E) → F →L[𝕜] G) ((isoE : (a : Eu) → E) y) : F →L[𝕜] G) *
      norm.{uF} (E := F) ((isoF : (a : Fu) → F) x : F)

Tactic:
ContinuousLinearMap.le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x_1 : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x_1 ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := (⇑isoE.symm : (a : E) → Eu) ∘ f ∘ (⇑isoD : (a : Du) → D)
gu : Du → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ g ∘ (⇑isoD : (a : Du) → D)
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G :=
  flip
    (comp (σ₂₃ := RingHom.id 𝕜) (B ∘SL (↑(↑isoE : Eu ≃L[𝕜] E) : Eu →L[𝕜] E)).flip (↑(↑isoF : Fu ≃L[𝕜] F) : Fu →L[𝕜] F))
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
  (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
            (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
          ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
            (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
        (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
      (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
    Bu₀
hBu :
  Bu =
    (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
              (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
            ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
              (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
          (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
        (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
      Bu₀
Bu_eq :
  Eq (α := (y : Du) → Gu) (fun (y : Du) ↦ (((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y))
    (Function.comp (β := G) (⇑isoG.symm : (a : G) → Gu)
      ((fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) ∘ (⇑isoD : (a : Du) → D)))
y : Eu
x : Fu
hbc :
  norm (E := F →L[𝕜] G) ((B : (a : E) → F →L[𝕜] G) ((isoE : (a : Eu) → E) y) : F →L[𝕜] G) ≤
    ‖B‖ * norm.{uE} (E := E) ((isoE : (a : Eu) → E) y : E)
⊢ norm (E := F →L[𝕜] G) ((B : (a : E) → F →L[𝕜] G) ((isoE : (a : Eu) → E) y) : F →L[𝕜] G) *
      norm.{uF} (E := F) ((isoF : (a : Fu) → F) x : F) ≤
    ‖B‖ * norm.{uE} (E := E) ((isoE : (a : Eu) → E) y : E) * norm.{uF} (E := F) ((isoF : (a : Fu) → F) x : F)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x_1 : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x_1 ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := (⇑isoE.symm : (a : E) → Eu) ∘ f ∘ (⇑isoD : (a : Du) → D)
gu : Du → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ g ∘ (⇑isoD : (a : Du) → D)
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G :=
  flip
    (comp (σ₂₃ := RingHom.id 𝕜) (B ∘SL (↑(↑isoE : Eu ≃L[𝕜] E) : Eu →L[𝕜] E)).flip (↑(↑isoF : Fu ≃L[𝕜] F) : Fu →L[𝕜] F))
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
  (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
            (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
          ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
            (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
        (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
      (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
    Bu₀
hBu :
  Bu =
    (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
              (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
            ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
              (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
          (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
        (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
      Bu₀
Bu_eq :
  Eq (α := (y : Du) → Gu) (fun (y : Du) ↦ (((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y))
    (Function.comp (β := G) (⇑isoG.symm : (a : G) → Gu)
      ((fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) ∘ (⇑isoD : (a : Du) → D)))
y : Eu
x : Fu
⊢ norm (E := F →L[𝕜] G) ((B : (a : E) → F →L[𝕜] G) ((isoE : (a : Eu) → E) y) : F →L[𝕜] G) ≤
    ‖B‖ * norm.{uE} (E := E) ((isoE : (a : Eu) → E) y : E)

Tactic:
apply ContinuousLinearMap.le_opNorm

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x_1 : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x_1 ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := (⇑isoE.symm : (a : E) → Eu) ∘ f ∘ (⇑isoD : (a : Du) → D)
gu : Du → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ g ∘ (⇑isoD : (a : Du) → D)
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G :=
  flip
    (comp (σ₂₃ := RingHom.id 𝕜) (B ∘SL (↑(↑isoE : Eu ≃L[𝕜] E) : Eu →L[𝕜] E)).flip (↑(↑isoF : Fu ≃L[𝕜] F) : Fu →L[𝕜] F))
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
  (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
            (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
          ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
            (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
        (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
      (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
    Bu₀
hBu :
  Bu =
    (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
              (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
            ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
              (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
          (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
        (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
      Bu₀
Bu_eq :
  Eq (α := (y : Du) → Gu) (fun (y : Du) ↦ (((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y))
    (Function.comp (β := G) (⇑isoG.symm : (a : G) → Gu)
      ((fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) ∘ (⇑isoD : (a : Du) → D)))
y : Eu
x : Fu
⊢ ‖B‖ * norm.{uE} (E := E) ((isoE : (a : Eu) → E) y : E) * norm.{uF} (E := F) ((isoF : (a : Fu) → F) x : F) =
    ‖B‖ * ‖y‖ * ‖x‖

Tactic:
simp only [LinearIsometryEquiv.norm_map]

Premises used: LinearIsometryEquiv.norm_map