Theorem: Matroid.parallelExtend_nonloop_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
⊢ (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]
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

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

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

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

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