/home/lean/actions-runner/_work/mathlib/mathlib/src/topology/vector_bundle/alternating.lean:99:22: type mismatch at application total_space E₁ term E₁ has type B → Type u_5 : Type (max u_3 (u_5+1)) but is expected to have type Type ? : Type (?+1) Additional information: /home/lean/actions-runner/_work/mathlib/mathlib/src/topology/vector_bundle/alternating.lean:99:22: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message type mismatch, term total_space ?m_2 has type (?m_1 → Type ?) → Type (max ? ?) : Type (max (max ? (?+1)) (?+1) (?+1)) but is expected to have type Type ? : Type (?+1)

Process completed with exit code 1.