B : Type u_1
E : B → Type u_2
x : B
b : E x
⊢ totalSpaceMk x (cast (_ : E x = E x) b) = totalSpaceMk x b
B : Type u_1
E : B → Type u_2
x x' : B
h : x = x'
b : E x
⊢ totalSpaceMk x' (cast (_ : E x = E x') b) = totalSpaceMk x b
subst h
no goals
B : Type u_1
E : B → Type u_2
x : B
b : E x
⊢ totalSpaceMk x (cast (_ : E x = E x) b) = totalSpaceMk x b
rfl