no goals
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 : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
y : E b
⊢ ↑(Trivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e (totalSpaceMk b y)).snd else 0
rw [coe_linearMapAt]