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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ P ∈ M.parallelClasses ↔ ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅
Tactic:
simp only [parallelClasses, Partition.mem_congr_iff, Flat.mem_covByPartition_iff,
  loops_covBy_iff, point_iff_exists_eq_cl_nonloop]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P) ↔ ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P) ↔ ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅
Tactic:
constructor
State after:
case mp
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P) → ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅

case mpr
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅) → ∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P

State before:
case mpr
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅) → ∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P
Tactic:
rintro ⟨e, he, rfl⟩
State after:
case mpr.intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
e : α
he : M.Nonloop e
⊢ ∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = M.cl {e} \ M.cl ∅

State before:
case mpr.intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
e : α
he : M.Nonloop e
⊢ ∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = M.cl {e} \ M.cl ∅
Tactic:
exact ⟨_, ⟨e, he, rfl⟩,rfl⟩
State after:
no goals

State before:
case mp
α : Type u_1
M N : Matroid α
e f g : α
I X P✝ D P : Set α
⊢ (∃ F', (∃ e, M.Nonloop e ∧ F' = M.cl {e}) ∧ F' \ M.cl ∅ = P) → ∃ e, M.Nonloop e ∧ P = M.cl {e} \ M.cl ∅
Tactic:
rintro ⟨_, ⟨e, he, rfl⟩, rfl⟩
State after:
case mp.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
e : α
he : M.Nonloop e
⊢ ∃ e_1, M.Nonloop e_1 ∧ M.cl {e} \ M.cl ∅ = M.cl {e_1} \ M.cl ∅

State before:
case mp.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
e : α
he : M.Nonloop e
⊢ ∃ e_1, M.Nonloop e_1 ∧ M.cl {e} \ M.cl ∅ = M.cl {e_1} \ M.cl ∅
Tactic:
exact ⟨e, he, rfl⟩
State after:
no goals