Theorem: Matroid.simple_iff_cl_subset_self_forall (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
⊢ M.Simple ↔ ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
Tactic:
refine ⟨fun h e he ↦ by rw [cl_singleton_eq], fun h ↦ ?_⟩
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
⊢ M.Simple

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
⊢ M.Simple
Tactic:
have hl : M.Loopless := by
  rw [loopless_iff_forall_not_loop]
  intro e _ hel
  obtain ⟨f, hf⟩ := M.exists_nonloop
  obtain (rfl : e = f) := (h f hf).subset (hel.mem_cl _)
  exact hf.not_loop hel
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
hl : M.Loopless
⊢ M.Simple

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
hl : M.Loopless
⊢ M.Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall, and_iff_right hl]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
hl : M.Loopless
⊢ ∀ (e f : α), M.Parallel e f → e = f

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
hl : M.Loopless
⊢ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
exact fun e f hp ↦ (h _ hp.nonloop_right) hp.mem_cl
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
inst✝ : M.RkPos
h : M.Simple
e : α
he : M.Nonloop e
⊢ M.cl {e} ⊆ {e}
Tactic:
rw [cl_singleton_eq]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
⊢ M.Loopless
Tactic:
rw [loopless_iff_forall_not_loop]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
⊢ ∀ e ∈ M.E, ¬M.Loop e

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
⊢ ∀ e ∈ M.E, ¬M.Loop e
Tactic:
intro e _ hel
State after:
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
⊢ False

State before:
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
⊢ False
Tactic:
obtain ⟨f, hf⟩ := M.exists_nonloop
State after:
case intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
f : α
hf : M.Nonloop f
⊢ False

State before:
case intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
f : α
hf : M.Nonloop f
⊢ False
Tactic:
obtain (rfl : e = f) := (h f hf).subset (hel.mem_cl _)
State after:
case intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
hf : M.Nonloop e
⊢ False

State before:
case intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
hf : M.Nonloop e
⊢ False
Tactic:
exact hf.not_loop hel
State after:
no goals