exact And.left <| h.covBy_and_covBy_of_covBy_of_ssubset_of_ssubset hH₁.covBy hH₂.flat
  (hH₁.inter_ssubset_right_of_ne hH₂ hne) hH₂.ssubset_ground
case inr.refine_1
α : 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 : α
hH₁ : M.Hyperplane H₁
hH₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
h : H₁ ∩ H₂ ⋖[M] H₁
⊢ H₁ ∩ H₂ ⋖[M] H₂
no goals