Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops (Matroid/Loop.lean)

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
⊢ M₁ = M₂
Tactic:
refine' eq_of_indep_iff_indep_forall hE fun I hI ↦ _
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
Tactic:
rw [indep_iff_diff_coloops_indep, @indep_iff_diff_coloops_indep _ M₂, ← hc]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
obtain hdj | hndj := em (Disjoint I (M₁.cl ∅))
State after:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)

case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)

State before:
case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
obtain ⟨e, heI, hel : M₁.Loop e⟩ := not_disjoint_iff_nonempty_inter.mp hndj
State after:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₁.Loop e
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)

State before:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₁.Loop e
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
refine' iff_of_false (hel.not_indep_of_mem ⟨heI, hel.not_coloop⟩) _
State after:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₁.Loop e
⊢ ¬M₂.Indep (I \ M₁✶.cl ∅)

State before:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₁.Loop e
⊢ ¬M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
rw [loop_iff_mem_cl_empty, hl, ← loop_iff_mem_cl_empty] at hel
State after:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₂.Loop e
⊢ ¬M₂.Indep (I \ M₁✶.cl ∅)

State before:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₂.Loop e
⊢ ¬M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
rw [hc]
State after:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₂.Loop e
⊢ ¬M₂.Indep (I \ M₂✶.cl ∅)

State before:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₂.Loop e
⊢ ¬M₂.Indep (I \ M₂✶.cl ∅)
Tactic:
exact hel.not_indep_of_mem ⟨heI, hel.not_coloop⟩
State after:
no goals

State before:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
rw [h _ (diff_subset.trans hI)]
State after:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ Disjoint (I \ M₁✶.cl ∅) (M₁.cl ∅ ∪ M₁✶.cl ∅)

State before:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ Disjoint (I \ M₁✶.cl ∅) (M₁.cl ∅ ∪ M₁✶.cl ∅)
Tactic:
rw [disjoint_union_right]
State after:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ Disjoint (I \ M₁✶.cl ∅) (M₁.cl ∅) ∧ Disjoint (I \ M₁✶.cl ∅) (M₁✶.cl ∅)

State before:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ Disjoint (I \ M₁✶.cl ∅) (M₁.cl ∅) ∧ Disjoint (I \ M₁✶.cl ∅) (M₁✶.cl ∅)
Tactic:
exact ⟨disjoint_of_subset_left diff_subset hdj, disjoint_sdiff_left⟩
State after:
no goals