awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mpr₁ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₂ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₃ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₄ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₅ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I)
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mpr₆ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → e ∈ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mpr₁ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₂ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₃ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₄ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₅ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I)
mpr₆ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → e ∈ M.E
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mpr₇ : e ∈ I → e ∉ I → ¬M.Indep (insert e I)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mpr₁ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₂ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₃ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₄ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₅ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I)
mpr₆ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → e ∈ M.E
mpr₇ : e ∈ I → e ∉ I → ¬M.Indep (insert e I)
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mpr₈ : e ∈ I → e ∉ I → e ∈ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mpr₁ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₂ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₃ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₄ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₅ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I)
mpr₆ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → e ∈ M.E
mpr₇ : e ∈ I → e ∉ I → ¬M.Indep (insert e I)
mpr₈ : e ∈ I → e ∉ I → e ∈ M.E
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mp₇ : e ∈ I → ¬¬M.Indep (insert e I) → e ∈ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mpr₁ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₂ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₃ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₄ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₅ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I)
mpr₆ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → e ∈ M.E
mpr₇ : e ∈ I → e ∉ I → ¬M.Indep (insert e I)
mpr₈ : e ∈ I → e ∉ I → e ∈ M.E
mp₇ : e ∈ I → ¬¬M.Indep (insert e I) → e ∈ I
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mp₈ : e ∈ I → e ∉ M.E → e ∈ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mpr₁ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₂ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₃ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₄ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₅ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I)
mpr₆ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → e ∈ M.E
mpr₇ : e ∈ I → e ∉ I → ¬M.Indep (insert e I)
mpr₈ : e ∈ I → e ∉ I → e ∈ M.E
mp₇ : e ∈ I → ¬¬M.Indep (insert e I) → e ∈ I
mp₈ : e ∈ I → e ∉ M.E → e ∈ I
mp₉ : e ∈ I → ¬¬M.Indep (insert e I) → e ∈ I
mp₁₀ : e ∈ I → e ∉ M.E → e ∈ I
mp₁₁ : e ∈ I → ¬¬M.Indep (insert e I) → e ∈ I
mp₁₂ : e ∈ I → e ∉ M.E → e ∈ I
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mp₁₃ : ¬M.Indep (insert e I) → e ∈ M.E → ¬¬M.Indep (insert e I) → e ∈ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mpr₁ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₂ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₃ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₄ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₅ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I)
mpr₆ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → e ∈ M.E
mpr₇ : e ∈ I → e ∉ I → ¬M.Indep (insert e I)
mpr₈ : e ∈ I → e ∉ I → e ∈ M.E
mp₇ : e ∈ I → ¬¬M.Indep (insert e I) → e ∈ I
mp₈ : e ∈ I → e ∉ M.E → e ∈ I
mp₉ : e ∈ I → ¬¬M.Indep (insert e I) → e ∈ I
mp₁₀ : e ∈ I → e ∉ M.E → e ∈ I
mp₁₁ : e ∈ I → ¬¬M.Indep (insert e I) → e ∈ I
mp₁₂ : e ∈ I → e ∉ M.E → e ∈ I
mp₁₃ : ¬M.Indep (insert e I) → e ∈ M.E → ¬¬M.Indep (insert e I) → e ∈ I
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mp₁₄ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ M.E → e ∈ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
⊢ M.IsBasis (⋃ (i : ι), I i) (⋃ (i : ι), X i)
have refine : ∀ (e : α), Membership.mem (γ := Set α) ((⋃ (i : ι), X i) \ ⋃ (i : ι), I i) e → M.Dep (insert e (⋃ (i : ι), I i))
Tactic: refine h_ind.isBasis_of_forall_insert
    (iUnion_subset (fun i ↦ (hI i).subset.trans (subset_iUnion _ _))) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
