awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
hI₁ : M.Indep (insert f (J \ {e}))
hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX₁ : ⋂₀ Js ⊆ insert f (J \ {e})
heEI₁ : e ∈ M.E \ insert f (J \ {e})
hJI₁ : M.IsBasis J (insert e (insert f (J \ {e})))
⊢ False
have hIb₁ : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
Tactic: obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))
Cleared hypotheses: I, hI, hIs, hiX, heEI, hJI, hIb, hfIJ, hfb
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
hI₁ : M.Indep (insert f (J \ {e}))
hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX₁ : ⋂₀ Js ⊆ insert f (J \ {e})
heEI₁ : e ∈ M.E \ insert f (J \ {e})
hJI₁ : M.IsBasis J (insert e (insert f (J \ {e})))
hIb₁ : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
⊢ False
have hfIJ₁ : f ∈ insert f (J \ {e}) \ J
Tactic: obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))
Cleared hypotheses: I, hI, hIs, hiX, heEI, hJI, hIb, hfIJ, hfb
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
⊢ False
have refine : ∀ (X : Set α) (hX' : X ∈ Js) (hfX : f ∉ X), False
Tactic: refine hfIJ.2 (heJ (mem_insert_of_mem _ fun X hX' ↦ by_contra fun hfX ↦ ?_))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
⊢ False
have inl : ∀ (hd : M.Dep (insert e X)), False
Tactic: obtain (hd | heX) := ((hI.subset (hIs X hX')).mem_closure_iff).mp (he _ hX')
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
inl : ∀ (hd : M.Dep (insert e X)), False
⊢ False
have inr : ∀ (heX : e ∈ X), False
Tactic: obtain (hd | heX) := ((hI.subset (hIs X hX')).mem_closure_iff).mp (he _ hX')
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
⊢ False
have inl : X ⊆ J
Tactic: refine (hJI.indep.subset (insert_subset (heJ (mem_insert _ _)) ?_)).not_dep hd
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
⊢ X ⊆ J
have hIs₁ : X ⊆ insert f (J \ {e})
Tactic: specialize hIs _ hX'
Cleared hypotheses: hIs
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
hIs : X ⊆ insert f (J \ {e})
⊢ X ⊆ J
have hIs₁ : X ⊆ J \ {e}
Tactic: rw [← singleton_union, ← diff_subset_iff, diff_singleton_eq_self hfX] at hIs
Cleared hypotheses: hIs
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ (i : ι), Is i)
⊢ M.closure (⋂ (i : ι), Is i) = ⋂ (i : ι), M.closure (Is i)
have h₁ : Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), M.closure (Is i)) (⋂ J ∈ range Is, M.closure J)
Tactic: convert!
    h.closure_sInter_eq_biInter_closure_of_forall_subset (range_nonempty Is)
      (by simp [subset_iUnion])
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
⊢ M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)
have this : Nonempty.{u_4 + 1} (↑A : Type u_4)
Tactic: have := hA.coe_sort
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty.{u_4 + 1} (↑A : Type u_4)
⊢ M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)
have h₁ : Eq.{u_2 + 1} (α := Set α) (⋂ i ∈ A, I i) (⋂ (i : (↑A : Type u_4)), I (↑i : ι))
Tactic: convert! closure_iInter_eq_iInter_closure_of_iUnion_indep (Is := fun i : A ↦ I i) (by simpa)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty.{u_4 + 1} (↑A : Type u_4)
h₁ : Eq.{u_2 + 1} (α := Set α) (⋂ i ∈ A, I i) (⋂ (i : (↑A : Type u_4)), I (↑i : ι))
⊢ M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)
have h₂ : Eq.{u_2 + 1} (α := Set α) (⋂ i ∈ A, M.closure (I i)) (⋂ (i : (↑A : Type u_4)), M.closure (I (↑i : ι)))
Tactic: convert! closure_iInter_eq_iInter_closure_of_iUnion_indep (Is := fun i : A ↦ I i) (by simpa)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ M.closure (I ∩ J) = M.closure I ∩ M.closure J
have rw : Eq.{u_2 + 1} (α := Set α) (⋂ (i : Bool), M.closure (bif i then I else J))
  (⋂ (b : Bool), bif b then M.closure I else M.closure J)
Tactic: rw [inter_eq_iInter, closure_iInter_eq_iInter_closure_of_iUnion_indep, inter_eq_iInter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
rw :
  Eq.{u_2 + 1} (α := Set α) (⋂ (i : Bool), M.closure (bif i then I else J))
    (⋂ (b : Bool), bif b then M.closure I else M.closure J)
⊢ M.closure (I ∩ J) = M.closure I ∩ M.closure J
have h₁ : M.Indep (⋃ (i : Bool), bif i then I else J)
Tactic: rw [inter_eq_iInter, closure_iInter_eq_iInter_closure_of_iUnion_indep, inter_eq_iInter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ M.IsBasis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)
have refine : ⋂ i ∈ A, X i ⊆ M.closure ((⋂ i ∈ A, X i) ∩ I)
Tactic: refine (hI.inter_left _).isBasis_of_subset_of_subset_closure inter_subset_left ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.closure ((⋂ i ∈ A, X i) ∩ I)
have simp_rw : ∀ (i : ι) (i_1 : i ∈ A), ⋂ i ∈ A, X i ⊆ M.closure (X i ∩ I)
Tactic: simp_rw [← biInter_inter hA,
  closure_biInter_eq_biInter_closure_of_biUnion_indep hA (I := fun i ↦ (X i) ∩ I)
      (hI.subset (by simp)), subset_iInter_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ M.IsBasis ((⋂ (i : ι), X i) ∩ I) (⋂ (i : ι), X i)
have h₁ : Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), X i)
  (⋂ (i : PLift ι), ⋂ (_ : Membership.mem (γ := Set (PLift ι)) univ i), X i.down)
Tactic: convert!
    hI.inter_isBasis_biInter (ι := PLift ι) univ_nonempty (X := fun i ↦ X i.down)
      (by simpa using fun (i : PLift ι) ↦ h i.down)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), X i)
    (⋂ (i : PLift ι), ⋂ (_ : Membership.mem (γ := Set (PLift ι)) univ i), X i.down)
