Theorem: Matroid.eq_addLoop_iff (Matroid/Constructions/ParallelExtension.lean)

State before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M
Tactic:
obtain (he' | he') := em' (e ∈ M'.E)
State after:
case inl
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M

case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M

State before:
case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M
Tactic:
simp_rw [deleteElem, eq_iff_indep_iff_indep_forall, addLoop_ground, addLoop_indep_iff,
  delete_ground, delete_indep_iff, disjoint_singleton_right, ← singleton_dep, dep_iff,
  singleton_subset_iff, and_iff_left he', subset_diff, disjoint_singleton_right, and_imp]
State after:
case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ (M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I) ↔
    ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)

State before:
case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ (M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I) ↔
    ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
Tactic:
refine ⟨fun ⟨hE, hi⟩ ↦ ⟨?_, ?_, ?_⟩, fun ⟨hi, hE, h⟩ ↦ ⟨?_, fun I hIss ↦ ?_⟩⟩
State after:
case inr.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ¬M'.Indep {e}

case inr.refine_2
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ M'.E \ {e} = M.E

case inr.refine_3
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)

case inr.refine_4
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
⊢ M'.E = insert e M.E

case inr.refine_5
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
⊢ M'.Indep I ↔ M.Indep I

State before:
case inr.refine_5
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
⊢ M'.Indep I ↔ M.Indep I
Tactic:
obtain (heI | heI) := em (e ∈ I)
State after:
case inr.refine_5.inl
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
heI : e ∈ I
⊢ M'.Indep I ↔ M.Indep I

case inr.refine_5.inr
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
⊢ M'.Indep I ↔ M.Indep I

State before:
case inr.refine_5.inr
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
⊢ M'.Indep I ↔ M.Indep I
Tactic:
specialize h I hIss
State after:
case inr.refine_5.inr
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
h : e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
⊢ M'.Indep I ↔ M.Indep I

State before:
case inr.refine_5.inr
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
h : e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
⊢ M'.Indep I ↔ M.Indep I
Tactic:
simpa [heI] using h
State after:
no goals

State before:
case inl
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M
Tactic:
refine iff_of_false ?_ ?_
State after:
case inl.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ ¬M' = M.addLoop e

case inl.refine_2
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ ¬(M'.Loop e ∧ M' ＼ e = M)

State before:
case inl.refine_2
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ ¬(M'.Loop e ∧ M' ＼ e = M)
Tactic:
rintro ⟨h, rfl⟩
State after:
case inl.refine_2.intro
α : Type u_1
M' : Matroid α
e f : α
I : Set α
he' : e ∉ M'.E
h : M'.Loop e
he : e ∉ (M' ＼ e).E
⊢ False

State before:
case inl.refine_2.intro
α : Type u_1
M' : Matroid α
e f : α
I : Set α
he' : e ∉ M'.E
h : M'.Loop e
he : e ∉ (M' ＼ e).E
⊢ False
Tactic:
exact he' h.mem_ground
State after:
no goals

State before:
case inl.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ ¬M' = M.addLoop e
Tactic:
rintro rfl
State after:
case inl.refine_1
α : Type u_1
M : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ (M.addLoop e).E
⊢ False

State before:
case inl.refine_1
α : Type u_1
M : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ (M.addLoop e).E
⊢ False
Tactic:
simp at he'
State after:
no goals

State before:
case inr.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ¬M'.Indep {e}
Tactic:
rw [hi _ (singleton_subset_iff.2 he')]
State after:
case inr.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ¬M.Indep {e}

State before:
case inr.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ¬M.Indep {e}
Tactic:
exact fun hei ↦ he (singleton_subset_iff.1 hei.subset_ground)
State after:
no goals

State before:
case inr.refine_2
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ M'.E \ {e} = M.E
Tactic:
simp [hE, he]
State after:
no goals

State before:
case inr.refine_3
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
Tactic:
rintro I hIss heI
State after:
case inr.refine_3
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
⊢ M'.Indep I ∧ e ∉ I ↔ M.Indep I

State before:
case inr.refine_3
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
⊢ M'.Indep I ∧ e ∉ I ↔ M.Indep I
Tactic:
rw [and_iff_left heI, hi _ hIss]
State after:
no goals

State before:
case inr.refine_4
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
⊢ M'.E = insert e M.E
Tactic:
rw [← hE, insert_diff_singleton, insert_eq_of_mem he']
State after:
no goals

State before:
case inr.refine_5.inl
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
heI : e ∈ I
⊢ M'.Indep I ↔ M.Indep I
Tactic:
exact iff_of_false (fun hI ↦ hi <| hI.subset (singleton_subset_iff.2 heI))
  (fun hI ↦ he <| hI.subset_ground heI)
State after:
no goals