[GOAL]
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (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)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
⊢ ∀ (e e' : Trivialization F TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'],
    SmoothOn IB' 𝓘(𝕜, F →L[𝕜] F) (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)
[PROOFSTEP]
rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩
[GOAL]
case mk.intro.intro.mk.intro.intro
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (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)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
⊢ SmoothOn IB' 𝓘(𝕜, F →L[𝕜] F)
    (fun b => ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b))
    ((Trivialization.pullback e f).baseSet ∩ (Trivialization.pullback e' f).baseSet)
[PROOFSTEP]
skip
[GOAL]
case mk.intro.intro.mk.intro.intro
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (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)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
⊢ SmoothOn IB' 𝓘(𝕜, F →L[𝕜] F)
    (fun b => ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b))
    ((Trivialization.pullback e f).baseSet ∩ (Trivialization.pullback e' f).baseSet)
[PROOFSTEP]
refine' ((smoothOn_coordChangeL _ e e').comp f.smooth.smoothOn fun b hb => hb).congr _
[GOAL]
case mk.intro.intro.mk.intro.intro
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (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)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
⊢ ∀ (y : B'),
    y ∈ ↑f ⁻¹' (e.baseSet ∩ e'.baseSet) →
      ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) y) =
        ((fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ↑f) y
[PROOFSTEP]
rintro b (hb : f b ∈ e.baseSet ∩ e'.baseSet)
[GOAL]
case mk.intro.intro.mk.intro.intro
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (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)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
⊢ ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b) =
    ((fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ↑f) b
[PROOFSTEP]
ext v
[GOAL]
case mk.intro.intro.mk.intro.intro.h
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (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)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ↑↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b) v =
    ↑(((fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ↑f) b) v
[PROOFSTEP]
show ((e.pullback f).coordChangeL 𝕜 (e'.pullback f) b) v = (e.coordChangeL 𝕜 e' (f b)) v
[GOAL]
case mk.intro.intro.mk.intro.intro.h
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (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)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b) v =
    ↑(Trivialization.coordChangeL 𝕜 e e' (↑f b)) v
[PROOFSTEP]
rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]
[GOAL]
case mk.intro.intro.mk.intro.intro.h
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (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)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (↑(Trivialization.pullback e' f)
        (↑(LocalHomeomorph.symm (Trivialization.pullback e f).toLocalHomeomorph) (b, v))).snd =
    (↑e' { proj := ↑f b, snd := Trivialization.symm e (↑f b) v }).snd
case mk.intro.intro.mk.intro.intro.h.hb
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (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)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ b ∈ (Trivialization.pullback e f).baseSet ∩ (Trivialization.pullback e' f).baseSet
[PROOFSTEP]
exacts [rfl, hb]
