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

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : ¬M.Nonloop e
f : α
⊢ M.parallelExtend e f = (M ＼ f).addLoop f
Tactic:
simp only [parallelExtend, deleteElem, eq_iff_indep_iff_indep_forall, restrict_ground_eq,
  addLoop_ground, delete_ground, mem_diff, mem_singleton_iff, not_true_eq_false, and_false,
  insert_diff_singleton, restrict_indep_iff, comap_indep_iff, ne_eq, image_update, id_eq,
  image_id', update_id_injOn_iff, addLoop_indep_iff, delete_indep_iff, disjoint_singleton_right,
  true_and]
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : ¬M.Nonloop e
f : α
⊢ ∀ I ⊆ insert f M.E,
    (M.Indep (if f ∈ I then insert e (I \ {f}) else I) ∧ (f ∈ I → e ∈ I → f = e)) ∧ I ⊆ insert f M.E ↔ M.Indep I ∧ f ∉ I

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : ¬M.Nonloop e
f : α
⊢ ∀ I ⊆ insert f M.E,
    (M.Indep (if f ∈ I then insert e (I \ {f}) else I) ∧ (f ∈ I → e ∈ I → f = e)) ∧ I ⊆ insert f M.E ↔ M.Indep I ∧ f ∉ I
Tactic:
rintro I hI
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I✝ C : Set α
he : ¬M.Nonloop e
f : α
I : Set α
hI : I ⊆ insert f M.E
⊢ (M.Indep (if f ∈ I then insert e (I \ {f}) else I) ∧ (f ∈ I → e ∈ I → f = e)) ∧ I ⊆ insert f M.E ↔ M.Indep I ∧ f ∉ I

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I✝ C : Set α
he : ¬M.Nonloop e
f : α
I : Set α
hI : I ⊆ insert f M.E
⊢ (M.Indep (if f ∈ I then insert e (I \ {f}) else I) ∧ (f ∈ I → e ∈ I → f = e)) ∧ I ⊆ insert f M.E ↔ M.Indep I ∧ f ∉ I
Tactic:
split_ifs with hf
State after:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I✝ C : Set α
he : ¬M.Nonloop e
f : α
I : Set α
hI : I ⊆ insert f M.E
hf : f ∈ I
⊢ (M.Indep (insert e (I \ {f})) ∧ (f ∈ I → e ∈ I → f = e)) ∧ I ⊆ insert f M.E ↔ M.Indep I ∧ f ∉ I

case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I✝ C : Set α
he : ¬M.Nonloop e
f : α
I : Set α
hI : I ⊆ insert f M.E
hf : f ∉ I
⊢ (M.Indep I ∧ (f ∈ I → e ∈ I → f = e)) ∧ I ⊆ insert f M.E ↔ M.Indep I ∧ f ∉ I

State before:
case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I✝ C : Set α
he : ¬M.Nonloop e
f : α
I : Set α
hI : I ⊆ insert f M.E
hf : f ∉ I
⊢ (M.Indep I ∧ (f ∈ I → e ∈ I → f = e)) ∧ I ⊆ insert f M.E ↔ M.Indep I ∧ f ∉ I
Tactic:
simp [hf, hI]
State after:
no goals

State before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I✝ C : Set α
he : ¬M.Nonloop e
f : α
I : Set α
hI : I ⊆ insert f M.E
hf : f ∈ I
⊢ (M.Indep (insert e (I \ {f})) ∧ (f ∈ I → e ∈ I → f = e)) ∧ I ⊆ insert f M.E ↔ M.Indep I ∧ f ∉ I
Tactic:
simp [(show ¬ M.Indep (insert e _) from fun hi ↦ he <| hi.nonloop_of_mem (mem_insert _ _)), hf]
State after:
no goals