-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
mp :
  (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mpr :
  ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R →
    ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₁ mp₂ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X →
      M.Indep I →
        I ⊆ R → ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mp₃ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → M.Indep I
mp₄ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ X
mp₅ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ R
mp₆ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X → M.Indep I → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y
mp₇ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ R
mpr₁ mpr₂ :
  I ⊆ R →
    (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) →
      M.Indep I →
        I ⊆ X → I ⊆ R → ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mpr₃ : I ⊆ R → (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) → M.Indep I → I ⊆ X → I ⊆ R → M.Indep I
mpr₄ : I ⊆ R → (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) → M.Indep I → I ⊆ X → I ⊆ R → I ⊆ R
mpr₅ : I ⊆ R → (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) → M.Indep I → I ⊆ X → I ⊆ R → I ⊆ X
mpr₆ :
  I ⊆ R →
    (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) →
      M.Indep I → I ⊆ X → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₈ mp₉ mp₁₀ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X → M.Indep I → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y
mpr₇ mpr₈ mpr₉ :
  I ⊆ R →
    (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) →
      M.Indep I → I ⊆ X → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₁₁ mp₁₂ mp₁₃ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X → M.Indep I → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y
mpr₁₀ mpr₁₁ mpr₁₂ :
  I ⊆ R →
    (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) →
      M.Indep I → I ⊆ X → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₁₄ mp₁₅ mp₁₆ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X → M.Indep I → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y
mpr₁₃ mpr₁₄ mpr₁₅ :
  I ⊆ R →
    (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) →
      M.Indep I → I ⊆ X → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₁₇ mp₁₈ mp₁₉ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X → M.Indep I → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y
mpr₁₆ mpr₁₇ mpr₁₈ :
  I ⊆ R →
    (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) →
      M.Indep I → I ⊆ X → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₂₀ mp₂₁ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X → M.Indep I → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y
mpr₁₉ mpr₂₀ :
  I ⊆ R →
    (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) →
      M.Indep I → I ⊆ X → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R

Tactic:
tauto