internlm/Lean-Github huggingface dataset:
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
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
Tactic:
exact ⟨parallelExtend_parallel he f, parallelExtend_delete_eq e hf⟩
Proof state after:
no goals
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
α : 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'.E = ((M' ＼ f).parallelExtend e f).E
Tactic:
simp [insert_eq_of_mem h.mem_ground_right]
Proof state after:
no goals
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
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
Tactic:
simp [hfI, parallelExtend, hI.trans (subset_insert _ _)]
Proof state after:
no goals
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
α : 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
this : M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I
Tactic:
simpa [hfI, parallelExtend, Ne.symm he.2, hI.trans (subset_insert _ _)]
Proof state after:
no goals
Theorem: Matroid.eq_parallelExtend_iff
Proof state before:
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
Tactic:
simp [heI, show ¬ M'.Indep I from
  fun hI ↦ he.2 (h.eq_of_indep (hI.subset (pair_subset heI hfI)))]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_cl_eq_of_mem
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
X : Set α
heX : e ∈ M.cl X
⊢ (M.parallelExtend e f).cl X = insert f (M.cl X)
Tactic:
nth_rw 2 [← M.parallelExtend_delete_eq e hf]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : e ∈ M.cl X
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f ＼ f).cl X)
Theorem: Matroid.parallelExtend_cl_eq_of_mem
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
X : Set α
heX : e ∈ M.cl X
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f ＼ f).cl X)
Tactic:
simp only [deleteElem, delete_cl_eq, insert_diff_singleton]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : e ∈ M.cl X
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f).cl (X \ {f}))
Theorem: Matroid.parallelExtend_cl_eq_of_mem
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
X : Set α
heX : e ∈ M.cl X
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f).cl (X \ {f}))
Tactic:
rw [← M.parallelExtend_delete_eq e hf, deleteElem, delete_cl_eq, mem_diff,
  (parallelExtend_parallel he f).mem_cl_iff_mem_cl] at heX
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f}
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f).cl (X \ {f}))
Theorem: Matroid.parallelExtend_cl_eq_of_mem
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
X : Set α
heX : f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f}
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f).cl (X \ {f}))
Tactic:
rw [cl_diff_singleton_eq_cl heX.1, eq_comm, insert_eq_self]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f}
⊢ f ∈ (M.parallelExtend e f).cl X
Theorem: Matroid.parallelExtend_cl_eq_of_mem
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
X : Set α
heX : f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f}
⊢ f ∈ (M.parallelExtend e f).cl X
Tactic:
exact mem_of_mem_of_subset heX.1 (cl_subset_cl _ diff_subset)
Proof state after:
no goals
Theorem: Matroid.parallelExtend_cl_eq_of_not_mem_not_mem
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
X : Set α
heX : e ∉ M.cl X
hfX : f ∉ X
⊢ (M.parallelExtend e f).cl X = M.cl X
Tactic:
nth_rw 2 [← M.parallelExtend_delete_eq e hf]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : e ∉ M.cl X
hfX : f ∉ X
⊢ (M.parallelExtend e f).cl X = (M.parallelExtend e f ＼ f).cl X
Theorem: Matroid.parallelExtend_cl_eq_of_not_mem_not_mem
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
X : Set α
heX : e ∉ M.cl X
hfX : f ∉ X
⊢ (M.parallelExtend e f).cl X = (M.parallelExtend e f ＼ f).cl X
Tactic:
have hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f}) := by
  rw [← M.parallelExtend_delete_eq e hf, deleteElem, delete_cl_eq, mem_diff,
    (parallelExtend_parallel he f).mem_cl_iff_mem_cl] at heX
  simpa [(show e ≠ f by rintro rfl; exact hf he.mem_ground)] using heX
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : e ∉ M.cl X
hfX : f ∉ X
hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f})
⊢ (M.parallelExtend e f).cl X = (M.parallelExtend e f ＼ f).cl X
Theorem: Matroid.parallelExtend_cl_eq_of_not_mem_not_mem
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
X : Set α
heX : e ∉ M.cl X
hfX : f ∉ X
hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f})
⊢ (M.parallelExtend e f).cl X = (M.parallelExtend e f ＼ f).cl X
Tactic:
simp only [deleteElem, delete_cl_eq, diff_singleton_eq_self hfX']
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : e ∉ M.cl X
hfX : f ∉ X
hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f})
⊢ (M.parallelExtend e f).cl X = (M.parallelExtend e f).cl (X \ {f})
Theorem: Matroid.parallelExtend_cl_eq_of_not_mem_not_mem
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
X : Set α
heX : e ∉ M.cl X
hfX : f ∉ X
hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f})
⊢ (M.parallelExtend e f).cl X = (M.parallelExtend e f).cl (X \ {f})
Tactic:
rw [diff_singleton_eq_self hfX]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_cl_eq_of_not_mem_not_mem
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
X : Set α
heX : e ∉ M.cl X
hfX : f ∉ X
⊢ f ∉ (M.parallelExtend e f).cl (X \ {f})
Tactic:
rw [← M.parallelExtend_delete_eq e hf, deleteElem, delete_cl_eq, mem_diff,
  (parallelExtend_parallel he f).mem_cl_iff_mem_cl] at heX
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : ¬(f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f})
hfX : f ∉ X
⊢ f ∉ (M.parallelExtend e f).cl (X \ {f})
Theorem: Matroid.parallelExtend_cl_eq_of_not_mem_not_mem
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
X : Set α
heX : ¬(f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f})
hfX : f ∉ X
⊢ f ∉ (M.parallelExtend e f).cl (X \ {f})
Tactic:
simpa [(show e ≠ f by rintro rfl; exact hf he.mem_ground)] using heX
Proof state after:
no goals
Theorem: Matroid.parallelExtend_cl_eq_of_not_mem_not_mem
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
X : Set α
heX : ¬(f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f})
hfX : f ∉ X
⊢ e ≠ f
Tactic:
rintro rfl
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
X : Set α
hf : e ∉ M.E
heX : ¬(e ∈ (M.parallelExtend e e).cl (X \ {e}) ∧ e ∉ {e})
hfX : e ∉ X
⊢ False
Theorem: Matroid.parallelExtend_cl_eq_of_not_mem_not_mem
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
X : Set α
hf : e ∉ M.E
heX : ¬(e ∈ (M.parallelExtend e e).cl (X \ {e}) ∧ e ∉ {e})
hfX : e ∉ X
⊢ False
Tactic:
exact hf he.mem_ground
Proof state after:
no goals
Theorem: Matroid.parallelExtend_indep_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
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
⊢ (M.parallelExtend e f).Indep I ↔ f ∉ I ∧ M.Indep I ∨ f ∈ I ∧ e ∉ I ∧ M.Indep (insert e (I \ {f}))
Tactic:
have hef : e ≠ f := by rintro rfl; exact hf he.mem_ground
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
⊢ (M.parallelExtend e f).Indep I ↔ f ∉ I ∧ M.Indep I ∨ f ∈ I ∧ e ∉ I ∧ M.Indep (insert e (I \ {f}))
Theorem: Matroid.parallelExtend_indep_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
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
⊢ (M.parallelExtend e f).Indep I ↔ f ∉ I ∧ M.Indep I ∨ f ∈ I ∧ e ∉ I ∧ M.Indep (insert e (I \ {f}))
Tactic:
obtain (hfI | hfI) := em (f ∈ I)
Proof state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
⊢ (M.parallelExtend e f).Indep I ↔ f ∉ I ∧ M.Indep I ∨ f ∈ I ∧ e ∉ I ∧ M.Indep (insert e (I \ {f}))