have h₁ : Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), X i) (⋂ (i : PLift ι), X i.down)
Tactic: simp only [mem_univ, iInter_true]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
⊢ M.IsBasis (⋂₀ Xs ∩ I) (⋂₀ Xs)
have rw : M.IsBasis ((⋂ i ∈ Xs, i) ∩ I) (⋂ i ∈ Xs, i)
Tactic: rw [sInter_eq_biInter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (M.closure X) ∧ I ⊆ X
have rw : M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (M.closure (X ∩ M.E)) ∧ I ⊆ X
Tactic: rw [← closure_inter_ground, isBasis'_iff_isBasis_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ ∃ (I : Set α), M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)
have obtain : ∀ (I : Set α) (hI : M.IsBasis I (X ∩ M.E)), ∃ (I : Set α), M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ ∃ (I : Set α), M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)
have hI' : M.IsBasis I (M.closure (X ∩ M.E))
Tactic: have hI' := hI.isBasis_closure_right
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure (X ∩ M.E))
⊢ ∃ (I : Set α), M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)
have hI'₁ : M.IsBasis I (M.closure X)
Tactic: rw [closure_inter_ground] at hI'
Cleared hypotheses: hI'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
⊢ M.IsBasis I Y
have refine : Y ⊆ M.closure I
Tactic: refine hI.indep.isBasis_of_subset_of_subset_closure hY ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
⊢ Y ⊆ M.closure I
have rw : Y ⊆ M.closure Y
Tactic: rw [hI.closure_eq_closure, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis (X ∩ I) X
hI : M.Indep I
⊢ M.IsBasis (M.closure X ∩ I) (M.closure X)
have rw : ∀ (h : X ⊆ M.closure (X ∩ I)) (hI : M.Indep I), M.closure X ⊆ M.closure (M.closure X ∩ I)
Tactic: rw [hI.inter_isBasis_closure_iff_subset_closure_inter] at h ⊢
Cleared hypotheses: h, hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I J : Set α
hI : M.IsBasis I X
hJI : J ⊆ I
hJ : X ⊆ M.closure J
⊢ J = I
have rw : I ⊆ M.closure J
Tactic: rw [← hI.indep.closure_inter_eq_self_of_subset hJI, inter_eq_self_of_subset_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsBasis ∅ X ↔ X ⊆ M.closure ∅
have rw : M.Indep ∅ ∧ X ⊆ M.closure ∅ ∧ ∅ ⊆ X ↔ X ⊆ M.closure ∅
Tactic: rw [isBasis_iff_indep_closure, and_iff_right M.empty_indep, and_iff_left (empty_subset _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
rw : M.Indep ∅ ∧ X ⊆ M.closure ∅ ∧ ∅ ⊆ X ↔ X ⊆ M.closure ∅
⊢ M.IsBasis ∅ X ↔ X ⊆ M.closure ∅
have rw₁ : X ⊆ M.closure ∅ ∧ ∅ ⊆ X ↔ X ⊆ M.closure ∅
Tactic: rw [isBasis_iff_indep_closure, and_iff_right M.empty_indep, and_iff_left (empty_subset _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
rw : M.Indep ∅ ∧ X ⊆ M.closure ∅ ∧ ∅ ⊆ X ↔ X ⊆ M.closure ∅
rw₁ : X ⊆ M.closure ∅ ∧ ∅ ⊆ X ↔ X ⊆ M.closure ∅
⊢ M.IsBasis ∅ X ↔ X ⊆ M.closure ∅
have rw₂ : X ⊆ M.closure ∅ ↔ X ⊆ M.closure ∅
Tactic: rw [isBasis_iff_indep_closure, and_iff_right M.empty_indep, and_iff_left (empty_subset _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
have mpr : (∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})) → M.Indep I
Tactic: use fun h e heI he ↦ ((h.closure_inter_eq_self_of_subset diff_subset).subset ⟨he, heI⟩).2 rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
⊢ M.Indep I
have mpr : ∀ (J : Set α) (hJ : M.IsBasis J I), M.Indep I
Tactic: obtain ⟨J, hJ⟩ := M.exists_isBasis I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
⊢ M.Indep I
have h₁ : I = J
Tactic: convert! hJ.indep
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
⊢ I = J
have h₁ : ∀ (e : α) (he : e ∈ I) (heJ : e ∉ J), e ∈ M.closure (I \ {e})
Tactic: refine hJ.subset.antisymm' (fun e he ↦ by_contra fun heJ ↦ h he ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ M.closure (insert f I \ {e}) = M.closure I
have a : M.closure (insert f I \ {e}) ⊆ M.closure I
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
a : M.closure (insert f I \ {e}) ⊆ M.closure I
⊢ M.closure (insert f I \ {e}) = M.closure I
have a₁ : M.closure I ⊆ M.closure (insert f I \ {e})
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ M.closure (insert f I \ {e}) ⊆ M.closure I
have a : insert f I \ {e} ⊆ M.closure I
Tactic: apply closure_subset_closure_of_subset_closure
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ M.closure I ⊆ M.closure (insert f I \ {e})
have a : I ⊆ M.closure (insert f I \ {e})
Tactic: apply closure_subset_closure_of_subset_closure
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
a : α
haI : a ∈ I
⊢ a ∈ M.closure (insert f I \ {e})
have a₁ : ∀ (he : a ∈ M.closure (insert f I \ {a})), a ∈ M.closure (insert f I \ {a})
Tactic: obtain rfl | ne := eq_or_ne a e
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
a : α
haI : a ∈ I
a₁ : ∀ (he : a ∈ M.closure (insert f I \ {a})), a ∈ M.closure (insert f I \ {a})
⊢ a ∈ M.closure (insert f I \ {e})
have a₂ : ∀ (ne : a ≠ e), a ∈ M.closure (insert f I \ {e})
Tactic: obtain rfl | ne := eq_or_ne a e
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ insert f I
⊢ M.Indep (insert f I \ {e})
have heI₁ : e = f ∨ e ∈ I
Tactic: simp only [mem_insert_iff] at heI
Cleared hypotheses: heI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e = f ∨ e ∈ I
⊢ M.Indep (insert f I \ {e})
have inl : ∀ (hfI : e ∈ M.closure I) (he : e ∈ M.closure (insert e I \ {e})), M.Indep (insert e I \ {e})
Tactic: obtain rfl | heI := heI
Cleared hypotheses: f, hfI, he, heI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e = f ∨ e ∈ I
inl : ∀ (hfI : e ∈ M.closure I) (he : e ∈ M.closure (insert e I \ {e})), M.Indep (insert e I \ {e})
⊢ M.Indep (insert f I \ {e})
have inr : ∀ (heI : e ∈ I), M.Indep (insert f I \ {e})
Tactic: obtain rfl | heI := heI
Cleared hypotheses: heI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
⊢ M.Indep (insert f I \ {e})
have inr : f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
Tactic: rw [Indep.insert_diff_indep_iff (hI.subset (diff_subset ..)) heI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
⊢ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
have inr : ∀ (h : f ∈ M.closure (I \ {e})), e ∈ M.closure (I \ {e})
Tactic: refine .inl ⟨mem_ground_of_mem_closure hfI, fun h ↦ hI.notMem_closure_diff_of_mem heI ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
B : Set α
hB : M.IsBasis B X
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
hfX : f ∈ X
⊢ M.IsBasis (insert f B \ {e}) X
have rw : ∀ (hB : M.Indep B ∧ X ⊆ M.closure B ∧ B ⊆ X) (he : e ∈ M.closure (insert f B \ {e})) (heB : e ∈ insert f B)
  (hfX : f ∈ X), M.Indep (insert f B \ {e}) ∧ X ⊆ M.closure (insert f B \ {e}) ∧ insert f B \ {e} ⊆ X
Tactic: rw [isBasis_iff_indep_closure] at hB ⊢
Cleared hypotheses: hB, he, heB, hfX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
⊢ M.IsBase (insert f B \ {e})
have rw : ∀ (hB : M.IsBasis B M.E) (he : e ∈ M.closure (insert f B \ {e})) (heB : e ∈ insert f B),
  M.IsBasis (insert f B \ {e}) M.E
Tactic: rw [← isBasis_ground_iff] at hB ⊢
Cleared hypotheses: hB, he, heB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
⊢ M.IsBasis (insert f B \ {e}) M.E
have pos : ∀ (hf : f ∈ M.E), M.IsBasis (insert f B \ {e}) M.E
Tactic: by_cases hf : f ∈ M.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
pos : ∀ (hf : f ∈ M.E), M.IsBasis (insert f B \ {e}) M.E
⊢ M.IsBasis (insert f B \ {e}) M.E
have neg : ∀ (hf : f ∉ M.E), M.IsBasis (insert f B \ {e}) M.E
Tactic: by_cases hf : f ∈ M.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
hf : f ∉ M.E
⊢ M.IsBasis (insert f B \ {e}) M.E
have neg : ∀ (he : e ∈ M.closure (insert e B \ {e})) (hf : e ∉ M.E), M.IsBasis (insert e B \ {e}) M.E
Tactic: obtain rfl | heB := heB
Cleared hypotheses: f, he, heB, hf
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
hf : f ∉ M.E
neg : ∀ (he : e ∈ M.closure (insert e B \ {e})) (hf : e ∉ M.E), M.IsBasis (insert e B \ {e}) M.E
⊢ M.IsBasis (insert f B \ {e}) M.E
have neg₁ : ∀ (heB : e ∈ B), M.IsBasis (insert f B \ {e}) M.E
Tactic: obtain rfl | heB := heB
Cleared hypotheses: heB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
hf : f ∉ M.E
heB : e ∈ B
⊢ M.IsBasis (insert f B \ {e}) M.E
have he₁ : e ∈ M.closure (insert f B \ {e} ∩ M.E)
Tactic: rw [← closure_inter_ground] at he
Cleared hypotheses: he, hf, heB