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

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
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}))

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)
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}))

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]
State after:
no goals

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
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

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
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

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]
State after:
no goals

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]
State after:
no goals

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
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

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
State after:
no goals

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]
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}))

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)
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}))

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]
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})

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)
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

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
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

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
State after:
no goals

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]
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

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))
State after:
no goals