case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∉ I
⊢ (M.parallelExtend e f).Indep I ↔ f ∉ I ∧ M.Indep I ∨ f ∈ I ∧ e ∉ I ∧ M.Indep (insert e (I \ {f}))
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∉ I
⊢ (M.parallelExtend e f).Indep I ↔ f ∉ I ∧ M.Indep I ∨ f ∈ I ∧ e ∉ I ∧ M.Indep (insert e (I \ {f}))
Tactic:
simp [hdel _ hfI, hfI]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_indep_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
⊢ ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
Tactic:
rintro J hfJ
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
J : Set α
hfJ : f ∉ J
⊢ (M.parallelExtend e f).Indep J ↔ M.Indep J
Theorem: Matroid.parallelExtend_indep_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
J : Set α
hfJ : f ∉ J
⊢ (M.parallelExtend e f).Indep J ↔ M.Indep J
Tactic:
convert (delete_indep_iff (M := M.parallelExtend e f) (D := {f}) (I := J)).symm using 1
Proof state after:
case h.e'_1.a
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
J : Set α
hfJ : f ∉ J
⊢ (M.parallelExtend e f).Indep J ↔ (M.parallelExtend e f).Indep J ∧ Disjoint J {f}

case h.e'_2.a
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
J : Set α
hfJ : f ∉ J
⊢ M.Indep J ↔ (M.parallelExtend e f ＼ {f}).Indep J
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
case h.e'_2.a
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
J : Set α
hfJ : f ∉ J
⊢ M.Indep J ↔ (M.parallelExtend e f ＼ {f}).Indep J
Tactic:
rw [← deleteElem, parallelExtend_delete_eq', deleteElem, delete_indep_iff,
  disjoint_singleton_right, and_iff_left hfJ]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
