internlm/Lean-Github huggingface dataset:
Theorem: Matroid.parallelExtend_not_nonloop
Proof 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]
Proof 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
Theorem: Matroid.parallelExtend_not_nonloop
Proof 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
Proof 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
Theorem: Matroid.parallelExtend_not_nonloop
Proof 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
Proof 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
Theorem: Matroid.parallelExtend_not_nonloop
Proof 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]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_not_nonloop
Proof 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]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_eq_parallelExtend_delete
Proof 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
Proof state after:
no goals
Theorem: Matroid.parallelExtend_eq_parallelExtend_delete
Proof 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]
Proof 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
Theorem: Matroid.parallelExtend_eq_parallelExtend_delete
Proof 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]
Proof 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
Theorem: Matroid.parallelExtend_eq_parallelExtend_delete
Proof 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
Proof state after:
no goals
Theorem: Matroid.parallelExtend_delete_eq'
Proof 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 _ _
Proof state after:
no goals
Theorem: Matroid.parallelExtend_delete_eq'
Proof 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]
Proof 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)
Theorem: Matroid.parallelExtend_delete_eq'
Proof 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 -
Proof 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
Theorem: Matroid.parallelExtend_delete_eq'
Proof 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]
Proof 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
Theorem: Matroid.parallelExtend_delete_eq'
Proof 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 _ _
Proof state after:
no goals
Theorem: Matroid.parallelExtend_delete_eq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e✝ f x : α
I C : Set α
e : α
hf : f ∉ M.E
⊢ M.parallelExtend e f ＼ f = M
Tactic:
rwa [parallelExtend_delete_eq', deleteElem, delete_eq_self_iff, disjoint_singleton_left]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_nonloop_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
⊢ (M.parallelExtend e f).Nonloop x ↔ M.Nonloop x ∨ x = f
Tactic:
rw [← indep_singleton, parallelExtend, restrict_indep_iff, singleton_subset_iff,
  comap_indep_iff, and_iff_left (injOn_singleton _ _), mem_insert_iff,
  image_update, image_id, image_id]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
⊢ M.Indep (if f ∈ {x} then insert e ({x} \ {f}) else {x}) ∧ (x = f ∨ x ∈ M.E) ↔ M.Nonloop x ∨ x = f
Theorem: Matroid.parallelExtend_nonloop_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
⊢ M.Indep (if f ∈ {x} then insert e ({x} \ {f}) else {x}) ∧ (x = f ∨ x ∈ M.E) ↔ M.Nonloop x ∨ x = f
Tactic:
obtain (rfl | hne) := eq_or_ne x f
Proof state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
⊢ M.Indep (if x ∈ {x} then insert e ({x} \ {x}) else {x}) ∧ (x = x ∨ x ∈ M.E) ↔ M.Nonloop x ∨ x = x

case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hne : x ≠ f
⊢ M.Indep (if f ∈ {x} then insert e ({x} \ {f}) else {x}) ∧ (x = f ∨ x ∈ M.E) ↔ M.Nonloop x ∨ x = f
Theorem: Matroid.parallelExtend_nonloop_iff
Proof state before:
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hne : x ≠ f
⊢ M.Indep (if f ∈ {x} then insert e ({x} \ {f}) else {x}) ∧ (x = f ∨ x ∈ M.E) ↔ M.Nonloop x ∨ x = f
Tactic:
simp only [mem_singleton_iff, hne.symm, not_false_eq_true, diff_singleton_eq_self, ite_false,
  indep_singleton, hne, false_or, or_false, and_iff_left_iff_imp]
Proof state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hne : x ≠ f
⊢ M.Nonloop x → x ∈ M.E
Theorem: Matroid.parallelExtend_nonloop_iff
Proof state before:
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hne : x ≠ f
⊢ M.Nonloop x → x ∈ M.E
Tactic:
exact Nonloop.mem_ground
Proof state after:
no goals
Theorem: Matroid.parallelExtend_nonloop_iff
Proof state before:
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
⊢ M.Indep (if x ∈ {x} then insert e ({x} \ {x}) else {x}) ∧ (x = x ∨ x ∈ M.E) ↔ M.Nonloop x ∨ x = x
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.parallelExtend_parallel
Proof 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).Parallel e f
Tactic:
have he' : (M.parallelExtend e f).Nonloop e := by
  rw [parallelExtend_nonloop_iff he]; left; assumption
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ (M.parallelExtend e f).Parallel e f
Theorem: Matroid.parallelExtend_parallel
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ (M.parallelExtend e f).Parallel e f
Tactic:
have hf : (M.parallelExtend e f).Nonloop f := by
  rw [parallelExtend_nonloop_iff he]; right; rfl
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
⊢ (M.parallelExtend e f).Parallel e f
Theorem: Matroid.parallelExtend_parallel
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
⊢ (M.parallelExtend e f).Parallel e f
Tactic:
obtain (rfl | hef) := eq_or_ne e f
Proof state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
he' hf : (M.parallelExtend e e).Nonloop e
⊢ (M.parallelExtend e e).Parallel e e

