awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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 ∧ (M.Indep (insert e I) → e ∈ I)) → False
Tactic: tauto
-- 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
⊢ 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 ∉ R → False
Tactic: tauto
-- 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
⊢ 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 → ¬M.Indep (insert e I) → M.Indep (insert e I) → insert e I ⊆ R → e ∈ I
Tactic: tauto
-- 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
⊢ 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 → M.Indep (insert e I) → insert e I ⊆ R → e ∈ I
Tactic: tauto
-- 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
⊢ 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 → M.Indep (insert e I) → insert e I ⊆ R → e ∈ I
Tactic: tauto
-- 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
⊢ 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 → ¬M.Indep (insert e I) → e ∉ M.E → False
Tactic: tauto
-- 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
⊢ 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 → ¬M.Indep (insert e I) → ¬(M.Indep (insert e I) → e ∈ I) → False
Tactic: tauto
-- 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
⊢ 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 → ¬insert e I ⊆ R → e ∉ M.E → False
Tactic: tauto
-- 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
⊢ 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 → ¬insert e I ⊆ R → ¬(M.Indep (insert e I) → e ∈ I) → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
X R : Set α
M : Matroid α
hXR : X ⊆ R
hR : R ⊆ M.E
⊢ (M ↾ R).closure X = M.closure X ∩ R
have rw : M.closure (X ∩ R) ∩ R ∪ R \ M.E = M.closure X ∩ R
Tactic: rw [restrict_closure_eq', diff_eq_empty.mpr hR, union_empty, inter_eq_self_of_subset_left hXR]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
X R : Set α
M : Matroid α
hXR : X ⊆ R
hR : R ⊆ M.E
rw : M.closure (X ∩ R) ∩ R ∪ R \ M.E = M.closure X ∩ R
⊢ (M ↾ R).closure X = M.closure X ∩ R
have rw₁ : M.closure (X ∩ R) ∩ R ∪ ∅ = M.closure X ∩ R
Tactic: rw [restrict_closure_eq', diff_eq_empty.mpr hR, union_empty, inter_eq_self_of_subset_left hXR]