e : α
he' : e ∉ ⋃ (i : ι), I i
i : ι
hes : e ∈ X i
⊢ M.Dep (insert e (⋃ (i : ι), I i))
have rw : ∀ (he' : ∀ (x : ι), e ∉ I x) (i : ι) (hes : e ∈ X i), M.Dep (insert e (⋃ (i : ι), I i))
Tactic: rw [mem_iUnion, not_exists] at he'
Cleared hypotheses: he', i, hes
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ M.Dep (insert e (⋃ (i : ι), I i))
have refine : insert e (⋃ (i : ι), I i) ⊆ M.E
Tactic: refine ((hI i).insert_dep ⟨hes, he' _⟩).superset (insert_subset_insert (subset_iUnion _ _)) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ insert e (⋃ (i : ι), I i) ⊆ M.E
have rw : e ∈ M.E
Tactic: rw [insert_subset_iff, iUnion_subset_iff, and_iff_left (fun i ↦ (hI i).indep.subset_ground)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.IsBasis I (⋃ (i : ι), X i)
have h : I = ⋃ (i : ι), I
Tactic: convert! IsBasis.iUnion_isBasis_iUnion X (fun _ ↦ I) (fun i ↦ hI i) _
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
h : I = ⋃ (i : ι), I
⊢ M.IsBasis I (⋃ (i : ι), X i)
have convert! : M.Indep (⋃ (i : ι), (fun (x : ι) ↦ I) i)
Tactic: convert! IsBasis.iUnion_isBasis_iUnion X (fun _ ↦ I) (fun i ↦ hI i) _
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ I = ⋃ (i : ι), I
have h : I = I
Tactic: rw [iUnion_const]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep (⋃ (i : ι), (fun (x : ι) ↦ I) i)
have rw : M.Indep I
Tactic: rw [iUnion_const]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
⊢ M.IsBasis I (⋃₀ Xs)
have rw : M.IsBasis I (⋃ (i : (↑Xs : Type u_1)), (↑i : Set α))
Tactic: rw [sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
⊢ M.IsBasis I (⋃ (i : (↑Xs : Type u_1)), (↑i : Set α))
have this : Nonempty.{u_1 + 1} (↑Xs : Type u_1)
Tactic: have := Iff.mpr nonempty_coe_sort hne
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I {x : α | M.IsBasis I (insert x I)}
have refine_1 : ∀ (e : α) (he : e ∈ I), M.IsBasis I (insert e I)
Tactic: refine hI.isBasis_of_forall_insert (fun e he ↦ (?_ : M.IsBasis _ _))
    (fun e he ↦ ⟨fun hu ↦ he.2 ?_, he.1.subset_ground⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
refine_1 : ∀ (e : α) (he : e ∈ I), M.IsBasis I (insert e I)
⊢ M.IsBasis I {x : α | M.IsBasis I (insert x I)}
have refine_2 : ∀ (e : α) (he : e ∈ {x : α | M.IsBasis I (insert x I)} \ I) (hu : M.Indep (insert e I)), e ∈ I
Tactic: refine hI.isBasis_of_forall_insert (fun e he ↦ (?_ : M.IsBasis _ _))
    (fun e he ↦ ⟨fun hu ↦ he.2 ?_, he.1.subset_ground⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
⊢ M.IsBasis I (insert e I)
have refine_1 : M.IsBasis I I
Tactic: rw [insert_eq_of_mem he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis (I ∪ J) (X ∪ Y)
have rw : M.IsBasis (⋃ (b : Bool), bif b then I else J) (⋃ (b : Bool), bif b then X else Y)
Tactic: rw [union_eq_iUnion, union_eq_iUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis (⋃ (b : Bool), bif b then I else J) (⋃ (b : Bool), bif b then X else Y)
have refine_1 : ∀ (i : Bool), M.IsBasis (bif i then I else J) (bif i then X else Y)
Tactic: refine IsBasis.iUnion_isBasis_iUnion _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
refine_1 : ∀ (i : Bool), M.IsBasis (bif i then I else J) (bif i then X else Y)
⊢ M.IsBasis (⋃ (b : Bool), bif b then I else J) (⋃ (b : Bool), bif b then X else Y)
have refine_2 : M.Indep (⋃ (i : Bool), bif i then I else J)
Tactic: refine IsBasis.iUnion_isBasis_iUnion _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ ∀ (i : Bool), M.IsBasis (bif i then I else J) (bif i then X else Y)
have refine_1 : M.IsBasis J Y ∧ M.IsBasis I X
Tactic: simp only [Bool.forall_bool, cond_false, cond_true]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.IsBasis I (X ∪ Y)
have h : I = I ∪ I
Tactic: convert! hIX.union_isBasis_union hIY _
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
h : I = I ∪ I
⊢ M.IsBasis I (X ∪ Y)
have convert! : M.Indep (I ∪ I)
Tactic: convert! hIX.union_isBasis_union hIY _
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ I = I ∪ I
have h : I = I
Tactic: rw [union_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep (I ∪ I)
have rw : M.Indep I
Tactic: rw [union_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.IsBasis J (J ∪ X)
have h : J = J ∪ I
Tactic: convert! hJ.isBasis_self.union_isBasis_union hI _
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
h : J = J ∪ I
⊢ M.IsBasis J (J ∪ X)
have convert! : M.Indep (J ∪ I)
Tactic: convert! hJ.isBasis_self.union_isBasis_union hI _
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ J = J ∪ I
have h : J = J
Tactic: rw [union_eq_self_of_subset_right hIJ]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
h : M.Indep (insert e I)
⊢ M.IsBasis (insert e I) (insert e X)
have simp_rw : ∀ (h : M.Indep (I ∪ {e})), M.IsBasis (I ∪ {e}) (X ∪ {e})
Tactic: simp_rw [← union_singleton] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
⊢ M.IsBase I
have by_contra : ∀ (h : ¬M.IsBase I), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
h : ¬M.IsBase I
⊢ False
have obtain : ∀ (e : α) (heBI : e ∈ B \ I) (he : M.Indep (insert e I)), False
Tactic: obtain ⟨e, heBI, he⟩ := hIX.indep.exists_insert_of_not_isBase h hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hB : M.IsBase B
⊢ ∃ (B' : Set α), M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B
have obtain : ∀ (B' : Set α) (hB' : M.IsBasis B' (I ∪ B)) (hIB' : I ⊆ B'), ∃ (B' : Set α), M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B
Tactic: obtain ⟨B', hB', hIB'⟩ := hI.subset_isBasis_of_subset <| subset_union_left (t := B)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
hIJ : I ⊆ J
hJ : M.Indep J
⊢ J ∩ X = I
have rw : J ∩ X = J ∩ (X ∩ M.E)
Tactic: rw [← hI.isBasis_inter_ground.inter_eq_of_subset_indep hIJ hJ, inter_comm X, ← inter_assoc,
    inter_eq_self_of_subset_left hJ.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
hIJ : I ⊆ J
hJ : M.Indep J
rw : J ∩ X = J ∩ (X ∩ M.E)
⊢ J ∩ X = I
have rw₁ : J ∩ X = J ∩ (M.E ∩ X)
Tactic: rw [← hI.isBasis_inter_ground.inter_eq_of_subset_indep hIJ hJ, inter_comm X, ← inter_assoc,
    inter_eq_self_of_subset_left hJ.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
hIJ : I ⊆ J
hJ : M.Indep J
rw : J ∩ X = J ∩ (X ∩ M.E)
rw₁ : J ∩ X = J ∩ (M.E ∩ X)
⊢ J ∩ X = I
have rw₂ : J ∩ X = J ∩ M.E ∩ X
Tactic: rw [← hI.isBasis_inter_ground.inter_eq_of_subset_indep hIJ hJ, inter_comm X, ← inter_assoc,
    inter_eq_self_of_subset_left hJ.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
hIJ : I ⊆ J
hJ : M.Indep J
rw : J ∩ X = J ∩ (X ∩ M.E)
rw₁ : J ∩ X = J ∩ (M.E ∩ X)
rw₂ : J ∩ X = J ∩ M.E ∩ X
⊢ J ∩ X = I
have rw₃ : J ∩ X = J ∩ X
Tactic: rw [← hI.isBasis_inter_ground.inter_eq_of_subset_indep hIJ hJ, inter_comm X, ← inter_assoc,
    inter_eq_self_of_subset_left hJ.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
⊢ M.IsBasis B X
have rw : ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J
Tactic: rw [isBasis_iff, and_iff_right hB.indep, and_iff_right hBX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J
have obtain : ∀ (I I' : Set α) (hI : M.IsBasis I X) (hI' : M.IsBasis I' Y) (hII' : I ⊆ I'),
  ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J
Tactic: obtain ⟨I, I', hI, hI', hII'⟩ := M.exists_isBasis_subset_isBasis hXY
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ M.IsBasis (I ∪ I' \ I) Y
have rwa : M.IsBasis (I ∪ I') Y
Tactic: rwa [union_diff_self, union_eq_self_of_subset_left hII']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J
have refine : Disjoint X (I' \ I)
Tactic: refine ⟨I, I' \ I, hI, by rwa [union_diff_self, union_eq_self_of_subset_left hII'], ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ Disjoint X (I' \ I)
have rw : ∀ ⦃a : α⦄, a ∈ X → ∀ ⦃b : α⦄, b ∈ I' \ I → a ≠ b
Tactic: rw [disjoint_iff_forall_ne]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
⊢ Function.Injective f
have refine : ∀ (M M' : Matroid α) (hMM' : f M = f M'), M = M'
Tactic: refine fun M M' hMM' ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
M M' : Matroid α
hMM' : f M = f M'
⊢ M = M'
have hMM'₁ : M.E = M'.E ∧
  ∀ (x : Set α),
    Membership.mem (γ := Set (Set α)) {B : Set α | M.IsBase B} x ↔
      Membership.mem (γ := Set (Set α)) {B : Set α | M'.IsBase B} x
Tactic: rw [Prod.mk.injEq, and_comm, Set.ext_iff, and_comm] at hMM'
Cleared hypotheses: hMM'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
⊢ Set.Finite.{u_1} (α := Matroid α) {M : Matroid α | M.E ⊆ E}
have hf : Function.Injective f
Tactic: have hf : f.Injective := by
    refine fun M M' hMM' ↦ ?_
    rw [Prod.mk.injEq, and_comm, Set.ext_iff, and_comm] at hMM'
    exact ext_isBase hMM'.1 (fun B _ ↦ hMM'.2 B)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
hf : Function.Injective f
⊢ Set.Finite.{u_1} (α := Matroid α) {M : Matroid α | M.E ⊆ E}
have rw : (f '' {M : Matroid α | M.E ⊆ E}).Finite
Tactic: rw [← Set.finite_image_iff hf.injOn]