Theorem: Matroid.comap_dep_iff (Matroid/Map.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
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]
State after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
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

State before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
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⟩ ↦ ?_, ?_⟩
State after:
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_2
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
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

State before:
case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
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)
State after:
case refine_2.inl.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
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 : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

State before:
case refine_2.inr
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
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]
State after:
case refine_2.inr
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ I ⊆ f ⁻¹' N.E

State before:
case refine_2.inr
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ I ⊆ f ⁻¹' N.E
Tactic:
simpa using hI.1.subset_ground
State after:
no goals

State before:
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
Tactic:
rw [and_iff_left h, ← imp_iff_not_or]
State after:
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

State before:
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
Tactic:
exact fun hI ↦ ⟨hI, hi hI⟩
State after:
no goals

State before:
case refine_2.inl.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
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⟩
State after:
no goals