Theorem: Matroid.Nonloop.cl_eq_cl_iff_eq_or_dep (Matroid/Loop.lean)

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
hf : M.Nonloop f
⊢ M.cl {e} = M.cl {f} ↔ e = f ∨ ¬M.Indep {e, f}
Tactic:
obtain (rfl | hne) := eq_or_ne e f
State after:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he hf : M.Nonloop e
⊢ M.cl {e} = M.cl {e} ↔ e = e ∨ ¬M.Indep {e, e}

case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ M.cl {e} = M.cl {f} ↔ e = f ∨ ¬M.Indep {e, f}

State before:
case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ M.cl {e} = M.cl {f} ↔ e = f ∨ ¬M.Indep {e, f}
Tactic:
simp_rw [he.cl_eq_cl_iff_circuit_of_ne hne, or_iff_right hne,
  circuit_iff_dep_forall_diff_singleton_indep, dep_iff, insert_subset_iff, singleton_subset_iff,
  and_iff_left hf.mem_ground, and_iff_left he.mem_ground, and_iff_left_iff_imp]
State after:
case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ ¬M.Indep {e, f} → ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})

State before:
case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ ¬M.Indep {e, f} → ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Tactic:
rintro hi x (rfl | rfl)
State after:
case inr.inl
α : Type u_1
β : Type u_2
M N : Matroid α
f : α
B L L' I X Y Z F C K : Set α
hf : M.Nonloop f
x : α
he : M.Nonloop x
hne : x ≠ f
hi : ¬M.Indep {x, f}
⊢ M.Indep ({x, f} \ {x})

case inr.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
x : α
hf : M.Nonloop x
hne : e ≠ x
hi : ¬M.Indep {e, x}
⊢ M.Indep ({e, x} \ {x})

State before:
case inr.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
x : α
hf : M.Nonloop x
hne : e ≠ x
hi : ¬M.Indep {e, x}
⊢ M.Indep ({e, x} \ {x})
Tactic:
rwa [pair_diff_right hne, indep_singleton]
State after:
no goals

State before:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he hf : M.Nonloop e
⊢ M.cl {e} = M.cl {e} ↔ e = e ∨ ¬M.Indep {e, e}
Tactic:
exact iff_of_true rfl (Or.inl rfl)
State after:
no goals

State before:
case inr.inl
α : Type u_1
β : Type u_2
M N : Matroid α
f : α
B L L' I X Y Z F C K : Set α
hf : M.Nonloop f
x : α
he : M.Nonloop x
hne : x ≠ f
hi : ¬M.Indep {x, f}
⊢ M.Indep ({x, f} \ {x})
Tactic:
rwa [pair_diff_left hne, indep_singleton]
State after:
no goals