[GOAL]
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝³⁵ : NontriviallyNormedField 𝕜
inst✝³⁴ : (x : B) → AddCommGroup (E₁ x)
inst✝³³ : (x : B) → Module 𝕜 (E₁ x)
inst✝³² : NormedAddCommGroup F₁
inst✝³¹ : NormedSpace 𝕜 F₁
inst✝³⁰ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁹ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁸ : (x : B) → AddCommGroup (E₂ x)
inst✝²⁷ : (x : B) → Module 𝕜 (E₂ x)
inst✝²⁶ : NormedAddCommGroup F₂
inst✝²⁵ : NormedSpace 𝕜 F₂
inst✝²⁴ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝²³ : (x : B) → TopologicalSpace (E₂ x)
inst✝²² : ∀ (x : B), TopologicalAddGroup (E₂ x)
inst✝²¹ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
EB : Type u_8
inst✝²⁰ : NormedAddCommGroup EB
inst✝¹⁹ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : ChartedSpace HB B
EM : Type u_10
inst✝¹⁵ : NormedAddCommGroup EM
inst✝¹⁴ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace HM M
inst✝¹⁰ : SmoothManifoldWithCorners IM M
n : ℕ∞
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : VectorBundle 𝕜 F₁ E₁
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : SmoothVectorBundle F₁ E₁ IB
inst✝⁴ : SmoothVectorBundle F₂ E₂ IB
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
⊢ SmoothOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) (continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
[PROOFSTEP]
have h₁ := smoothOn_coordChangeL IB e₁' e₁
[GOAL]
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝³⁵ : NontriviallyNormedField 𝕜
inst✝³⁴ : (x : B) → AddCommGroup (E₁ x)
inst✝³³ : (x : B) → Module 𝕜 (E₁ x)
inst✝³² : NormedAddCommGroup F₁
inst✝³¹ : NormedSpace 𝕜 F₁
inst✝³⁰ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁹ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁸ : (x : B) → AddCommGroup (E₂ x)
inst✝²⁷ : (x : B) → Module 𝕜 (E₂ x)
inst✝²⁶ : NormedAddCommGroup F₂
inst✝²⁵ : NormedSpace 𝕜 F₂
inst✝²⁴ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝²³ : (x : B) → TopologicalSpace (E₂ x)
inst✝²² : ∀ (x : B), TopologicalAddGroup (E₂ x)
inst✝²¹ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
EB : Type u_8
inst✝²⁰ : NormedAddCommGroup EB
inst✝¹⁹ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : ChartedSpace HB B
EM : Type u_10
inst✝¹⁵ : NormedAddCommGroup EM
inst✝¹⁴ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace HM M
inst✝¹⁰ : SmoothManifoldWithCorners IM M
n : ℕ∞
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : VectorBundle 𝕜 F₁ E₁
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : SmoothVectorBundle F₁ E₁ IB
inst✝⁴ : SmoothVectorBundle F₂ E₂ IB
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
h₁ : SmoothOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) (fun b => ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)
⊢ SmoothOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) (continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
[PROOFSTEP]
have h₂ := smoothOn_coordChangeL IB e₂ e₂'
[GOAL]
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝³⁵ : NontriviallyNormedField 𝕜
inst✝³⁴ : (x : B) → AddCommGroup (E₁ x)
inst✝³³ : (x : B) → Module 𝕜 (E₁ x)
inst✝³² : NormedAddCommGroup F₁
inst✝³¹ : NormedSpace 𝕜 F₁
inst✝³⁰ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁹ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁸ : (x : B) → AddCommGroup (E₂ x)
inst✝²⁷ : (x : B) → Module 𝕜 (E₂ x)
inst✝²⁶ : NormedAddCommGroup F₂
inst✝²⁵ : NormedSpace 𝕜 F₂
inst✝²⁴ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝²³ : (x : B) → TopologicalSpace (E₂ x)
inst✝²² : ∀ (x : B), TopologicalAddGroup (E₂ x)
inst✝²¹ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
EB : Type u_8
inst✝²⁰ : NormedAddCommGroup EB
inst✝¹⁹ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : ChartedSpace HB B
EM : Type u_10
inst✝¹⁵ : NormedAddCommGroup EM
inst✝¹⁴ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace HM M
inst✝¹⁰ : SmoothManifoldWithCorners IM M
n : ℕ∞
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : VectorBundle 𝕜 F₁ E₁
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : SmoothVectorBundle F₁ E₁ IB
inst✝⁴ : SmoothVectorBundle F₂ E₂ IB
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
h₁ : SmoothOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) (fun b => ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ : SmoothOn IB 𝓘(𝕜, F₂ →L[𝕜] F₂) (fun b => ↑(Trivialization.coordChangeL 𝕜 e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)
⊢ SmoothOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) (continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
[PROOFSTEP]
refine (h₁.mono ?_).cle_arrowCongr (h₂.mono ?_)
[GOAL]
case refine_1
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝³⁵ : NontriviallyNormedField 𝕜
inst✝³⁴ : (x : B) → AddCommGroup (E₁ x)
inst✝³³ : (x : B) → Module 𝕜 (E₁ x)
inst✝³² : NormedAddCommGroup F₁
inst✝³¹ : NormedSpace 𝕜 F₁
inst✝³⁰ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁹ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁸ : (x : B) → AddCommGroup (E₂ x)
inst✝²⁷ : (x : B) → Module 𝕜 (E₂ x)
inst✝²⁶ : NormedAddCommGroup F₂
inst✝²⁵ : NormedSpace 𝕜 F₂
inst✝²⁴ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝²³ : (x : B) → TopologicalSpace (E₂ x)
inst✝²² : ∀ (x : B), TopologicalAddGroup (E₂ x)
inst✝²¹ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
EB : Type u_8
inst✝²⁰ : NormedAddCommGroup EB
inst✝¹⁹ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : ChartedSpace HB B
EM : Type u_10
inst✝¹⁵ : NormedAddCommGroup EM
inst✝¹⁴ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace HM M
inst✝¹⁰ : SmoothManifoldWithCorners IM M
n : ℕ∞
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : VectorBundle 𝕜 F₁ E₁
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : SmoothVectorBundle F₁ E₁ IB
inst✝⁴ : SmoothVectorBundle F₂ E₂ IB
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
h₁ : SmoothOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) (fun b => ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ : SmoothOn IB 𝓘(𝕜, F₂ →L[𝕜] F₂) (fun b => ↑(Trivialization.coordChangeL 𝕜 e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
[PROOFSTEP]
mfld_set_tac
[GOAL]
case refine_2
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝³⁵ : NontriviallyNormedField 𝕜
inst✝³⁴ : (x : B) → AddCommGroup (E₁ x)
inst✝³³ : (x : B) → Module 𝕜 (E₁ x)
inst✝³² : NormedAddCommGroup F₁
inst✝³¹ : NormedSpace 𝕜 F₁
inst✝³⁰ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁹ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁸ : (x : B) → AddCommGroup (E₂ x)
inst✝²⁷ : (x : B) → Module 𝕜 (E₂ x)
inst✝²⁶ : NormedAddCommGroup F₂
inst✝²⁵ : NormedSpace 𝕜 F₂
inst✝²⁴ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝²³ : (x : B) → TopologicalSpace (E₂ x)
inst✝²² : ∀ (x : B), TopologicalAddGroup (E₂ x)
inst✝²¹ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
EB : Type u_8
inst✝²⁰ : NormedAddCommGroup EB
inst✝¹⁹ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : ChartedSpace HB B
EM : Type u_10
inst✝¹⁵ : NormedAddCommGroup EM
inst✝¹⁴ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace HM M
inst✝¹⁰ : SmoothManifoldWithCorners IM M
n : ℕ∞
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : VectorBundle 𝕜 F₁ E₁
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : SmoothVectorBundle F₁ E₁ IB
inst✝⁴ : SmoothVectorBundle F₂ E₂ IB
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
h₁ : SmoothOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) (fun b => ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ : SmoothOn IB 𝓘(𝕜, F₂ →L[𝕜] F₂) (fun b => ↑(Trivialization.coordChangeL 𝕜 e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
[PROOFSTEP]
mfld_set_tac
[GOAL]
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝²⁹ : NontriviallyNormedField 𝕜
inst✝²⁸ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁷ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁶ : NormedAddCommGroup F₁
inst✝²⁵ : NormedSpace 𝕜 F₁
inst✝²⁴ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²³ : (x : B) → TopologicalSpace (E₁ x)
inst✝²² : (x : B) → AddCommGroup (E₂ x)
inst✝²¹ : (x : B) → Module 𝕜 (E₂ x)
inst✝²⁰ : NormedAddCommGroup F₂
inst✝¹⁹ : NormedSpace 𝕜 F₂
inst✝¹⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁷ : (x : B) → TopologicalSpace (E₂ x)
inst✝¹⁶ : ∀ (x : B), TopologicalAddGroup (E₂ x)
inst✝¹⁵ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
EB : Type u_8
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
EM : Type u_10
inst✝⁹ : NormedAddCommGroup EM
inst✝⁸ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁷ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace HM M
inst✝⁴ : SmoothManifoldWithCorners IM M
n : ℕ∞
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
y₀ y : LE₁E₂
⊢ ↑(chartAt (ModelProd HB (F₁ →L[𝕜] F₂)) y₀) y =
    (↑(chartAt HB y₀.proj) y.proj, inCoordinates F₁ E₁ F₂ E₂ y₀.proj y.proj y₀.proj y.proj y.snd)
[PROOFSTEP]
rw [FiberBundle.chartedSpace_chartAt, trans_apply, LocalHomeomorph.prod_apply, Trivialization.coe_coe,
  LocalHomeomorph.refl_apply, Function.id_def, hom_trivializationAt_apply]
[GOAL]
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝³¹ : NontriviallyNormedField 𝕜
inst✝³⁰ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁹ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁸ : NormedAddCommGroup F₁
inst✝²⁷ : NormedSpace 𝕜 F₁
inst✝²⁶ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁴ : (x : B) → AddCommGroup (E₂ x)
inst✝²³ : (x : B) → Module 𝕜 (E₂ x)
inst✝²² : NormedAddCommGroup F₂
inst✝²¹ : NormedSpace 𝕜 F₂
inst✝²⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁹ : (x : B) → TopologicalSpace (E₂ x)
inst✝¹⁸ : ∀ (x : B), TopologicalAddGroup (E₂ x)
inst✝¹⁷ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
EB : Type u_8
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
EM : Type u_10
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace HM M
inst✝⁶ : SmoothManifoldWithCorners IM M
n : ℕ∞
inst✝⁵ : FiberBundle F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝¹ : SmoothVectorBundle F₁ E₁ IB
inst✝ : SmoothVectorBundle F₂ E₂ IB
⊢ ∀ (e : Pretrivialization (F₁ →L[𝕜] F₂) TotalSpace.proj),
    e ∈ (vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂).pretrivializationAtlas →
      ∀ (e' : Pretrivialization (F₁ →L[𝕜] F₂) TotalSpace.proj),
        e' ∈ (vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂).pretrivializationAtlas →
          ∃ f,
            SmoothOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) f (e.baseSet ∩ e'.baseSet) ∧
              ∀ (b : B),
                b ∈ e.baseSet ∩ e'.baseSet →
                  ∀ (v : F₁ →L[𝕜] F₂), ↑(f b) v = (↑e' { proj := b, snd := Pretrivialization.symm e b v }).snd
[PROOFSTEP]
rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩ _ ⟨e₁', e₂', he₁', he₂', rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝³¹ : NontriviallyNormedField 𝕜
inst✝³⁰ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁹ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁸ : NormedAddCommGroup F₁
inst✝²⁷ : NormedSpace 𝕜 F₁
inst✝²⁶ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁴ : (x : B) → AddCommGroup (E₂ x)
inst✝²³ : (x : B) → Module 𝕜 (E₂ x)
inst✝²² : NormedAddCommGroup F₂
inst✝²¹ : NormedSpace 𝕜 F₂
inst✝²⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁹ : (x : B) → TopologicalSpace (E₂ x)
inst✝¹⁸ : ∀ (x : B), TopologicalAddGroup (E₂ x)
inst✝¹⁷ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
EB : Type u_8
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
EM : Type u_10
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace HM M
inst✝⁶ : SmoothManifoldWithCorners IM M
n : ℕ∞
inst✝⁵ : FiberBundle F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
e₁✝ e₁'✝ : Trivialization F₁ TotalSpace.proj
e₂✝ e₂'✝ : Trivialization F₂ TotalSpace.proj
inst✝¹ : SmoothVectorBundle F₁ E₁ IB
inst✝ : SmoothVectorBundle F₂ E₂ IB
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ ∃ f,
    SmoothOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) f
        ((continuousLinearMap (RingHom.id 𝕜) e₁ e₂).baseSet ∩ (continuousLinearMap (RingHom.id 𝕜) e₁' e₂').baseSet) ∧
      ∀ (b : B),
        b ∈ (continuousLinearMap (RingHom.id 𝕜) e₁ e₂).baseSet ∩ (continuousLinearMap (RingHom.id 𝕜) e₁' e₂').baseSet →
          ∀ (v : F₁ →L[𝕜] F₂),
            ↑(f b) v =
              (↑(continuousLinearMap (RingHom.id 𝕜) e₁' e₂')
                  { proj := b, snd := Pretrivialization.symm (continuousLinearMap (RingHom.id 𝕜) e₁ e₂) b v }).snd
[PROOFSTEP]
exact
  ⟨continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂', smoothOn_continuousLinearMapCoordChange IB,
    continuousLinearMapCoordChange_apply (RingHom.id 𝕜) e₁ e₁' e₂ e₂'⟩


[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : ℕ∞
⊢ Algebra 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : ℕ∞
⊢ IsScalarTower 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
n : ℕ∞
x : M
k : 𝕜
f : C^⊤⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
⊢ (k • f) • h = k • f • h
[PROOFSTEP]
rw [smul_def, smul_def, SmoothMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul, mul_assoc]
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
    (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g'
[PROOFSTEP]
dsimp
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ ↑v (ContMDiffMap.comp (g + g') f) = ↑v (ContMDiffMap.comp g f) + ↑v (ContMDiffMap.comp g' f)
[PROOFSTEP]
rw [SmoothMap.add_comp, Derivation.map_add]
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
k : 𝕜
g : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ AddHom.toFun
      { toFun := fun g => ↑v (ContMDiffMap.comp g f),
        map_add' :=
          (_ :
            ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
              (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
      (k • g) =
    ↑(RingHom.id 𝕜) k •
      AddHom.toFun
        { toFun := fun g => ↑v (ContMDiffMap.comp g f),
          map_add' :=
            (_ :
              ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                  (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
        g
[PROOFSTEP]
dsimp
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
k : 𝕜
g : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ ↑v (ContMDiffMap.comp (k • g) f) = k * ↑v (ContMDiffMap.comp g f)
[PROOFSTEP]
rw [SmoothMap.smul_comp, Derivation.map_smul, smul_eq_mul]
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ ↑{
          toAddHom :=
            { toFun := fun g => ↑v (ContMDiffMap.comp g f),
              map_add' :=
                (_ :
                  ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                    (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                      (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') },
          map_smul' :=
            (_ :
              ∀ (k : 𝕜) (g : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                AddHom.toFun
                    { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                      map_add' :=
                        (_ :
                          ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                            (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                              (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                    (k • g) =
                  ↑(RingHom.id 𝕜) k •
                    AddHom.toFun
                      { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                        map_add' :=
                          (_ :
                            ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                              (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                                (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                      g) }
      (g * g') =
    g •
        ↑{
              toAddHom :=
                { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                  map_add' :=
                    (_ :
                      ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                        (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                          (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') },
              map_smul' :=
                (_ :
                  ∀ (k : 𝕜) (g : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                    AddHom.toFun
                        { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                          map_add' :=
                            (_ :
                              ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                                (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                                  (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                        (k • g) =
                      ↑(RingHom.id 𝕜) k •
                        AddHom.toFun
                          { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                            map_add' :=
                              (_ :
                                ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                                  (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                                    (fun g => ↑v (ContMDiffMap.comp g f)) g +
                                      (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                          g) }
          g' +
      g' •
        ↑{
              toAddHom :=
                { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                  map_add' :=
                    (_ :
                      ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                        (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                          (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') },
              map_smul' :=
                (_ :
                  ∀ (k : 𝕜) (g : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                    AddHom.toFun
                        { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                          map_add' :=
                            (_ :
                              ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                                (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                                  (fun g => ↑v (ContMDiffMap.comp g f)) g + (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                        (k • g) =
                      ↑(RingHom.id 𝕜) k •
                        AddHom.toFun
                          { toFun := fun g => ↑v (ContMDiffMap.comp g f),
                            map_add' :=
                              (_ :
                                ∀ (g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩),
                                  (fun g => ↑v (ContMDiffMap.comp g f)) (g + g') =
                                    (fun g => ↑v (ContMDiffMap.comp g f)) g +
                                      (fun g => ↑v (ContMDiffMap.comp g f)) g') }
                          g) }
          g
[PROOFSTEP]
dsimp
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ ↑v (ContMDiffMap.comp (g * g') f) = g • ↑v (ContMDiffMap.comp g' f) + g' • ↑v (ContMDiffMap.comp g f)
[PROOFSTEP]
rw [SmoothMap.mul_comp, Derivation.leibniz, PointedSmoothMap.smul_def, ContMDiffMap.comp_apply,
  PointedSmoothMap.smul_def, ContMDiffMap.comp_apply, h]
[GOAL]
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞
X Y : Derivation 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ g✝ : C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^⊤⟮I, M; I', M'⟯
x : M
y : M'
h : ↑f x = y
v : PointDerivation I x
g g' : C^⊤⟮I', M'; 𝕜⟯⟨y⟩
⊢ ↑g y * ↑v (ContMDiffMap.comp g' f) + ↑g' y * ↑v (ContMDiffMap.comp g f) =
    g • ↑v (ContMDiffMap.comp g' f) + g' • ↑v (ContMDiffMap.comp g f)
[PROOFSTEP]
norm_cast


[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
α : Sort u_13
h : M ≃ₘ^n⟮I, J⟯ N
f : α → M
⊢ range (↑h ∘ f) = ↑h.symm ⁻¹' range f
[PROOFSTEP]
rw [range_comp, image_eq_preimage]
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n m : ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
⊢ ContMDiffWithinAt I I' m (f ∘ ↑h) s x ↔ ContMDiffWithinAt J I' m f (↑h.symm ⁻¹' s) (↑h x)
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n m : ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
⊢ ContMDiffWithinAt I I' m (f ∘ ↑h) s x → ContMDiffWithinAt J I' m f (↑h.symm ⁻¹' s) (↑h x)
[PROOFSTEP]
intro Hfh
[GOAL]
case mp
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n m : ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
Hfh : ContMDiffWithinAt I I' m (f ∘ ↑h) s x
⊢ ContMDiffWithinAt J I' m f (↑h.symm ⁻¹' s) (↑h x)
[PROOFSTEP]
rw [← h.symm_apply_apply x] at Hfh
[GOAL]
case mp
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n m : ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
Hfh : ContMDiffWithinAt I I' m (f ∘ ↑h) s (↑h.symm (↑h x))
⊢ ContMDiffWithinAt J I' m f (↑h.symm ⁻¹' s) (↑h x)
[PROOFSTEP]
simpa only [(· ∘ ·), h.apply_symm_apply] using Hfh.comp (h x) (h.symm.contMDiffWithinAt.of_le hm) (mapsTo_preimage _ _)
[GOAL]
case mpr
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n m : ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
⊢ ContMDiffWithinAt J I' m f (↑h.symm ⁻¹' s) (↑h x) → ContMDiffWithinAt I I' m (f ∘ ↑h) s x
[PROOFSTEP]
rw [← h.image_eq_preimage]
[GOAL]
case mpr
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n m : ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
⊢ ContMDiffWithinAt J I' m f (↑h '' s) (↑h x) → ContMDiffWithinAt I I' m (f ∘ ↑h) s x
[PROOFSTEP]
exact fun hf => hf.comp x (h.contMDiffWithinAt.of_le hm) (mapsTo_image _ _)
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n m : ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
hm : m ≤ n
x✝ : M
⊢ x✝ ∈ s → ContMDiffWithinAt I I' m (f ∘ ↑h) s x✝ ↔
    ↑h.toEquiv x✝ ∈ ↑h.symm ⁻¹' s → ContMDiffWithinAt J I' m f (↑h.symm ⁻¹' s) (↑h.toEquiv x✝)
[PROOFSTEP]
simp only [hm, coe_toEquiv, h.symm_apply_apply, contMDiffWithinAt_comp_diffeomorph_iff, mem_preimage]
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n m : ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
f : M' → M
hm : m ≤ n
s : Set M'
x : M'
Hhf : ContMDiffWithinAt I' J m (↑h ∘ f) s x
⊢ ContMDiffWithinAt I' I m f s x
[PROOFSTEP]
simpa only [(· ∘ ·), h.symm_apply_apply] using (h.symm.contMDiffAt.of_le hm).comp_contMDiffWithinAt _ Hhf
[GOAL]
𝕜 : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁷ : NormedAddCommGroup E'
inst✝¹⁶ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace 𝕜 F
H : Type u_5
inst✝¹³ : TopologicalSpace H
H' : Type u_6
inst✝¹² : TopologicalSpace H'
G : Type u_7
inst✝¹¹ : TopologicalSpace G
G' : Type u_8
inst✝¹⁰ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
M' : Type u_10
inst✝⁷ : TopologicalSpace M'
inst✝⁶ : ChartedSpace H' M'
N : Type u_11
inst✝⁵ : TopologicalSpace N
inst✝⁴ : ChartedSpace G N
N' : Type u_12
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace G' N'
n : ℕ∞
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : SmoothManifoldWithCorners J N
h : M ≃ₘ^n⟮I, J⟯ N
hn : 1 ≤ n
s : Set M
hs : UniqueMDiffOn I s
⊢ UniqueMDiffOn J (↑h '' s)
[PROOFSTEP]
convert hs.uniqueMDiffOn_preimage (h.toLocalHomeomorph_mdifferentiable hn)
[GOAL]
case h.e'_12
𝕜 : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁷ : NormedAddCommGroup E'
inst✝¹⁶ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace 𝕜 F
H : Type u_5
inst✝¹³ : TopologicalSpace H
H' : Type u_6
inst✝¹² : TopologicalSpace H'
G : Type u_7
inst✝¹¹ : TopologicalSpace G
G' : Type u_8
inst✝¹⁰ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
M' : Type u_10
inst✝⁷ : TopologicalSpace M'
inst✝⁶ : ChartedSpace H' M'
N : Type u_11
inst✝⁵ : TopologicalSpace N
inst✝⁴ : ChartedSpace G N
N' : Type u_12
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace G' N'
n : ℕ∞
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : SmoothManifoldWithCorners J N
h : M ≃ₘ^n⟮I, J⟯ N
hn : 1 ≤ n
s : Set M
hs : UniqueMDiffOn I s
⊢ ↑h '' s =
    (Homeomorph.toLocalHomeomorph (toHomeomorph h)).toLocalEquiv.target ∩
      ↑(LocalHomeomorph.symm (Homeomorph.toLocalHomeomorph (toHomeomorph h))) ⁻¹' s
[PROOFSTEP]
simp [h.image_eq_preimage]
[GOAL]
𝕜 : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁷ : NormedAddCommGroup E'
inst✝¹⁶ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace 𝕜 F
H : Type u_5
inst✝¹³ : TopologicalSpace H
H' : Type u_6
inst✝¹² : TopologicalSpace H'
G : Type u_7
inst✝¹¹ : TopologicalSpace G
G' : Type u_8
inst✝¹⁰ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
M' : Type u_10
inst✝⁷ : TopologicalSpace M'
inst✝⁶ : ChartedSpace H' M'
N : Type u_11
inst✝⁵ : TopologicalSpace N
inst✝⁴ : ChartedSpace G N
N' : Type u_12
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace G' N'
n : ℕ∞
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : SmoothManifoldWithCorners J N
h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
hn : 1 ≤ n
s : Set E
⊢ UniqueDiffOn 𝕜 (↑h '' s) ↔ UniqueDiffOn 𝕜 s
[PROOFSTEP]
simp only [← uniqueMDiffOn_iff_uniqueDiffOn, uniqueMDiffOn_image, hn]
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I✝ : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
I : ModelWithCorners 𝕜 E H
e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
⊢ (I.toLocalEquiv ≫ Equiv.toLocalEquiv e.toEquiv).source = univ
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I✝ : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
I : ModelWithCorners 𝕜 E H
e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
⊢ UniqueDiffOn 𝕜 (I.toLocalEquiv ≫ Equiv.toLocalEquiv e.toEquiv).target
[PROOFSTEP]
simp [range_comp e, I.unique_diff]
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
x : M
⊢ (extChartAt (transDiffeomorph I e) x).target = ↑e.symm ⁻¹' (extChartAt I x).target
[PROOFSTEP]
simp only [e.range_comp, preimage_preimage, mfld_simps]
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
x : M
⊢ ↑e.symm ⁻¹' range ↑I ∩ ↑(ModelWithCorners.symm I) ∘ ↑e.symm ⁻¹' (chartAt H x).toLocalEquiv.target =
    ↑e.symm ⁻¹' range ↑I ∩ (fun x => ↑(ModelWithCorners.symm I) (↑e.symm x)) ⁻¹' (chartAt H x).toLocalEquiv.target
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁸ : NormedAddCommGroup E
inst✝¹⁷ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁶ : NormedAddCommGroup E'
inst✝¹⁵ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
H : Type u_5
inst✝¹² : TopologicalSpace H
H' : Type u_6
inst✝¹¹ : TopologicalSpace H'
G : Type u_7
inst✝¹⁰ : TopologicalSpace G
G' : Type u_8
inst✝⁹ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
M' : Type u_10
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
N : Type u_11
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
N' : Type u_12
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace G' N'
n : ℕ∞
e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
inst✝ : SmoothManifoldWithCorners I M
⊢ SmoothManifoldWithCorners (ModelWithCorners.transDiffeomorph I e) M
[PROOFSTEP]
refine smoothManifoldWithCorners_of_contDiffOn (I.transDiffeomorph e) M fun e₁ e₂ h₁ h₂ => ?_
[GOAL]
𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁸ : NormedAddCommGroup E
inst✝¹⁷ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁶ : NormedAddCommGroup E'
inst✝¹⁵ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
H : Type u_5
inst✝¹² : TopologicalSpace H
H' : Type u_6
inst✝¹¹ : TopologicalSpace H'
G : Type u_7
inst✝¹⁰ : TopologicalSpace G
G' : Type u_8
inst✝⁹ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
M' : Type u_10
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
N : Type u_11
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
N' : Type u_12
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace G' N'
n : ℕ∞
e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
inst✝ : SmoothManifoldWithCorners I M
e₁ e₂ : LocalHomeomorph M H
h₁ : e₁ ∈ atlas H M
h₂ : e₂ ∈ atlas H M
⊢ ContDiffOn 𝕜 ⊤
    (↑(ModelWithCorners.transDiffeomorph I e) ∘
      ↑(LocalHomeomorph.symm e₁ ≫ₕ e₂) ∘ ↑(ModelWithCorners.symm (ModelWithCorners.transDiffeomorph I e)))
    (↑(ModelWithCorners.symm (ModelWithCorners.transDiffeomorph I e)) ⁻¹'
        (LocalHomeomorph.symm e₁ ≫ₕ e₂).toLocalEquiv.source ∩
      range ↑(ModelWithCorners.transDiffeomorph I e))
[PROOFSTEP]
refine' e.contDiff.comp_contDiffOn (((contDiffGroupoid ⊤ I).compatible h₁ h₂).1.comp e.symm.contDiff.contDiffOn _)
[GOAL]
𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁸ : NormedAddCommGroup E
inst✝¹⁷ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁶ : NormedAddCommGroup E'
inst✝¹⁵ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
H : Type u_5
inst✝¹² : TopologicalSpace H
H' : Type u_6
inst✝¹¹ : TopologicalSpace H'
G : Type u_7
inst✝¹⁰ : TopologicalSpace G
G' : Type u_8
inst✝⁹ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
M' : Type u_10
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
N : Type u_11
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
N' : Type u_12
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace G' N'
n : ℕ∞
e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
inst✝ : SmoothManifoldWithCorners I M
e₁ e₂ : LocalHomeomorph M H
h₁ : e₁ ∈ atlas H M
h₂ : e₂ ∈ atlas H M
⊢ ↑(ModelWithCorners.symm (ModelWithCorners.transDiffeomorph I e)) ⁻¹'
        (LocalHomeomorph.symm e₁ ≫ₕ e₂).toLocalEquiv.source ∩
      range ↑(ModelWithCorners.transDiffeomorph I e) ⊆
    (fun x => ↑(LocalEquiv.symm (LocalEquiv.restr (Equiv.toLocalEquiv e.toEquiv) I.target)) x) ⁻¹'
      (↑(ModelWithCorners.symm I) ⁻¹' (LocalHomeomorph.symm e₁ ≫ₕ e₂).toLocalEquiv.source ∩ range ↑I)
[PROOFSTEP]
mfld_set_tac
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
⊢ ContMDiffAt I (ModelWithCorners.transDiffeomorph I e) ⊤ (↑(Equiv.refl M)) x
[PROOFSTEP]
refine' contMDiffWithinAt_iff'.2 ⟨continuousWithinAt_id, _⟩
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
⊢ ContDiffWithinAt 𝕜 ⊤
    (↑(extChartAt (ModelWithCorners.transDiffeomorph I e) (↑(Equiv.refl M) x)) ∘
      ↑(Equiv.refl M) ∘ ↑(LocalEquiv.symm (extChartAt I x)))
    ((extChartAt I x).target ∩
      ↑(LocalEquiv.symm (extChartAt I x)) ⁻¹'
        (univ ∩ ↑(Equiv.refl M) ⁻¹' (extChartAt (ModelWithCorners.transDiffeomorph I e) (↑(Equiv.refl M) x)).source))
    (↑(extChartAt I x) x)
[PROOFSTEP]
refine' e.contDiff.contDiffWithinAt.congr' (fun y hy => _) _
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
y : E
hy :
  y ∈
    (extChartAt I x).target ∩
      ↑(LocalEquiv.symm (extChartAt I x)) ⁻¹'
        (univ ∩ ↑(Equiv.refl M) ⁻¹' (extChartAt (ModelWithCorners.transDiffeomorph I e) (↑(Equiv.refl M) x)).source)
⊢ (↑(extChartAt (ModelWithCorners.transDiffeomorph I e) (↑(Equiv.refl M) x)) ∘
        ↑(Equiv.refl M) ∘ ↑(LocalEquiv.symm (extChartAt I x)))
      y =
    ↑e y
[PROOFSTEP]
simp only [Equiv.coe_refl, id, (· ∘ ·), I.coe_extChartAt_transDiffeomorph]
  -- porting note: `simp only` failed to used next lemma, converted to `rw`
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
y : E
hy :
  y ∈
    (extChartAt I x).target ∩
      ↑(LocalEquiv.symm (extChartAt I x)) ⁻¹'
        (univ ∩ ↑(Equiv.refl M) ⁻¹' (extChartAt (ModelWithCorners.transDiffeomorph I e) (↑(Equiv.refl M) x)).source)
⊢ ↑e (↑(extChartAt I x) (↑(LocalEquiv.symm (extChartAt I x)) y)) = ↑e y
[PROOFSTEP]
rw [(extChartAt I x).right_inv hy.1]
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
⊢ ↑(extChartAt I x) x ∈
    (extChartAt I x).target ∩
      ↑(LocalEquiv.symm (extChartAt I x)) ⁻¹'
        (univ ∩ ↑(Equiv.refl M) ⁻¹' (extChartAt (ModelWithCorners.transDiffeomorph I e) (↑(Equiv.refl M) x)).source)
[PROOFSTEP]
exact ⟨(extChartAt I x).map_source (mem_extChartAt_source I x), trivial, by simp only [mfld_simps]⟩
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
⊢ ↑(LocalEquiv.symm (extChartAt I x)) (↑(extChartAt I x) x) ∈
    ↑(Equiv.refl M) ⁻¹' (extChartAt (ModelWithCorners.transDiffeomorph I e) (↑(Equiv.refl M) x)).source
[PROOFSTEP]
simp only [mfld_simps]
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
⊢ ContMDiffAt (ModelWithCorners.transDiffeomorph I e) I ⊤ (↑(Equiv.refl M).symm) x
[PROOFSTEP]
refine' contMDiffWithinAt_iff'.2 ⟨continuousWithinAt_id, _⟩
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
⊢ ContDiffWithinAt 𝕜 ⊤
    (↑(extChartAt I (↑(Equiv.refl M).symm x)) ∘
      ↑(Equiv.refl M).symm ∘ ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.transDiffeomorph I e) x)))
    ((extChartAt (ModelWithCorners.transDiffeomorph I e) x).target ∩
      ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.transDiffeomorph I e) x)) ⁻¹'
        (univ ∩ ↑(Equiv.refl M).symm ⁻¹' (extChartAt I (↑(Equiv.refl M).symm x)).source))
    (↑(extChartAt (ModelWithCorners.transDiffeomorph I e) x) x)
[PROOFSTEP]
refine' e.symm.contDiff.contDiffWithinAt.congr' (fun y hy => _) _
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
y : F
hy :
  y ∈
    (extChartAt (ModelWithCorners.transDiffeomorph I e) x).target ∩
      ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.transDiffeomorph I e) x)) ⁻¹'
        (univ ∩ ↑(Equiv.refl M).symm ⁻¹' (extChartAt I (↑(Equiv.refl M).symm x)).source)
⊢ (↑(extChartAt I (↑(Equiv.refl M).symm x)) ∘
        ↑(Equiv.refl M).symm ∘ ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.transDiffeomorph I e) x)))
      y =
    ↑e.symm y
[PROOFSTEP]
simp only [mem_inter_iff, I.extChartAt_transDiffeomorph_target] at hy
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
y : F
hy :
  y ∈ ↑e.symm ⁻¹' (extChartAt I x).target ∧
    y ∈
      ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.transDiffeomorph I e) x)) ⁻¹'
        (univ ∩ ↑(Equiv.refl M).symm ⁻¹' (extChartAt I (↑(Equiv.refl M).symm x)).source)
⊢ (↑(extChartAt I (↑(Equiv.refl M).symm x)) ∘
        ↑(Equiv.refl M).symm ∘ ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.transDiffeomorph I e) x)))
      y =
    ↑e.symm y
[PROOFSTEP]
simp only [Equiv.coe_refl, Equiv.refl_symm, id, (· ∘ ·), I.coe_extChartAt_transDiffeomorph_symm,
  (extChartAt I x).right_inv hy.1]
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
⊢ ↑(extChartAt (ModelWithCorners.transDiffeomorph I e) x) x ∈
    (extChartAt (ModelWithCorners.transDiffeomorph I e) x).target ∩
      ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.transDiffeomorph I e) x)) ⁻¹'
        (univ ∩ ↑(Equiv.refl M).symm ⁻¹' (extChartAt I (↑(Equiv.refl M).symm x)).source)
[PROOFSTEP]
exact
  ⟨(extChartAt _ x).map_source (mem_extChartAt_source _ x), trivial, by
    simp only [e.symm_apply_apply, Equiv.refl_symm, Equiv.coe_refl, mfld_simps]⟩
[GOAL]
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁵ : NormedAddCommGroup E'
inst✝¹⁴ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹¹ : TopologicalSpace H
H' : Type u_6
inst✝¹⁰ : TopologicalSpace H'
G : Type u_7
inst✝⁹ : TopologicalSpace G
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_10
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
N : Type u_11
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞
e✝ e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
x : M
⊢ ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.transDiffeomorph I e) x))
      (↑(extChartAt (ModelWithCorners.transDiffeomorph I e) x) x) ∈
    ↑(Equiv.refl M).symm ⁻¹' (extChartAt I (↑(Equiv.refl M).symm x)).source
[PROOFSTEP]
simp only [e.symm_apply_apply, Equiv.refl_symm, Equiv.coe_refl, mfld_simps]


[GOAL]
z : ℂ
⊢ ↑(leftMulMatrix basisOneI) z = ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
z : ℂ
i j : Fin 2
⊢ ↑(leftMulMatrix basisOneI) z i j = ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] i j
[PROOFSTEP]
rw [Algebra.leftMulMatrix_eq_repr_mul, Complex.coe_basisOneI_repr, Complex.coe_basisOneI, mul_re, mul_im,
  Matrix.of_apply]
[GOAL]
case a.h
z : ℂ
i j : Fin 2
⊢ Matrix.vecCons (z.re * (Matrix.vecCons 1 ![I] j).re - z.im * (Matrix.vecCons 1 ![I] j).im)
      ![z.re * (Matrix.vecCons 1 ![I] j).im + z.im * (Matrix.vecCons 1 ![I] j).re] i =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] i j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head
z : ℂ
i : Fin 2
⊢ Matrix.vecCons
      (z.re * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).re -
        z.im * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).im)
      ![z.re * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).im +
          z.im * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).re]
      i =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] i { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp only [Fin.mk_zero, Matrix.cons_val_zero, one_re, mul_one, one_im, mul_zero, sub_zero, zero_add]
[GOAL]
case a.h.head
z : ℂ
i : Fin 2
⊢ Matrix.vecCons z.re ![z.im] i = Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] i 0
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head.head
z : ℂ
⊢ Matrix.vecCons z.re ![z.im] { val := 0, isLt := (_ : 0 < 2) } =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] { val := 0, isLt := (_ : 0 < 2) } 0
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.head
z : ℂ
⊢ Matrix.vecCons z.re ![z.im] { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } 0
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head
z : ℂ
i : Fin 2
⊢ Matrix.vecCons
      (z.re * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).re -
        z.im * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).im)
      ![z.re * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).im +
          z.im * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).re]
      i =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] i { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp only [Fin.mk_one, Matrix.cons_val_one, Matrix.head_cons, I_re, mul_zero, I_im, mul_one, zero_sub, add_zero]
[GOAL]
case a.h.tail.head
z : ℂ
i : Fin 2
⊢ Matrix.vecCons (-z.im) ![z.re] i = Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] i 1
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.tail.head.head
z : ℂ
⊢ Matrix.vecCons (-z.im) ![z.re] { val := 0, isLt := (_ : 0 < 2) } =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] { val := 0, isLt := (_ : 0 < 2) } 1
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.head
z : ℂ
⊢ Matrix.vecCons (-z.im) ![z.re] { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    Matrix.vecCons ![z.re, -z.im] ![![z.im, z.re]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1
[PROOFSTEP]
rfl
[GOAL]
z : ℂ
⊢ ↑(trace ℝ ℂ) z = 2 * z.re
[PROOFSTEP]
rw [Algebra.trace_eq_matrix_trace Complex.basisOneI, Algebra.leftMulMatrix_complex, Matrix.trace_fin_two]
[GOAL]
z : ℂ
⊢ ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 0 0 + ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 1 1 = 2 * z.re
[PROOFSTEP]
exact (two_mul _).symm
[GOAL]
z : ℂ
⊢ ↑(norm ℝ) z = ↑normSq z
[PROOFSTEP]
rw [Algebra.norm_eq_matrix_det Complex.basisOneI, Algebra.leftMulMatrix_complex, Matrix.det_fin_two, normSq_apply]
[GOAL]
z : ℂ
⊢ ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 0 0 * ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 1 1 -
      ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 0 1 * ↑Matrix.of ![![z.re, -z.im], ![z.im, z.re]] 1 0 =
    z.re * z.re + z.im * z.im
[PROOFSTEP]
simp