ι : Type ?u.53743
B : Type u_1
F : Type u_2
E : B → Type ?u.53754
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x✝ : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, coordChange e₁ e₂ b x).fst = (↑e₂ (↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x))).fst
ι : Type ?u.53743
B : Type u_1
F : Type u_2
E : B → Type ?u.53754
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x✝ : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, coordChange e₁ e₂ b x) = ↑e₂ (↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x))
refine' Prod.ext _ rfl
ι : Type ?u.53743
B : Type u_1
F : Type u_2
E : B → Type ?u.53754
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x✝ : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x)) ∈ e₁.baseSet

ι : Type ?u.53743
B : Type u_1
F : Type u_2
E : B → Type ?u.53754
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x✝ : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x)) ∈ e₂.baseSet
ι : Type ?u.53743
B : Type u_1
F : Type u_2
E : B → Type ?u.53754
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x✝ : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, coordChange e₁ e₂ b x).fst = (↑e₂ (↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x))).fst
rw [e₂.coe_fst', ← e₁.coe_fst', e₁.apply_symm_apply' h₁]
no goals
ι : Type ?u.53743
B : Type u_1
F : Type u_2
E : B → Type ?u.53754
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x✝ : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x)) ∈ e₁.baseSet
rwa [e₁.proj_symm_apply' h₁]
no goals
ι : Type ?u.53743
B : Type u_1
F : Type u_2
E : B → Type ?u.53754
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x✝ : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x)) ∈ e₂.baseSet
rwa [e₁.proj_symm_apply' h₁]