case h
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
z : F
⊢ (b, z) ∈ e.target

R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
z : F
h : (b, z) ∈ e.target
⊢ ↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, z) =
    totalSpaceMk b (↑(ContinuousLinearEquiv.symm (continuousLinearEquivAt R e b hb)) z)
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
z : F
⊢ ↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, z) =
    totalSpaceMk b (↑(ContinuousLinearEquiv.symm (continuousLinearEquivAt R e b hb)) z)
have h : (b, z) ∈ e.target
case a
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
z : F
h : (b, z) ∈ e.target
⊢ totalSpaceMk b (↑(ContinuousLinearEquiv.symm (continuousLinearEquivAt R e b hb)) z) ∈ e.source

case a
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
z : F
h : (b, z) ∈ e.target
⊢ ↑e.toLocalHomeomorph (↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, z)) =
    ↑e.toLocalHomeomorph (totalSpaceMk b (↑(ContinuousLinearEquiv.symm (continuousLinearEquivAt R e b hb)) z))
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
z : F
h : (b, z) ∈ e.target
⊢ ↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, z) =
    totalSpaceMk b (↑(ContinuousLinearEquiv.symm (continuousLinearEquivAt R e b hb)) z)
apply e.injOn (e.map_target h)
case h
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
z : F
⊢ (b, z) ∈ e.baseSet ×ˢ univ
case h
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
z : F
⊢ (b, z) ∈ e.target
rw [e.target_eq]
no goals
case h
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
z : F
⊢ (b, z) ∈ e.baseSet ×ˢ univ
exact ⟨hb, mem_univ _⟩
no goals
case a
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
z : F
h : (b, z) ∈ e.target
⊢ totalSpaceMk b (↑(ContinuousLinearEquiv.symm (continuousLinearEquivAt R e b hb)) z) ∈ e.source
simpa only [e.source_eq, mem_preimage]
no goals
case a
R : Type u_4
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
z : F
h : (b, z) ∈ e.target
⊢ ↑e.toLocalHomeomorph (↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, z)) =
    ↑e.toLocalHomeomorph (totalSpaceMk b (↑(ContinuousLinearEquiv.symm (continuousLinearEquivAt R e b hb)) z))
simp_rw [e.right_inv h, coe_coe, e.apply_eq_prod_continuousLinearEquivAt R b hb,
  ContinuousLinearEquiv.apply_symm_apply]