awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
rw : B₁.encard.toNat = B₂.ncard
rw₁ : B₂.encard.toNat = B₂.ncard
⊢ B₁.ncard = B₂.ncard
have rw₂ : B₂.ncard = B₂.ncard
Tactic: rw [ncard_def B₁, hB₁.encard_eq_encard_of_isBase hB₂, ← ncard_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B B₁ : Set α
hB : M.IsBase B
h : B.Infinite
hB₁ : M.IsBase B₁
⊢ B₁.Infinite
have contrapose! : ∀ (h : B₁.Finite), B.Finite
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
inst : M.RankPos
hB : M.IsBase B
⊢ B.Nonempty
have rw : B ≠ ∅
Tactic: rw [nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
⊢ M.RankPos
have rw : ¬M.IsBase ∅
Tactic: rw [rankPos_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
he hB₁ : M.IsBase ∅
⊢ False
have h₁ : Set.Nonempty.{u_1} (α := α) ∅
Tactic: obtain rfl := he.eq_of_subset_isBase hB (empty_subset B)
Cleared hypotheses: B, hB, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
inst : M.RankInfinite
h : M.RankFinite
⊢ False
have obtain : ∀ (B : Set α) (hB : M.IsBase B), False
Tactic: obtain ⟨B, hB⟩ := M.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
inst : M.RankFinite
h : M.RankInfinite
⊢ False
have obtain : ∀ (B : Set α) (hB : M.IsBase B), False
Tactic: obtain ⟨B, hB⟩ := M.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ ¬M.RankInfinite ↔ M.RankFinite
have rw : ¬¬M.RankFinite ↔ M.RankFinite
Tactic: rw [← not_rankFinite_iff, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
rw : ¬¬M.RankFinite ↔ M.RankFinite
⊢ ¬M.RankInfinite ↔ M.RankFinite
have rw₁ : M.RankFinite ↔ M.RankFinite
Tactic: rw [← not_rankFinite_iff, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
⊢ M₁ = M₂
have h' : ∀ (B : Set α), M₁.IsBase B ↔ M₂.IsBase B
Tactic: have h' : ∀ B, M₁.IsBase B ↔ M₂.IsBase B :=
    fun B ↦ ⟨fun hB ↦ (h hB.subset_ground).1 hB,
      fun hB ↦ (h <| hB.subset_ground.trans_eq hE.symm).2 hB⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
h' : ∀ (B : Set α), M₁.IsBase B ↔ M₂.IsBase B
⊢ M₁ = M₂
have E : ∀ (x : α), x ∈ M₁.E ↔ x ∈ M₂.E
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
h' : ∀ (B : Set α), M₁.IsBase B ↔ M₂.IsBase B
E : ∀ (x : α), x ∈ M₁.E ↔ x ∈ M₂.E
IsBase : ∀ (x : Set α), M₁.IsBase x ↔ M₂.IsBase x
⊢ M₁ = M₂
have Indep : ∀ (x : Set α), M₁.Indep x ↔ M₂.Indep x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔ Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) B
have simp_rw : M.IsBase (M.E \ B) ↔
  (∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
Tactic: simp_rw [maximal_iff, and_iff_right hB, and_imp, forall_exists_index]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔
    (∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
have refine_1 : ∀ (h : M.IsBase (M.E \ B)) (I : Set α) (hI : I ⊆ M.E) (B' : Set α),
  M.IsBase B' ∧ Disjoint I B' → ∀ (hBI : B ≤ I) (hB' : M.IsBase B') (hIB' : Disjoint I B'), I ≤ B
Tactic: refine ⟨fun h ↦ ⟨⟨_, h, disjoint_sdiff_right⟩,
    fun I hI B' ⟨hB', hIB'⟩ hBI ↦ hBI.antisymm ?_⟩, fun ⟨⟨B', hB', hBB'⟩,h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
refine_1 :
  ∀ (h : M.IsBase (M.E \ B)) (I : Set α) (hI : I ⊆ M.E) (B' : Set α),
    M.IsBase B' ∧ Disjoint I B' → ∀ (hBI : B ≤ I) (hB' : M.IsBase B') (hIB' : Disjoint I B'), I ≤ B
⊢ M.IsBase (M.E \ B) ↔
    (∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
have refine_2 : ((∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y) →
  ∀ (B' : Set α) (hB' : M.IsBase B') (hBB' : Disjoint B B')
    (h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y), M.IsBase (M.E \ B)
Tactic: refine ⟨fun h ↦ ⟨⟨_, h, disjoint_sdiff_right⟩,
    fun I hI B' ⟨hB', hIB'⟩ hBI ↦ hBI.antisymm ?_⟩, fun ⟨⟨B', hB', hBB'⟩,h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
h_1 : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ I ≤ B
have refine_1 : ∀ (hIB' : I ⊆ M.Eᶜ ∪ B), I ≤ B
Tactic: rw [hB'.eq_of_subset_isBase h, ← subset_compl_iff_disjoint_right, diff_eq, compl_inter,
      compl_compl] at hIB'
Cleared hypotheses: hIB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
h_1 : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
refine_1 : ∀ (hIB' : I ⊆ M.Eᶜ ∪ B), I ≤ B
⊢ I ≤ B
have refine_1₁ : B' ⊆ M.E \ B
Tactic: rw [hB'.eq_of_subset_isBase h, ← subset_compl_iff_disjoint_right, diff_eq, compl_inter,
      compl_compl] at hIB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
h_1 : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E \ B
have refine_1 : Disjoint B B'
Tactic: rw [subset_diff, and_iff_right hB'.subset_ground, disjoint_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h_1 :
  (∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
⊢ M.IsBase (M.E \ B)
have refine_2 : M.IsBase (M.E \ (M.E \ B'))
Tactic: rw [h diff_subset B' ⟨hB', disjoint_sdiff_left⟩]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h_1 :
  (∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
refine_2 : M.IsBase (M.E \ (M.E \ B'))
⊢ M.IsBase (M.E \ B)
have refine_2₁ : B ≤ M.E \ B'
Tactic: rw [h diff_subset B' ⟨hB', disjoint_sdiff_left⟩]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ {I : Set α | M.Indep I} = (↑(lowerClosure {B : Set α | M.IsBase B}) : Set (Set α))
have simp_rw : {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B} = (↑(lowerClosure {B : Set α | M.IsBase B}) : Set (Set α))
Tactic: simp_rw [indep_iff, lowerClosure, LowerSet.coe_mk, mem_setOf, le_eq_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
simp_rw : {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B} = (↑(lowerClosure {B : Set α | M.IsBase B}) : Set (Set α))
⊢ {I : Set α | M.Indep I} = (↑(lowerClosure {B : Set α | M.IsBase B}) : Set (Set α))
have simp_rw₁ : {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B} =
  (↑{ carrier := {x : Set α | ∃ (a : Set α), Membership.mem (γ := Set (Set α)) {B : Set α | M.IsBase B} a ∧ x ≤ a},
        lower' := sorry : LowerSet (Set α) } :
    Set (Set α))
Tactic: simp_rw [indep_iff, lowerClosure, LowerSet.coe_mk, mem_setOf, le_eq_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
simp_rw : {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B} = (↑(lowerClosure {B : Set α | M.IsBase B}) : Set (Set α))
simp_rw₁ :
  {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B} =
    (↑{ carrier := {x : Set α | ∃ (a : Set α), Membership.mem (γ := Set (Set α)) {B : Set α | M.IsBase B} a ∧ x ≤ a},
          lower' := ⋯ : LowerSet (Set α) } :
      Set (Set α))
⊢ {I : Set α | M.Indep I} = (↑(lowerClosure {B : Set α | M.IsBase B}) : Set (Set α))
have simp_rw₂ : Eq.{u_1 + 1} (α := Set (Set α)) {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B}
  {x : Set α | ∃ (a : Set α), Membership.mem (γ := Set (Set α)) {B : Set α | M.IsBase B} a ∧ x ≤ a}
Tactic: simp_rw [indep_iff, lowerClosure, LowerSet.coe_mk, mem_setOf, le_eq_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
simp_rw : {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B} = (↑(lowerClosure {B : Set α | M.IsBase B}) : Set (Set α))
simp_rw₁ :
  {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B} =
    (↑{ carrier := {x : Set α | ∃ (a : Set α), Membership.mem (γ := Set (Set α)) {B : Set α | M.IsBase B} a ∧ x ≤ a},
          lower' := ⋯ : LowerSet (Set α) } :
      Set (Set α))
simp_rw₂ :
  Eq.{u_1 + 1} (α := Set (Set α)) {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B}
    {x : Set α | ∃ (a : Set α), Membership.mem (γ := Set (Set α)) {B : Set α | M.IsBase B} a ∧ x ≤ a}
⊢ {I : Set α | M.Indep I} = (↑(lowerClosure {B : Set α | M.IsBase B}) : Set (Set α))
have simp_rw₃ : Eq.{u_1 + 1} (α := Set (Set α)) {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B}
  {x : Set α | ∃ (a : Set α), M.IsBase a ∧ x ≤ a}
Tactic: simp_rw [indep_iff, lowerClosure, LowerSet.coe_mk, mem_setOf, le_eq_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ I ⊆ M.E
have obtain : ∀ (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B), I ⊆ M.E
Tactic: obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.Indep X ∨ M.Dep X
have rw : M.Indep X ∨ ¬M.Indep X
Tactic: rw [Dep, and_iff_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ ¬M.Dep X ↔ M.Indep X
have rw : ¬(¬M.Indep X ∧ X ⊆ M.E) ↔ M.Indep X
Tactic: rw [Dep, and_iff_left hX, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : ¬(¬M.Indep X ∧ X ⊆ M.E) ↔ M.Indep X
⊢ ¬M.Dep X ↔ M.Indep X
have rw₁ : ¬¬M.Indep X ↔ M.Indep X
Tactic: rw [Dep, and_iff_left hX, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : ¬(¬M.Indep X ∧ X ⊆ M.E) ↔ M.Indep X
rw₁ : ¬¬M.Indep X ↔ M.Indep X
⊢ ¬M.Dep X ↔ M.Indep X
have rw₂ : M.Indep X ↔ M.Indep X
Tactic: rw [Dep, and_iff_left hX, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ ¬M.Indep X ↔ M.Dep X
have rw : ¬M.Indep X ↔ ¬M.Indep X ∧ X ⊆ M.E
Tactic: rw [Dep, and_iff_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : ¬M.Indep X ↔ ¬M.Indep X ∧ X ⊆ M.E
⊢ ¬M.Indep X ↔ M.Dep X
have rw₁ : ¬M.Indep X ↔ ¬M.Indep X
Tactic: rw [Dep, and_iff_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ ¬M.Dep I ∧ I ⊆ M.E
have rw : M.Indep I ↔ (I ⊆ M.E → M.Indep I) ∧ I ⊆ M.E
Tactic: rw [dep_iff, not_and, not_imp_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.Indep I
have obtain : ∀ (B : Set α) (hB : M.IsBase B) (hJB : J ⊆ B), M.Indep I
Tactic: obtain ⟨B, hB, hJB⟩ := hJ.exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D.Nonempty
have rw : D ≠ ∅
Tactic: rw [nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hne : I.Nonempty
⊢ M.RankPos
have obtain : ∀ (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B), M.RankPos
Tactic: obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ Maximal M.Indep B
have rw : M.IsBase B ↔ M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
Tactic: rw [maximal_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
have refine : (M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t) →
  ∀ (h : M.Indep B) (h' : ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t), M.IsBase B
Tactic: refine ⟨fun h ↦ ⟨h.indep, fun _ ↦ h.eq_of_subset_indep⟩, fun ⟨h, h'⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h_1 : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
h : M.Indep B
h' : ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → 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_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
h : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → I = J
⊢ M.IsBase I
have rwa : Maximal M.Indep I
Tactic: rwa [isBase_iff_maximal_indep, maximal_subset_iff, and_iff_right hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
h : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → I = J
rwa : Maximal M.Indep I
⊢ M.IsBase I
have rwa₁ : M.Indep I ∧ ∀ ⦃t : Set α⦄, M.Indep t → I ⊆ t → I = t
Tactic: rwa [isBase_iff_maximal_indep, maximal_subset_iff, and_iff_right hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}
have obtain : ∀ (f : α) (hf : f ∈ B' \ B) (hb : M.IsBase (insert f (B \ {e}))), ∃ f ∈ B' \ B, B' = insert f B \ {e}
Tactic: obtain ⟨f, hf, hb⟩ := hB.exchange hB' (h.symm.subset (mem_singleton e))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f (B \ {e}))
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}
have hne : f ≠ e
Tactic: have hne : f ≠ e := by rintro rfl; exact hf.2 (h.symm.subset (mem_singleton f)).1
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f (B \ {e}))
hne : f ≠ e
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}
have hb₁ : M.IsBase (insert f B \ {e})
Tactic: rw [insert_diff_singleton_comm hne] at hb
Cleared hypotheses: hb, hne
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}
have refine : insert f B \ {e} ⊆ B'
Tactic: refine ⟨f, hf, (hb.eq_of_subset_isBase hB' ?_).symm⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ insert f B \ {e} ⊆ B'
have rw : f ∈ B' ∪ {e}
Tactic: rw [diff_subset_iff, insert_subset_iff, union_comm, ← diff_subset_iff, h, and_iff_left rfl.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
⊢ M.IsBase (insert f (B \ {e}))
have obtain : ∀ (B' : Set α) (hB' : M.IsBase B') (hIB' : insert f (B \ {e}) ⊆ B'), M.IsBase (insert f (B \ {e}))
Tactic: obtain ⟨B', hB', hIB'⟩ := hI.exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : insert f (B \ {e}) ⊆ B'
⊢ M.IsBase (insert f (B \ {e}))
have hcard : (B' \ B).encard = (B \ B').encard
Tactic: have hcard := hB'.encard_diff_comm hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : insert f (B \ {e}) ⊆ B'
hcard : (B' \ B).encard = (B \ B').encard
⊢ M.IsBase (insert f (B \ {e}))
have hIB'₁ : f ∈ B' ∧ (B \ B' = ∅ ∨ B \ B' = {e})
Tactic: rw [insert_subset_iff, ← diff_eq_empty, diff_diff_comm, diff_eq_empty, subset_singleton_iff_eq]
    at hIB'
Cleared hypotheses: hIB', hcard
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : f ∈ B' ∧ (B \ B' = ∅ ∨ B \ B' = {e})
hcard : (B' \ B).encard = (B \ B').encard
⊢ M.IsBase (insert f (B \ {e}))
have inl : ∀ (hfB : f ∈ B') (h : B \ B' = ∅), M.IsBase (insert f (B \ {e}))
Tactic: obtain ⟨hfB, (h | h)⟩ := hIB'
Cleared hypotheses: hIB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : f ∈ B' ∧ (B \ B' = ∅ ∨ B \ B' = {e})
hcard : (B' \ B).encard = (B \ B').encard
inl : ∀ (hfB : f ∈ B') (h : B \ B' = ∅), M.IsBase (insert f (B \ {e}))
⊢ M.IsBase (insert f (B \ {e}))
have inr : ∀ (hfB : f ∈ B') (h : B \ B' = {e}), M.IsBase (insert f (B \ {e}))
Tactic: obtain ⟨hfB, (h | h)⟩ := hIB'
Cleared hypotheses: hIB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))
have hcard₁ : ∀ (x : α), x ∉ B' \ B
Tactic: rw [h, encard_empty, encard_eq_zero, eq_empty_iff_forall_notMem] at hcard
Cleared hypotheses: hcard, hfB, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = {e}
⊢ M.IsBase (insert f (B \ {e}))
have hcard₁ : ∃ (x : α), B' \ B = {x}
Tactic: rw [h, encard_singleton, encard_eq_one] at hcard
Cleared hypotheses: hcard, hfB, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : ∃ (x : α), B' \ B = {x}
hfB : f ∈ B'
h : B \ B' = {e}
⊢ M.IsBase (insert f (B \ {e}))
have inr : ∀ (x : α) (hx : B' \ B = {x}), M.IsBase (insert f (B \ {e}))
Tactic: obtain ⟨x, hx⟩ := hcard
Cleared hypotheses: hcard
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
x : α
hx : B' \ B = {x}
⊢ M.IsBase (insert f (B \ {e}))
have hx₁ : B' \ B = {f}
Tactic: obtain (rfl : f = x) := hx.subset ⟨hfB, hf⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
⊢ M.IsBase (insert f B \ {e})
have hfe : f ≠ e
Tactic: have hfe : f ≠ e := ne_of_mem_of_not_mem he hf |>.symm
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
hfe : f ≠ e
⊢ M.IsBase (insert f B \ {e})
have rw : ∀ (hI : M.Indep (insert f (B \ {e}))) (hfe : f ≠ e), M.IsBase (insert f (B \ {e}))
Tactic: rw [← insert_diff_singleton_comm hfe] at *
Cleared hypotheses: hI, hfe
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
⊢ M.IsBase (insert f I)
have inl : ∀ (hf : e ∉ I) (hfI : M.Indep (insert e I)), M.IsBase (insert e I)
Tactic: obtain rfl | hef := eq_or_ne e f
Cleared hypotheses: f, hf, hfI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
inl : ∀ (hf : e ∉ I) (hfI : M.Indep (insert e I)), M.IsBase (insert e I)
⊢ M.IsBase (insert f I)
have inr : ∀ (hef : e ≠ f), M.IsBase (insert f I)
Tactic: obtain rfl | hef := eq_or_ne e f
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e : α
hB : M.IsBase B
h : e ∈ M.E \ B
⊢ M.Dep (insert e B)
have rw : ¬M.Indep (insert e B)
Tactic: rw [← not_indep_iff (insert_subset h.1 hB.subset_ground)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)
have obtain : ∀ (B' : Set α) (hB' : M.IsBase B') (hIB' : I ⊆ B'), ∃ e ∈ B \ I, M.Indep (insert e I)
Tactic: obtain ⟨B', hB', hIB'⟩ := hI.exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)
have obtain : ∀ (x : α) (hxB' : x ∈ B') (hx : x ∉ I), ∃ e ∈ B \ I, M.Indep (insert e I)
Tactic: obtain ⟨x, hxB', hx⟩ := exists_of_ssubset (hIB'.ssubset_of_ne (by (rintro rfl; exact hI' hB')))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)
have pos : ∀ (hxB : x ∈ B), ∃ e ∈ B \ I, M.Indep (insert e I)
Tactic: by_cases hxB : x ∈ B
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
pos : ∀ (hxB : x ∈ B), ∃ e ∈ B \ I, M.Indep (insert e I)
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)
have neg : ∀ (hxB : x ∉ B), ∃ e ∈ B \ I, M.Indep (insert e I)
Tactic: by_cases hxB : x ∈ B