Theorem: Matroid.cl_empty_eq_ground_iff (Matroid/Closure.lean)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.cl ∅ = M.E ↔ M = loopyOn M.E
Tactic:
refine ⟨fun h ↦ eq_of_cl_eq_cl_forall ?_, fun h ↦ by rw [h, loopyOn_cl_eq, loopyOn_ground]⟩
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.cl ∅ = M.E
⊢ ∀ (X : Set α), M.cl X = (loopyOn M.E).cl X

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.cl ∅ = M.E
⊢ ∀ (X : Set α), M.cl X = (loopyOn M.E).cl X
Tactic:
refine fun X ↦ subset_antisymm (by simp [cl_subset_ground]) ?_
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
h : M.cl ∅ = M.E
X : Set α
⊢ (loopyOn M.E).cl X ⊆ M.cl X

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
h : M.cl ∅ = M.E
X : Set α
⊢ (loopyOn M.E).cl X ⊆ M.cl X
Tactic:
rw [loopyOn_cl_eq, ← h]
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
h : M.cl ∅ = M.E
X : Set α
⊢ M.cl ∅ ⊆ M.cl X

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
h : M.cl ∅ = M.E
X : Set α
⊢ M.cl ∅ ⊆ M.cl X
Tactic:
exact M.cl_mono (empty_subset _)
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M = loopyOn M.E
⊢ M.cl ∅ = M.E
Tactic:
rw [h, loopyOn_cl_eq, loopyOn_ground]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
h : M.cl ∅ = M.E
X : Set α
⊢ M.cl X ⊆ (loopyOn M.E).cl X
Tactic:
simp [cl_subset_ground]
State after:
no goals