norm_cast at h
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : ⊤ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h' : M.relRank F F₁ = ⊤
⊢ False
no goals