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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D E : Set α
⊢ (uniqueBaseOn I E).Simple ↔ E ⊆ I
Tactic:
simp only [simple_iff_forall_pair_indep, uniqueBaseOn_ground, uniqueBaseOn_indep_iff',
  subset_inter_iff, pair_subset_iff]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D E : Set α
⊢ (∀ ⦃e f : α⦄, e ∈ E → f ∈ E → (e ∈ I ∧ f ∈ I) ∧ e ∈ E ∧ f ∈ E) ↔ E ⊆ I

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D E : Set α
⊢ (∀ ⦃e f : α⦄, e ∈ E → f ∈ E → (e ∈ I ∧ f ∈ I) ∧ e ∈ E ∧ f ∈ E) ↔ E ⊆ I
Tactic:
exact ⟨fun h e heE ↦ (h heE heE).1.1, by tauto⟩
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D E : Set α
⊢ E ⊆ I → ∀ ⦃e f : α⦄, e ∈ E → f ∈ E → (e ∈ I ∧ f ∈ I) ∧ e ∈ E ∧ f ∈ E
Tactic:
tauto
State after:
no goals