case h.e'_1.a
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
J : Set α
hfJ : f ∉ J
⊢ (M.parallelExtend e f).Indep J ↔ (M.parallelExtend e f).Indep J ∧ Disjoint J {f}
Tactic:
rw [disjoint_singleton_right, and_iff_left hfJ]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_indep_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
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
⊢ e ≠ f
Tactic:
rintro rfl
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
hf : e ∉ M.E
hdel : ∀ (J : Set α), e ∉ J → ((M.parallelExtend e e).Indep J ↔ M.Indep J)
⊢ False
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
hf : e ∉ M.E
hdel : ∀ (J : Set α), e ∉ J → ((M.parallelExtend e e).Indep J ↔ M.Indep J)
⊢ False
Tactic:
exact hf he.mem_ground
Proof state after:
no goals
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
⊢ (M.parallelExtend e f).Indep I ↔ f ∉ I ∧ M.Indep I ∨ f ∈ I ∧ e ∉ I ∧ M.Indep (insert e (I \ {f}))
Tactic:
rw [iff_true_intro hfI, not_true, false_and, false_or, true_and]
Proof state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
⊢ (M.parallelExtend e f).Indep I ↔ e ∉ I ∧ M.Indep (insert e (I \ {f}))
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
⊢ (M.parallelExtend e f).Indep I ↔ e ∉ I ∧ M.Indep (insert e (I \ {f}))
Tactic:
obtain (heI | heI) := em (e ∈ I)
Proof state after:
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∈ I
⊢ (M.parallelExtend e f).Indep I ↔ e ∉ I ∧ M.Indep (insert e (I \ {f}))

case inl.inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∉ I
⊢ (M.parallelExtend e f).Indep I ↔ e ∉ I ∧ M.Indep (insert e (I \ {f}))
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
case inl.inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∉ I
⊢ (M.parallelExtend e f).Indep I ↔ e ∉ I ∧ M.Indep (insert e (I \ {f}))
Tactic:
rw [and_iff_right heI,
  (parallelExtend_parallel he f).parallel'.symm.indep_substitute_iff hfI heI, hdel]
Proof state after:
case inl.inr.a
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∉ I
⊢ f ∉ insert e (I \ {f})
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
case inl.inr.a
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∉ I
⊢ f ∉ insert e (I \ {f})
Tactic:
rintro (rfl | h)
Proof state after:
case inl.inr.a.inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
f x : α
I C : Set α
hf : f ∉ M.E
hfI : f ∈ I
he : M.Nonloop f
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend f f).Indep J ↔ M.Indep J)
hef : f ≠ f
heI : f ∉ I
⊢ False

case inl.inr.a.inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∉ I
h : f ∈ I \ {f}
⊢ False
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
case inl.inr.a.inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
f x : α
I C : Set α
hf : f ∉ M.E
hfI : f ∈ I
he : M.Nonloop f
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend f f).Indep J ↔ M.Indep J)
hef : f ≠ f
heI : f ∉ I
⊢ False

case inl.inr.a.inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∉ I
h : f ∈ I \ {f}
⊢ False
Tactic:
exact hef rfl
Proof state after:
case inl.inr.a.inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∉ I
h : f ∈ I \ {f}
⊢ False
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
case inl.inr.a.inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∉ I
h : f ∈ I \ {f}
⊢ False
Tactic:
exact h.2 rfl
Proof state after:
no goals
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∈ I
⊢ (M.parallelExtend e f).Indep I ↔ e ∉ I ∧ M.Indep (insert e (I \ {f}))
Tactic:
simp only [heI, not_true_eq_false, mem_diff, mem_singleton_iff, true_and, false_and,
  iff_false, parallelExtend_ground]
Proof state after:
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∈ I
⊢ ¬(M.parallelExtend e f).Indep I
Theorem: Matroid.parallelExtend_indep_iff
Proof state before:
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hdel : ∀ (J : Set α), f ∉ J → ((M.parallelExtend e f).Indep J ↔ M.Indep J)
hef : e ≠ f
hfI : f ∈ I
heI : e ∈ I
⊢ ¬(M.parallelExtend e f).Indep I
Tactic:
exact fun hi ↦ ((parallelExtend_parallel he f).dep_of_ne hef).not_indep
  (hi.subset (pair_subset heI hfI))
Proof state after:
no goals
Theorem: Matroid.parallelExtend_circuit_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.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
have hef : e ≠ f := by rintro rfl; exact hf he.mem_ground
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Theorem: Matroid.parallelExtend_circuit_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
hef : e ≠ f
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
have aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C') := by
  intro C' hfC'
  suffices h' : ((M.parallelExtend e f) ＼ f).Circuit C' ↔ M.Circuit C' by
    simpa [deleteElem, delete_circuit_iff, hfC'] using h'
  rw [parallelExtend_delete_eq _ hf]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Theorem: Matroid.parallelExtend_circuit_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
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
by_cases hfC : f ∈ C
Proof state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Theorem: Matroid.parallelExtend_circuit_iff
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
swap
Proof state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))