Theorem: Matroid.restrict_parallel_iff (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D R : Set α
⊢ (M ↾ R).Parallel e f ↔ M.Parallel e f ∧ e ∈ R ∧ f ∈ R
Tactic:
simp only [parallel_iff_nonloop_nonloop_indep_imp_eq, restrict_nonloop_iff, restrict_indep_iff,
  pair_subset_iff, and_imp]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D R : Set α
⊢ (M.Nonloop e ∧ e ∈ R) ∧ (M.Nonloop f ∧ f ∈ R) ∧ (M.Indep {e, f} → e ∈ R → f ∈ R → e = f) ↔
    (M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)) ∧ e ∈ R ∧ f ∈ R

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D R : Set α
⊢ (M.Nonloop e ∧ e ∈ R) ∧ (M.Nonloop f ∧ f ∈ R) ∧ (M.Indep {e, f} → e ∈ R → f ∈ R → e = f) ↔
    (M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)) ∧ e ∈ R ∧ f ∈ R
Tactic:
aesop
State after:
no goals