Theorem: Matroid.simple_iff_parallelClasses_eq_discrete' (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
Tactic:
refine ⟨fun h ↦ ⟨by infer_instance, Partition.eq_of_rel_iff_rel ?_⟩, fun ⟨_,h⟩ ↦ ?_⟩
State after:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ ∀ (x y : α), M.parallelClasses.Rel x y ↔ (Partition.discrete {e | M.Nonloop e}).Rel x y

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ M.Simple

State before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ 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 α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ ∀ (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 α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
simp [Parallel, h]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ M.Loopless
Tactic:
infer_instance
State after:
no goals

State before:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ ∀ (x y : α), M.parallelClasses.Rel x y ↔ (Partition.discrete {e | M.Nonloop e}).Rel x y
Tactic:
simp only [Partition.discrete.rel_iff_eq, mem_setOf_eq,
  show M.parallelClasses.Rel = M.Parallel from rfl]
State after:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ ∀ (x y : α), M.Parallel x y ↔ x = y ∧ M.Nonloop x

State before:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ ∀ (x y : α), M.Parallel x y ↔ x = y ∧ M.Nonloop x
Tactic:
exact fun x y ↦ ⟨fun h ↦ ⟨h.eq, h.nonloop_left⟩, by rintro ⟨rfl, h⟩; exact h.parallel_self⟩
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
x y : α
⊢ x = y ∧ M.Nonloop x → M.Parallel x y
Tactic:
rintro ⟨rfl, h⟩
State after:
case intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h✝ : M.Simple
x : α
h : M.Nonloop x
⊢ M.Parallel x x

State before:
case intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h✝ : M.Simple
x : α
h : M.Nonloop x
⊢ M.Parallel x x
Tactic:
exact h.parallel_self
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ M.Loopless
Tactic:
assumption
State after:
no goals