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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple ↔ ∀ P ∈ M.parallelClasses, P.encard = 1
Tactic:
simp only [mem_parallelClasses_iff, forall_exists_index, and_imp, encard_eq_one]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple ↔ ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple ↔ ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
Tactic:
refine ⟨?_, fun h ↦ ?_⟩
State after:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple → ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
⊢ M.Simple

State before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
⊢ M.Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall, and_iff_right (by assumption)]
State after:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
⊢ ∀ (e f : α), M.Parallel e f → e = f

State before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
⊢ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
refine fun e f hef ↦ ?_
State after:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
e f : α
hef : M.Parallel e f
⊢ e = f

State before:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
e f : α
hef : M.Parallel e f
⊢ e = f
Tactic:
obtain ⟨x, hx⟩ := h _ e hef.nonloop_left rfl
State after:
case refine_2.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
e f : α
hef : M.Parallel e f
x : α
hx : {f | M.Parallel e f} = {x}
⊢ e = f

State before:
case refine_2.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
e f : α
hef : M.Parallel e f
x : α
hx : {f | M.Parallel e f} = {x}
⊢ e = f
Tactic:
rw [(show f = x from hx.subset hef), show e = x from hx.subset (hef.nonloop_left.parallel_self)]
State after:
no goals

State before:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
⊢ M.Simple → ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
Tactic:
rintro h P x hx rfl
State after:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : M.Simple
x : α
hx : M.Nonloop x
⊢ ∃ x_1, {f | M.Parallel x f} = {x_1}

State before:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : M.Simple
x : α
hx : M.Nonloop x
⊢ ∃ x_1, {f | M.Parallel x f} = {x_1}
Tactic:
exact ⟨x, by simp [Set.ext_iff, parallel_iff_eq hx.mem_ground]⟩
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : M.Simple
x : α
hx : M.Nonloop x
⊢ {f | M.Parallel x f} = {x}
Tactic:
simp [Set.ext_iff, parallel_iff_eq hx.mem_ground]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Loopless
h : ∀ (P : Set α) (x : α), M.Nonloop x → P = {f | M.Parallel x f} → ∃ x, P = {x}
⊢ M.Loopless
Tactic:
assumption
State after:
no goals