-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma comap_dep_iff :
    (N.comap f).Dep I ↔ N.Dep (f '' I) ∨ (N.Indep (f '' I) ∧ ¬ InjOn f I)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I → (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

Tactic:
rintro (⟨hI, hIE⟩ | hI)

Result:
case refine_2.inl.intro
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : ¬N.Indep (f '' I)
hIE : I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

case refine_2.inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

Proof state:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
I : Set α
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

Tactic:
rw [and_iff_left h, ← imp_iff_not_or]

Result:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
I : Set α
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

Proof state:
case refine_2.inl.intro
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : ¬N.Indep (f '' I)
hIE : I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

Tactic:
exact ⟨fun h ↦ (hI h).elim, hIE⟩

Result:
no goals

Proof state:
case refine_2.inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

Tactic:
rw [iff_true_intro hI.1, iff_true_intro hI.2, implies_true, true_and]

Result:
case refine_2.inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ I ⊆ f ⁻¹' N.E

Proof state:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
I : Set α
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

Tactic:
exact fun hI ↦ ⟨hI, hi hI⟩

Result:
no goals

Proof state:
case refine_2.inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ I ⊆ f ⁻¹' N.E

Tactic:
simpa using hI.1.subset_ground

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E ↔ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I

Tactic:
refine ⟨fun ⟨hi, h⟩ ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
I : Set α
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_2
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I → (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

Proof state:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ (N.comap f).Dep I ↔ N.Dep (f '' I) ∨ N.Indep (f '' I) ∧ ¬InjOn f I

Tactic:
rw [Dep, comap_indep_iff, not_and, comap_ground_eq, Dep, image_subset_iff]

Result:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E ↔ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I