case h₁
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace E
b✝ : B
y✝ : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ (b, ↑(coordChangeL R e e' b) y).fst = (↑e' (totalSpaceMk b (Trivialization.symm e b y))).fst

case h₂
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace E
b✝ : B
y✝ : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ (b, ↑(coordChangeL R e e' b) y).snd = (↑e' (totalSpaceMk b (Trivialization.symm e b y))).snd
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace E
b✝ : B
y✝ : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ (b, ↑(coordChangeL R e e' b) y) = ↑e' (totalSpaceMk b (Trivialization.symm e b y))
ext
case h₁
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace E
b✝ : B
y✝ : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ TotalSpace.proj (↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, y)) ∈ e'.baseSet
case h₁
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace E
b✝ : B
y✝ : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ (b, ↑(coordChangeL R e e' b) y).fst = (↑e' (totalSpaceMk b (Trivialization.symm e b y))).fst
rw [e.mk_symm hb.1 y, e'.coe_fst', e.proj_symm_apply' hb.1]
case h₁
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace E
b✝ : B
y✝ : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ b ∈ e'.baseSet
case h₁
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace E
b✝ : B
y✝ : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ TotalSpace.proj (↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, y)) ∈ e'.baseSet
rw [e.proj_symm_apply' hb.1]
no goals
case h₁
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace E
b✝ : B
y✝ : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ b ∈ e'.baseSet
exact hb.2
no goals
case h₂
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace E
b✝ : B
y✝ : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ (b, ↑(coordChangeL R e e' b) y).snd = (↑e' (totalSpaceMk b (Trivialization.symm e b y))).snd
exact e.coordChangeL_apply e' hb y