awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst_9 : NormedAddCommGroup Eu] [inst_10 : NormedSpace 𝕜 Eu] [inst_11 : NormedAddCommGroup Fu]
    [inst_12 : NormedSpace 𝕜 Fu] [inst_13 : NormedAddCommGroup Gu] [inst_14 : NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} (hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 n
          (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g s
In : HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 ≤ (↑n.succ : ℕ∞ω)
I1 :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) (Du →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 n
        (fun (y : Du) ↦
          (((precompR Du B : (a : Eu) → (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) (f y) : (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) :
              (a : Du →L[𝕜] Fu) → Du →L[𝕜] Gu)
            (fderivWithin 𝕜 g s y))
        s x) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1 - i)) ↦ Du) Fu)
            (iteratedFDerivWithin 𝕜 (n + 1 - i) g s x)
hbc : sorry ≤ ‖B‖
⊢ HMul.hMul (α := ℝ) sorry
      (∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) (Du →L[𝕜] Eu))
              (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
            (iteratedFDerivWithin 𝕜 (n - i) g s x)) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) (Du →L[𝕜] Eu))
              (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu) (iteratedFDerivWithin 𝕜 (n - i) g s x)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst_9 : NormedAddCommGroup Eu] [inst_10 : NormedSpace 𝕜 Eu] [inst_11 : NormedAddCommGroup Fu]
    [inst_12 : NormedSpace 𝕜 Fu] [inst_13 : NormedAddCommGroup Gu] [inst_14 : NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} (hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 n
          (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g s
In : HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 ≤ (↑n.succ : ℕ∞ω)
I1 :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) (Du →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 n
        (fun (y : Du) ↦
          (((precompR Du B : (a : Eu) → (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) (f y) : (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) :
              (a : Du →L[𝕜] Fu) → Du →L[𝕜] Gu)
            (fderivWithin 𝕜 g s y))
        s x) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1 - i)) ↦ Du) Fu)
            (iteratedFDerivWithin 𝕜 (n + 1 - i) g s x)
⊢ sorry ≤ ‖B‖

Tactic:
B.norm_precompL_le Du

Premises used: ContinuousLinearMap.norm_precompL_le
-- 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
have :
  ∀ (isoD : Du ≃ₗᵢ[𝕜] D),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uG} 𝕜 (fun (i : Fin n) ↦ D) G)
        (iteratedFDerivWithin 𝕜 n (fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) s
          x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uE} 𝕜 (fun (i : Fin i) ↦ D) E)
                (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uF} 𝕜 (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uG} 𝕜 (fun (i : Fin n) ↦ D) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) s
        x) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uE} 𝕜 (fun (i : Fin i) ↦ D) E)
              (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uF} 𝕜 (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDerivWithin 𝕜 (n - i) g s x)

Tactic:
have isoD : Du ≃ₗᵢ[𝕜] D := LinearIsometryEquiv.ulift 𝕜 D
-- 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
have :
  ∀ (isoE : Eu ≃ₗᵢ[𝕜] E),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uG} 𝕜 (fun (i : Fin n) ↦ D) G)
        (iteratedFDerivWithin 𝕜 n (fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) s
          x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uE} 𝕜 (fun (i : Fin i) ↦ D) E)
                (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uF} 𝕜 (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uG} 𝕜 (fun (i : Fin n) ↦ D) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) s
        x) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uE} 𝕜 (fun (i : Fin i) ↦ D) E)
              (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uF} 𝕜 (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDerivWithin 𝕜 (n - i) g s x)

Tactic:
have isoE : Eu ≃ₗᵢ[𝕜] E := LinearIsometryEquiv.ulift 𝕜 E
-- 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
have :
  ∀ (isoF : Fu ≃ₗᵢ[𝕜] F),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uG} 𝕜 (fun (i : Fin n) ↦ D) G)
        (iteratedFDerivWithin 𝕜 n (fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) s
          x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uE} 𝕜 (fun (i : Fin i) ↦ D) E)
                (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uF} 𝕜 (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uG} 𝕜 (fun (i : Fin n) ↦ D) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) s
        x) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uE} 𝕜 (fun (i : Fin i) ↦ D) E)
              (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uF} 𝕜 (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDerivWithin 𝕜 (n - i) g s x)

Tactic:
have isoF : Fu ≃ₗᵢ[𝕜] F := LinearIsometryEquiv.ulift 𝕜 F
-- 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
have :
  ∀ (isoG : Gu ≃ₗᵢ[𝕜] G),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uG} 𝕜 (fun (i : Fin n) ↦ D) G)
        (iteratedFDerivWithin 𝕜 n (fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) s
          x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uE} 𝕜 (fun (i : Fin i) ↦ D) E)
                (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uF} 𝕜 (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uG} 𝕜 (fun (i : Fin n) ↦ D) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) s
        x) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uE} 𝕜 (fun (i : Fin i) ↦ D) E)
              (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uF} 𝕜 (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDerivWithin 𝕜 (n - i) g s x)

Tactic:
have isoG : Gu ≃ₗᵢ[𝕜] G := LinearIsometryEquiv.ulift 𝕜 G
-- 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₀
⊢ 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₀

Tactic:
have hBu : Bu = ContinuousLinearMap.compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)
      (ContinuousLinearMap.compL 𝕜 Fu G Gu (isoG.symm : G →L[𝕜] Gu)) Bu₀ := rfl
-- 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₀
h :
  ∀ (y : Du),
    Eq (α := Gu) ((((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y) : Gu)
      (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 :
        Gu)
⊢ 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)))

Tactic:
ext1 y
-- 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₀
y : Du
⊢ Eq (α := Gu) ((((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y) : Gu)
    (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 :
      Gu)

Tactic:
simp [Du, Eu, Fu, Gu, hBu, Bu₀, fu, gu]
-- 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₀
⊢ 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)))

Tactic:
have Bu_eq : (fun y => Bu (fu y) (gu y)) = isoG.symm ∘ (fun y => B (f y) (g y)) ∘ isoD := by
    ext1 y
    simp [Du, Eu, Fu, Gu, hBu, Bu₀, fu, gu]