case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
⊢ (M.parallelExtend e f).Parallel e f
Theorem: Matroid.parallelExtend_parallel
Proof state before:
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
⊢ (M.parallelExtend e f).Parallel e f
Tactic:
rw [he'.parallel_iff_dep hf hef, Dep, pair_subset_iff, and_iff_right he'.mem_ground,
  and_iff_left hf.mem_ground, parallelExtend, restrict_indep_iff, comap_indep_iff,
  image_update, image_id, image_id,
  if_pos (mem_insert_of_mem _ (show f ∈ ({f} : Set α) from rfl))]
Proof state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
⊢ ¬((M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E)
Theorem: Matroid.parallelExtend_parallel
Proof state before:
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
⊢ ¬((M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E)
Tactic:
exact fun hcon ↦ hef <| hcon.1.2 (by simp) (by simp) (by simp [update_noteq hef e id])
Proof state after:
no goals
Theorem: Matroid.parallelExtend_parallel
Proof 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).Nonloop e
Tactic:
rw [parallelExtend_nonloop_iff he]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ M.Nonloop e ∨ e = f
Theorem: Matroid.parallelExtend_parallel
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ M.Nonloop e ∨ e = f
Tactic:
left
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ M.Nonloop e
Theorem: Matroid.parallelExtend_parallel
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ M.Nonloop e
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.parallelExtend_parallel
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ (M.parallelExtend e f).Nonloop f
Tactic:
rw [parallelExtend_nonloop_iff he]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ M.Nonloop f ∨ f = f
Theorem: Matroid.parallelExtend_parallel
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ M.Nonloop f ∨ f = f
Tactic:
right
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ f = f
Theorem: Matroid.parallelExtend_parallel
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ f = f
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.parallelExtend_parallel
Proof state before:
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
he' hf : (M.parallelExtend e e).Nonloop e
⊢ (M.parallelExtend e e).Parallel e e
Tactic:
rwa [parallel_self_iff]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_parallel
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
hcon : (M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E
⊢ e ∈ {e, f}
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.parallelExtend_parallel
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
hcon : (M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E
⊢ f ∈ {e, f}
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.parallelExtend_parallel
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
hcon : (M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E
⊢ update id f e e = update id f e f
Tactic:
simp [update_noteq hef e id]
Proof state after:
no goals
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M' = M.parallelExtend e f ↔ M'.Parallel e f ∧ M' ＼ f = M
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M' = M.parallelExtend e f → M'.Parallel e f ∧ M' ＼ f = M

case mpr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M'.Parallel e f ∧ M' ＼ f = M → M' = M.parallelExtend e f
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M'.Parallel e f ∧ M' ＼ f = M → M' = M.parallelExtend e f
Tactic:
rintro ⟨h, rfl⟩
Proof state after:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
he : (M' ＼ f).Nonloop e
hf : f ∉ (M' ＼ f).E
⊢ M' = (M' ＼ f).parallelExtend e f
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
he : (M' ＼ f).Nonloop e
hf : f ∉ (M' ＼ f).E
⊢ M' = (M' ＼ f).parallelExtend e f
Tactic:
simp only [deleteElem, delete_nonloop_iff, mem_singleton_iff] at he
Proof state after:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
⊢ M' = (M' ＼ f).parallelExtend e f
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
⊢ M' = (M' ＼ f).parallelExtend e f
Tactic:
refine eq_of_indep_iff_indep_forall (by simp [insert_eq_of_mem h.mem_ground_right])
  (fun I hI ↦ ?_)
Proof state after:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I
Tactic:
obtain (hfI | hfI) := em' (f ∈ I)
Proof state after:
case mpr.intro.inl
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∉ I
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I

case mpr.intro.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
case mpr.intro.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I
Tactic:
suffices M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I by
  simpa [hfI, parallelExtend, Ne.symm he.2, hI.trans (subset_insert _ _)]
Proof state after:
case mpr.intro.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
case mpr.intro.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I
Tactic:
obtain (heI | heI) := em (e ∈ I)
Proof state after:
case mpr.intro.inr.inl
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
heI : e ∈ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I

case mpr.intro.inr.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
heI : e ∉ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
case mpr.intro.inr.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
heI : e ∉ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I
Tactic:
simp [heI, h.parallel'.symm.indep_substitute_iff hfI heI]
Proof state after:
no goals
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
case mp
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M' = M.parallelExtend e f → M'.Parallel e f ∧ M' ＼ f = M
Tactic:
rintro rfl
Proof state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
M : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ (M.parallelExtend e f).Parallel e f ∧ M.parallelExtend e f ＼ f = M