Theorem: Matroid.parallel_iff_circuit (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
⊢ M.Parallel e f ↔ M.Circuit {e, f}
Tactic:
refine' ⟨fun h ↦ circuit_iff_dep_forall_diff_singleton_indep.2 ⟨h.dep_of_ne hef,_⟩, fun h ↦ _⟩
State after:
case refine'_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Parallel e f
⊢ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})

case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.Parallel e f

State before:
case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.Parallel e f
Tactic:
rw [Nonloop.parallel_iff_mem_cl]
State after:
case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ e ∈ M.cl {f}

case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.Nonloop e

State before:
case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.Nonloop e
Tactic:
apply h.nonloop_of_mem_of_one_lt_card _ (mem_insert _ _)
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ 1 < {e, f}.encard

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ 1 < {e, f}.encard
Tactic:
rw [encard_pair hef]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ 1 < 2

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ 1 < 2
Tactic:
norm_num
State after:
no goals

State before:
case refine'_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Parallel e f
⊢ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Tactic:
rintro x (rfl | rfl)
State after:
case refine'_1.inl
α : Type u_1
M N : Matroid α
f g : α
I X P D : Set α
x : α
hef : x ≠ f
h : M.Parallel x f
⊢ M.Indep ({x, f} \ {x})

case refine'_1.inr
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
x : α
hef : e ≠ x
h : M.Parallel e x
⊢ M.Indep ({e, x} \ {x})

State before:
case refine'_1.inl
α : Type u_1
M N : Matroid α
f g : α
I X P D : Set α
x : α
hef : x ≠ f
h : M.Parallel x f
⊢ M.Indep ({x, f} \ {x})
Tactic:
rw [pair_diff_left hef]
State after:
case refine'_1.inl
α : Type u_1
M N : Matroid α
f g : α
I X P D : Set α
x : α
hef : x ≠ f
h : M.Parallel x f
⊢ M.Indep {f}

State before:
case refine'_1.inl
α : Type u_1
M N : Matroid α
f g : α
I X P D : Set α
x : α
hef : x ≠ f
h : M.Parallel x f
⊢ M.Indep {f}
Tactic:
exact h.nonloop_right.indep
State after:
no goals

State before:
case refine'_1.inr
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
x : α
hef : e ≠ x
h : M.Parallel e x
⊢ M.Indep ({e, x} \ {x})
Tactic:
rw [pair_diff_right hef]
State after:
case refine'_1.inr
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
x : α
hef : e ≠ x
h : M.Parallel e x
⊢ M.Indep {e}

State before:
case refine'_1.inr
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
x : α
hef : e ≠ x
h : M.Parallel e x
⊢ M.Indep {e}
Tactic:
exact h.nonloop_left.indep
State after:
no goals

State before:
case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ e ∈ M.cl {f}
Tactic:
convert h.mem_cl_diff_singleton_of_mem (mem_insert _ _)
State after:
case h.e'_5.h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ {f} = {e, f} \ {e}

State before:
case h.e'_5.h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ {f} = {e, f} \ {e}
Tactic:
rw [pair_diff_left hef]
State after:
no goals