-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
he : ¬M.Indep (insert e I)
neg :
  e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) →
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
neg₁ :
  (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E →
    e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I)
neg₂ neg₃ :
  e ∈ R →
    (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) →
      (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
neg₄ :
  e ∈ R →
    (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) → ¬((e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R) → e ∈ R
neg₅ :
  e ∈ R →
    (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) → ¬((e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R) → e ∉ M.E
neg₆ : e ∈ R → e ∈ M.E → (M.Indep (insert e I) → e ∈ I) → e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I)
neg₇ : e ∈ R → e ∉ M.E → e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I)
neg₈ : e ∈ R → e ∈ M.E → (M.Indep (insert e I) → e ∈ I) → e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I)
neg₉ : e ∈ R → e ∉ M.E → e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I)
neg₁₀ : e ∈ R → e ∈ M.E → (M.Indep (insert e I) → e ∈ I) → e ∈ R
neg₁₁ : e ∈ R → e ∈ M.E → (M.Indep (insert e I) → e ∈ I) → M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I
neg₁₂ : e ∈ R → e ∉ M.E → e ∈ R
neg₁₃ : e ∈ R → e ∉ M.E → M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I
neg₁₄ : e ∈ R → e ∈ M.E → ¬(M.Indep (insert e I) ∧ insert e I ⊆ R) → ¬(e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) → False
neg₁₅ : e ∈ R → e ∈ M.E → ¬(M.Indep (insert e I) ∧ insert e I ⊆ R) → e ∉ R → False
neg₁₆ : e ∈ R → e ∈ M.E → e ∈ I → ¬(e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) → False
neg₁₇ : e ∈ R → e ∈ M.E → e ∈ I → e ∉ R → False
neg₁₈ : e ∈ R → e ∈ M.E → ¬(M.Indep (insert e I) ∧ insert e I ⊆ R) → ¬(e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) → False
neg₁₉ : e ∈ R → e ∈ M.E → e ∈ I → ¬(e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) → False
neg₂₀ : e ∈ R → e ∈ M.E → ¬(M.Indep (insert e I) ∧ insert e I ⊆ R) → ¬(e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) → False
neg₂₁ : e ∈ R → e ∈ M.E → e ∈ I → ¬(e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) → False
neg₂₂ : e ∈ R → e ∈ M.E → ¬M.Indep (insert e I) → M.Indep (insert e I) → insert e I ⊆ R → e ∈ I
neg₂₃ : e ∈ R → e ∈ M.E → e ∈ I → M.Indep (insert e I) → insert e I ⊆ R → e ∈ I
neg₂₄ : e ∈ R → e ∉ M.E → M.Indep (insert e I) → insert e I ⊆ R → e ∈ I
neg₂₅ : e ∈ R → e ∈ M.E → ¬M.Indep (insert e I) → e ∉ M.E → False
neg₂₆ : e ∈ R → e ∈ M.E → ¬M.Indep (insert e I) → ¬(M.Indep (insert e I) → e ∈ I) → False
neg₂₇ : e ∈ R → e ∈ M.E → ¬insert e I ⊆ R → e ∉ M.E → False
neg₂₈ : e ∈ R → e ∈ M.E → ¬insert e I ⊆ R → ¬(M.Indep (insert e I) → e ∈ I) → False
neg₂₉ : e ∈ R → e ∈ M.E → ¬M.Indep (insert e I) → ¬(M.Indep (insert e I) → e ∈ I) → False
neg₃₀ : e ∈ R → e ∈ M.E → ¬insert e I ⊆ R → ¬(M.Indep (insert e I) → e ∈ I) → False
neg₃₁ : e ∈ R → e ∈ M.E → ¬M.Indep (insert e I) → ¬(M.Indep (insert e I) → e ∈ I) → False
neg₃₂ : e ∈ R → e ∈ M.E → ¬insert e I ⊆ R → ¬(M.Indep (insert e I) → e ∈ I) → False
⊢ e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
have neg₃₃ : e ∈ R → e ∈ M.E → e ∈ I → e ∉ M.E → False
Tactic: tauto