Theorem: Matroid.parallelExtend_delete_eq' (Matroid/Constructions/ParallelExtension.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
⊢ M.parallelExtend e f ＼ f = M ＼ f
Tactic:
classical
simp only [parallelExtend, deleteElem, eq_iff_indep_iff_indep_forall, delete_ground,
  restrict_ground_eq, mem_insert_iff, true_or, not_true_eq_false, mem_singleton_iff,
  insert_diff_of_mem, subset_diff, disjoint_singleton_right, delete_indep_iff, restrict_indep_iff,
  comap_indep_iff, ne_eq, image_update, id_eq, image_id', mem_diff, update_id_injOn_iff,
  and_congr_left_iff, and_imp, true_and]
rintro I - hf -
simp only [hf, not_false_eq_true, diff_singleton_eq_self, ite_false, IsEmpty.forall_iff, and_true,
  and_iff_left_iff_imp]
exact fun hI ↦ hI.subset_ground.trans <| subset_insert _ _
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
⊢ M.parallelExtend e f ＼ f = M ＼ f
Tactic:
simp only [parallelExtend, deleteElem, eq_iff_indep_iff_indep_forall, delete_ground,
  restrict_ground_eq, mem_insert_iff, true_or, not_true_eq_false, mem_singleton_iff,
  insert_diff_of_mem, subset_diff, disjoint_singleton_right, delete_indep_iff, restrict_indep_iff,
  comap_indep_iff, ne_eq, image_update, id_eq, image_id', mem_diff, update_id_injOn_iff,
  and_congr_left_iff, and_imp, true_and]
State after:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
⊢ ∀ I ⊆ M.E,
    f ∉ I →
      f ∉ I →
        ((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)

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
⊢ ∀ I ⊆ M.E,
    f ∉ I →
      f ∉ I →
        ((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)
Tactic:
rintro I - hf -
State after:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I✝ C : Set α
M : Matroid α
e f : α
I : Set α
hf : f ∉ I
⊢ (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

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I✝ C : Set α
M : Matroid α
e f : α
I : Set α
hf : f ∉ I
⊢ (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
Tactic:
simp only [hf, not_false_eq_true, diff_singleton_eq_self, ite_false, IsEmpty.forall_iff, and_true,
  and_iff_left_iff_imp]
State after:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I✝ C : Set α
M : Matroid α
e f : α
I : Set α
hf : f ∉ I
⊢ M.Indep I → I ⊆ insert f M.E

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I✝ C : Set α
M : Matroid α
e f : α
I : Set α
hf : f ∉ I
⊢ M.Indep I → I ⊆ insert f M.E
Tactic:
exact fun hI ↦ hI.subset_ground.trans <| subset_insert _ _
State after:
no goals