awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
i : ℕ
rw rw₁ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)

Tactic:
rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ hs hx]

Premises used: LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
⊢ ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)

Tactic:
have Nfu : ∀ i, ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖ := fun i ↦ by
    rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ hs hx]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
⊢ ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i

Tactic:
simp_rw [← Nfu] at hD
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
i : ℕ
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) G)
      (iteratedFDerivWithin 𝕜 i (g ∘ (⇑isoF : (a : Fu) → F)) tu (fu x)) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G) (iteratedFDerivWithin 𝕜 i g t (f x))
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G) (iteratedFDerivWithin 𝕜 i g t (f x))

Tactic:
rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ htu (hstu hx)]

Premises used: LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
i : ℕ
hx₁ : Membership.mem (α := F) t ((isoF : (a : Fu) → F) (fu x) : F)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) G)
      (iteratedFDerivWithin 𝕜 i (g ∘ (⇑isoF : (a : Fu) → F)) tu (fu x)) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G) (iteratedFDerivWithin 𝕜 i g t (f x))

Tactic:
rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right _ _ ht, Ffu]

Premises used: LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
i : ℕ
hx₁ : f x ∈ t
⊢ Membership.mem (α := F) t ((isoF : (a : Fu) → F) (fu x) : F)

Tactic:
rw [Ffu]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
i : ℕ
⊢ f x ∈ t

Tactic:
hst hx
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
i : ℕ
⊢ f x ∈ t

Tactic:
exact hst hx
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
⊢ ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x))

Tactic:
have Ngu : ∀ i,
      ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ = ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ := fun i ↦ by
    rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ htu (hstu hx)]
    rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right _ _ ht, Ffu]
    rw [Ffu]
    exact hst hx
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x)) ≤
      C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
Ngu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x))
⊢ ∀ i ≤ n, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) ≤ C

Tactic:
simp_rw [← Ngu] at hC
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
Ngu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x))
hC :
  ∀ i ≤ n, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) ≤ C
h : ∀ (x : E), ULift.down.{uF, uG} ((gu ∘ fu) x) = ULift.down.{uF, uG} (((⇑isoG.symm : (a : G) → Gu) ∘ g ∘ f) x)
⊢ gu ∘ fu = (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ f

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x_1 : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x_1 ∈ s
C D : ℝ
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x_1) = f x_1
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x_1) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x_1)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x_1) ≤ D ^ i
Ngu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x_1)) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x_1))
hC :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x_1)) ≤ C
x : E
⊢ ULift.down.{uF, uG} ((gu ∘ fu) x) = ULift.down.{uF, uG} (((⇑isoG.symm : (a : G) → Gu) ∘ g ∘ f) x)

Tactic:
simp only [fu, gu, comp_apply,
        LinearIsometryEquiv.apply_symm_apply]

Premises used: LinearIsometryEquiv.apply_symm_apply, Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : (↑n : ℕ∞ω) ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ f
gu : Fu → Gu := (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ (⇑isoF : (a : Fu) → F)
tu : Set Fu := (⇑isoF : (a : Fu) → F) ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : (isoF : (a : Fu) → F) (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu s
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu tu
Nfu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n → norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) Fu) (iteratedFDerivWithin 𝕜 i fu s x) ≤ D ^ i
Ngu :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uF, uG} 𝕜 (fun (i : Fin i) ↦ F) G)
        (iteratedFDerivWithin 𝕜 i g t (f x))
hC :
  ∀ i ≤ n, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i gu tu (fu x)) ≤ C
⊢ gu ∘ fu = (⇑isoG.symm : (a : G) → Gu) ∘ g ∘ f

Tactic:
have : gu ∘ fu = isoG.symm ∘ g ∘ f := by
      ext x
      simp only [fu, gu, comp_apply,
        LinearIsometryEquiv.apply_symm_apply]