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

State before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
⊢ (N.comap f).Basis I X ↔ N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
State after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
⊢ N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I

case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
⊢ (N.comap f).Basis I X

State before:
case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
⊢ (N.comap f).Basis I X
Tactic:
refine Indep.basis_of_forall_insert ?_ h.2.1 fun e ⟨heX, heI⟩ ↦ ?_
State after:
case refine_2.refine_1
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
⊢ (N.comap f).Indep I

case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ (N.comap f).Dep (insert e I)

State before:
case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ (N.comap f).Dep (insert e I)
Tactic:
have hIE : insert e I ⊆ (N.comap f).E := by
    simp_rw [comap_ground_eq, ← image_subset_iff]
    exact (image_subset _ (insert_subset heX h.2.1)).trans h.1.subset_ground
State after:
case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ (N.comap f).Dep (insert e I)

State before:
case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ (N.comap f).Dep (insert e I)
Tactic:
suffices N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
  by simpa [← not_indep_iff hIE, injOn_insert heI, h.2.2, image_insert_eq]
State after:
case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e

State before:
case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
Tactic:
exact h.1.mem_of_insert_indep (mem_image_of_mem f heX)
State after:
no goals

State before:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
⊢ N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
Tactic:
obtain ⟨hI, hinj⟩ := comap_indep_iff.1 h.indep
State after:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
⊢ N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I

State before:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
⊢ N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
Tactic:
refine ⟨hI.basis_of_forall_insert (image_subset f h.subset) fun e he ↦ ?_, h.subset, hinj⟩
State after:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : e ∈ f '' X \ f '' I
⊢ N.Dep (insert e (f '' I))

State before:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : e ∈ f '' X \ f '' I
⊢ N.Dep (insert e (f '' I))
Tactic:
simp only [mem_diff, mem_image, not_exists, not_and, and_imp, forall_exists_index,
  forall_apply_eq_imp_iff₂] at he
State after:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : (∃ x ∈ X, f x = e) ∧ ∀ x ∈ I, ¬f x = e
⊢ N.Dep (insert e (f '' I))

State before:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : (∃ x ∈ X, f x = e) ∧ ∀ x ∈ I, ¬f x = e
⊢ N.Dep (insert e (f '' I))
Tactic:
obtain ⟨⟨e, heX, rfl⟩, he⟩ := he
State after:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
⊢ N.Dep (insert (f e) (f '' I))

State before:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
⊢ N.Dep (insert (f e) (f '' I))
Tactic:
have heI : e ∉ I := fun heI ↦ (he e heI rfl)
State after:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
⊢ N.Dep (insert (f e) (f '' I))

State before:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
⊢ N.Dep (insert (f e) (f '' I))
Tactic:
replace h := h.insert_dep ⟨heX, heI⟩
State after:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
h : (N.comap f).Dep (insert e I)
⊢ N.Dep (insert (f e) (f '' I))

State before:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
h : (N.comap f).Dep (insert e I)
⊢ N.Dep (insert (f e) (f '' I))
Tactic:
simp only [comap_dep_iff, image_insert_eq, or_iff_not_imp_right, injOn_insert heI,
  hinj, mem_image, not_exists, not_and, true_and, not_forall, Classical.not_imp, not_not] at h
State after:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
h : (N.Indep (insert (f e) (f '' I)) → ∀ x ∈ I, ¬f x = f e) → N.Dep (insert (f e) (f '' I))
⊢ N.Dep (insert (f e) (f '' I))

State before:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
h : (N.Indep (insert (f e) (f '' I)) → ∀ x ∈ I, ¬f x = f e) → N.Dep (insert (f e) (f '' I))
⊢ N.Dep (insert (f e) (f '' I))
Tactic:
exact h (fun _ ↦ he)
State after:
no goals

State before:
case refine_2.refine_1
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
⊢ (N.comap f).Indep I
Tactic:
simp [comap_indep_iff, h.1.indep, h.2]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ insert e I ⊆ (N.comap f).E
Tactic:
simp_rw [comap_ground_eq, ← image_subset_iff]
State after:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ f '' insert e I ⊆ N.E

State before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ f '' insert e I ⊆ N.E
Tactic:
exact (image_subset _ (insert_subset heX h.2.1)).trans h.1.subset_ground
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
this : N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
⊢ (N.comap f).Dep (insert e I)
Tactic:
simpa [← not_indep_iff hIE, injOn_insert heI, h.2.2, image_insert_eq]
State after:
no goals