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

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
hef : e ≠ f
⊢ M.parallelExtend e f = (M ＼ f).parallelExtend e f
Tactic:
classical
rw [parallelExtend, parallelExtend, deleteElem, delete_ground, insert_diff_singleton,
  eq_iff_indep_iff_indep_forall]
simp only [restrict_ground_eq, restrict_indep_iff, comap_indep_iff, ne_eq, image_update, id_eq,
  image_id', mem_diff, mem_singleton_iff, update_id_injOn_iff, delete_indep_iff,
  disjoint_singleton_right, and_congr_left_iff, iff_self_and, true_and]
aesop
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
hef : e ≠ f
⊢ M.parallelExtend e f = (M ＼ f).parallelExtend e f
Tactic:
rw [parallelExtend, parallelExtend, deleteElem, delete_ground, insert_diff_singleton,
  eq_iff_indep_iff_indep_forall]
State after:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
hef : e ≠ f
⊢ (M.comap (update id f e) ↾ insert f M.E).E = ((M ＼ {f}).comap (update id f e) ↾ insert f M.E).E ∧
    ∀ I ⊆ (M.comap (update id f e) ↾ insert f M.E).E,
      (M.comap (update id f e) ↾ insert f M.E).Indep I ↔ ((M ＼ {f}).comap (update id f e) ↾ insert f M.E).Indep I

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
hef : e ≠ f
⊢ (M.comap (update id f e) ↾ insert f M.E).E = ((M ＼ {f}).comap (update id f e) ↾ insert f M.E).E ∧
    ∀ I ⊆ (M.comap (update id f e) ↾ insert f M.E).E,
      (M.comap (update id f e) ↾ insert f M.E).Indep I ↔ ((M ＼ {f}).comap (update id f e) ↾ insert f M.E).Indep I
Tactic:
simp only [restrict_ground_eq, restrict_indep_iff, comap_indep_iff, ne_eq, image_update, id_eq,
  image_id', mem_diff, mem_singleton_iff, update_id_injOn_iff, delete_indep_iff,
  disjoint_singleton_right, and_congr_left_iff, iff_self_and, true_and]
State after:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
hef : e ≠ f
⊢ ∀ I ⊆ insert f M.E,
    I ⊆ insert f M.E →
      (f ∈ I → e ∈ I → f = e) →
        M.Indep (if f ∈ I then insert e (I \ {f}) else I) → f ∉ if f ∈ I then insert e (I \ {f}) else I

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
hef : e ≠ f
⊢ ∀ I ⊆ insert f M.E,
    I ⊆ insert f M.E →
      (f ∈ I → e ∈ I → f = e) →
        M.Indep (if f ∈ I then insert e (I \ {f}) else I) → f ∉ if f ∈ I then insert e (I \ {f}) else I
Tactic:
aesop
State after:
no goals