awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
rw : M.Coindep I ↔ M'✶.Indep I
⊢ M✶.Indep I ↔ M'✶.Indep I
have rw₁ : M.Coindep I ↔ M'.Coindep I
Tactic: rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
rw : M.Coindep I ↔ M'✶.Indep I
rw₁ : M.Coindep I ↔ M'.Coindep I
⊢ M✶.Indep I ↔ M'✶.Indep I
have rw₂ : M.Spanning (M.E \ I) ↔ M'.Coindep I
Tactic: rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
rw : M.Coindep I ↔ M'✶.Indep I
rw₁ : M.Coindep I ↔ M'.Coindep I
rw₂ : M.Spanning (M.E \ I) ↔ M'.Coindep I
⊢ M✶.Indep I ↔ M'✶.Indep I
have rw₃ : M.Spanning (M.E \ I) ↔ M'.Spanning (M'.E \ I)
Tactic: rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
rw : M.Coindep I ↔ M'✶.Indep I
rw₁ : M.Coindep I ↔ M'.Coindep I
rw₂ : M.Spanning (M.E \ I) ↔ M'.Coindep I
rw₃ : M.Spanning (M.E \ I) ↔ M'.Spanning (M'.E \ I)
⊢ M✶.Indep I ↔ M'✶.Indep I
have rw₄ : M'.Spanning (M.E \ I) ↔ M'.Spanning (M'.E \ I)
Tactic: rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
rw : M.Coindep I ↔ M'✶.Indep I
rw₁ : M.Coindep I ↔ M'.Coindep I
rw₂ : M.Spanning (M.E \ I) ↔ M'.Coindep I
rw₃ : M.Spanning (M.E \ I) ↔ M'.Spanning (M'.E \ I)
rw₄ : M'.Spanning (M.E \ I) ↔ M'.Spanning (M'.E \ I)
⊢ M✶.Indep I ↔ M'✶.Indep I
have rw₅ : M'.Spanning (M'.E \ I) ↔ M'.Spanning (M'.E \ I)
Tactic: rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ Minimal M.Spanning B
have rw : M.IsBase B ↔ M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
Tactic: rw [minimal_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
have refine : (M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t) →
  ∀ (h : M.Spanning B) (h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t), M.IsBase B
Tactic: refine ⟨fun h ↦ ⟨h.spanning, fun _ ↦ h.eq_of_superset_spanning⟩, fun ⟨h, h'⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
B : Set α
h_1 : M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
h : M.Spanning B
h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
⊢ M.IsBase B
have obtain : ∀ (B' : Set α) (hB' : M.IsBase B') (hBB' : B' ⊆ B), M.IsBase B
Tactic: obtain ⟨B', hB', hBB'⟩ := h.exists_isBase_subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
hX : M.Spanning X
h : ∀ ⦃Y : Set α⦄, M.Spanning Y → Y ⊆ X → X = Y
⊢ M.IsBase X
have rwa : Minimal M.Spanning X
Tactic: rwa [isBase_iff_minimal_spanning, minimal_subset_iff, and_iff_right hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
hX : M.Spanning X
h : ∀ ⦃Y : Set α⦄, M.Spanning Y → Y ⊆ X → X = Y
rwa : Minimal M.Spanning X
⊢ M.IsBase X
have rwa₁ : M.Spanning X ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ X → X = t
Tactic: rwa [isBase_iff_minimal_spanning, minimal_subset_iff, and_iff_right hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X R : Set α
⊢ (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E
have obtain : ∀ (I : Set α) (hI : (M ↾ R).IsBasis' I X), (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E
Tactic: obtain ⟨I, hI⟩ := (M ↾ R).exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
⊢ (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E
have hI' : M.IsBasis' I (X ∩ R)
Tactic: obtain ⟨hI', hIR⟩ := isBasis'_restrict_iff.1 hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
⊢ (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E
have hIR : I ⊆ R
Tactic: obtain ⟨hI', hIR⟩ := isBasis'_restrict_iff.1 hI
-- 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
⊢ (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E
have h : ∀ (e : α), e ∈ (M ↾ R).closure X ↔ e ∈ M.closure (X ∩ R) ∩ R ∪ R \ M.E
Tactic: ext e
-- 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 : α
⊢ e ∈ (M ↾ R).closure X ↔ e ∈ M.closure (X ∩ R) ∩ R ∪ R \ M.E
have h : 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
Tactic: rw [← hI.closure_eq_closure, ← hI'.closure_eq_closure, hI.indep.mem_closure_iff', mem_union,
    mem_inter_iff, hI'.indep.mem_closure_iff', restrict_ground_eq, restrict_indep_iff, mem_diff]
-- 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 : α
⊢ 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 pos : ∀ (he : M.Indep (insert 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
Tactic: by_cases he : M.Indep (insert e I)
-- 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 : α
pos :
  ∀ (he : M.Indep (insert 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
⊢ 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 : ∀ (he : ¬M.Indep (insert 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
Tactic: by_cases he : M.Indep (insert e I)
-- 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)
⊢ 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 ∧ (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
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
⊢ 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 ∈ 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)
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)
⊢ 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 →
  (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
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
⊢ 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 → (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
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
⊢ 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 →
  (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
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
⊢ 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 ∈ I) → e ∈ R ∧ (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)
⊢ 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 ∈ R ∧ (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)
⊢ 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 ∈ I) → e ∈ R
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
⊢ 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 ∈ 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
⊢ 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 ∈ R
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
⊢ 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
⊢ 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 ∈ 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
⊢ 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 ∉ R → False
Tactic: tauto