Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne (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
hef : e ≠ f
⊢ M.cl {e} = M.cl {f} ↔ M.Circuit {e, f}
Tactic:
refine' ⟨fun h ↦ _, fun h ↦ _⟩
State after:
case refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
⊢ M.Circuit {e, f}

case refine'_2
α : 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
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.cl {e} = M.cl {f}

State before:
case refine'_2
α : 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
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.cl {e} = M.cl {f}
Tactic:
have hcl := (h.cl_diff_singleton_eq_cl e).trans (h.cl_diff_singleton_eq_cl f).symm
State after:
case refine'_2
α : 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
hef : e ≠ f
h : M.Circuit {e, f}
hcl : M.cl ({e, f} \ {e}) = M.cl ({e, f} \ {f})
⊢ M.cl {e} = M.cl {f}

State before:
case refine'_2
α : 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
hef : e ≠ f
h : M.Circuit {e, f}
hcl : M.cl ({e, f} \ {e}) = M.cl ({e, f} \ {f})
⊢ M.cl {e} = M.cl {f}
Tactic:
rwa [pair_diff_left hef, pair_diff_right hef, eq_comm] at hcl
State after:
no goals

State before:
case refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
⊢ M.Circuit {e, f}
Tactic:
have hf := he.nonloop_of_mem_cl (by rw [← h]; exact M.mem_cl_self e)
State after:
case refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ M.Circuit {e, f}

State before:
case refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ M.Circuit {e, f}
Tactic:
rw [circuit_iff_dep_forall_diff_singleton_indep, dep_iff, insert_subset_iff,
  and_iff_right he.mem_ground, singleton_subset_iff, and_iff_left hf.mem_ground]
State after:
case refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ ¬M.Indep {e, f} ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})

State before:
case refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ ¬M.Indep {e, f} ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Tactic:
refine' ⟨fun hi ↦ _, _⟩
State after:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ False

case refine'_1.refine'_2
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})

State before:
case refine'_1.refine'_2
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Tactic:
rintro x (rfl | rfl)
State after:
case refine'_1.refine'_2.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
hef : x ≠ f
h : M.cl {x} = M.cl {f}
⊢ M.Indep ({x, f} \ {x})

case refine'_1.refine'_2.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 : α
hef : e ≠ x
h : M.cl {e} = M.cl {x}
hf : M.Nonloop x
⊢ M.Indep ({e, x} \ {x})

State before:
case refine'_1.refine'_2.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 : α
hef : e ≠ x
h : M.cl {e} = M.cl {x}
hf : M.Nonloop x
⊢ M.Indep ({e, x} \ {x})
Tactic:
rwa [pair_diff_right hef, indep_singleton]
State after:
no goals

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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
⊢ e ∈ M.cl {?m.31393}
Tactic:
rw [← h]
State after:
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
⊢ e ∈ M.cl {e}

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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
⊢ e ∈ M.cl {e}
Tactic:
exact M.mem_cl_self e
State after:
no goals

State before:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ False
Tactic:
apply hi.not_mem_cl_diff_of_mem (mem_insert _ _)
State after:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∈ M.cl ({e, f} \ {e})

State before:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∈ M.cl ({e, f} \ {e})
Tactic:
rw [insert_diff_of_mem _ (by exact rfl : e ∈ {e}), diff_singleton_eq_self (by simpa), ← h]
State after:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∈ M.cl {e}

State before:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∈ M.cl {e}
Tactic:
exact mem_cl_self _ _ he.mem_ground
State after:
no goals

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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∈ {e}
Tactic:
exact rfl
State after:
no goals

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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∉ {f}
Tactic:
simpa
State after:
no goals

State before:
case refine'_1.refine'_2.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
hef : x ≠ f
h : M.cl {x} = M.cl {f}
⊢ M.Indep ({x, f} \ {x})
Tactic:
rwa [pair_diff_left hef, indep_singleton]
State after:
no goals