Theorem: Matroid.Indep.restr_simple (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
⊢ (M ↾ I).Simple
Tactic:
simp only [simple_iff_forall_pair_indep, restrict_ground_eq, mem_singleton_iff,
  restrict_indep_iff, pair_subset_iff]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
⊢ ∀ ⦃e f : α⦄, e ∈ I → f ∈ I → M.Indep {e, f} ∧ e ∈ I ∧ f ∈ I

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
⊢ ∀ ⦃e f : α⦄, e ∈ I → f ∈ I → M.Indep {e, f} ∧ e ∈ I ∧ f ∈ I
Tactic:
rintro e f he hf
State after:
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
hI : M.Indep I
e f : α
he : e ∈ I
hf : f ∈ I
⊢ M.Indep {e, f} ∧ e ∈ I ∧ f ∈ I

State before:
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
hI : M.Indep I
e f : α
he : e ∈ I
hf : f ∈ I
⊢ M.Indep {e, f} ∧ e ∈ I ∧ f ∈ I
Tactic:
exact ⟨hI.subset (pair_subset he hf), he, hf⟩
State after:
no goals