rw [and_iff_left h, ← imp_iff_not_or]
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
x✝ : (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
hi : N.Indep (f '' I) → ¬InjOn f I
h : I ⊆ f ⁻¹' N.E
⊢ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
x✝ : (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
hi : N.Indep (f '' I) → ¬InjOn f I
h : I ⊆ f ⁻¹' N.E
⊢ N.Indep (f '' I) → N.Indep (f '' I) ∧ ¬InjOn f I