awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
s t : Finset X
inst_1 : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
simp : ∀ ⦃a : Numbering X⦄, a.IsPrefix s → ¬a.IsPrefix t
⊢ Disjoint (α := Finset (Numbering X)) (prefixed s) (prefixed t)

Tactic:
simp only [Finset.disjoint_left, mem_prefixed]

Premises used: Numbering.mem_prefixed, Finset.disjoint_left
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
s t : Finset X
inst_1 : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
inl : ∀ (hst' : #s ≤ #t), False
inr : ∀ (hts' : #t ≤ #s), False
⊢ False

Tactic:
obtain hst' | hts' := Nat.le_total #s #t

Premises used: Nat.le_total, Finset.card
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
s t : Finset X
inst_1 : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
hst' : #s ≤ #t
⊢ False

Tactic:
hst <| hs.subset_of_card_le_card ht hst'

Premises used: Numbering.IsPrefix.subset_of_card_le_card
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
s t : Finset X
inst_1 : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
hst' : #s ≤ #t
⊢ False

Tactic:
exact hst <| hs.subset_of_card_le_card ht hst'

Premises used: Numbering.IsPrefix.subset_of_card_le_card
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
s t : Finset X
inst_1 : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
hts' : #t ≤ #s
⊢ False

Tactic:
hts <| ht.subset_of_card_le_card hs hts'

Premises used: Numbering.IsPrefix.subset_of_card_le_card
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
s t : Finset X
inst_1 : DecidableEq X
hst : ¬s ⊆ t
hts : ¬t ⊆ s
f : Numbering X
hs : f.IsPrefix s
ht : f.IsPrefix t
hts' : #t ≤ #s
⊢ False

Tactic:
exact hts <| ht.subset_of_card_le_card hs hts'

Premises used: Numbering.IsPrefix.subset_of_card_le_card
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
⊢ Nonempty.{max 1 (u_1 + 1)} { B : Set α // M.IsBase B }

Tactic:
nonempty_subtype.2 M.exists_isBase

Premises used: Iff.mpr, nonempty_subtype, Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.Nonempty
⊢ M.E.Nonempty

Tactic:
Nonempty.ground_nonempty

Premises used: Matroid.Nonempty.ground_nonempty
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
⊢ M.E.Nonempty ↔ M.Nonempty

Tactic:
⟨fun h ↦ ⟨h⟩, fun ⟨h⟩ ↦ h⟩

Premises used: Matroid.E, _private.0.Matroid.ground_nonempty_iff.match_1, Set.Nonempty, Iff.intro, Matroid.Nonempty.mk
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
h : M.Nonempty
⊢ Nonempty α

Tactic:
⟨M.ground_nonempty.some⟩

Premises used: Matroid.ground_nonempty, Nonempty.intro, Set.Nonempty.some
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.Finite
⊢ M.E.Finite

Tactic:
Finite.ground_finite

Premises used: Matroid.Finite.ground_finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.Finite
X : Set α
hX : X ⊆ M.E
⊢ X.Finite

Tactic:
M.ground_finite.subset hX

Premises used: Set.Finite.subset, Matroid.ground_finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 : Matroid α
inst : Finite α
M : Matroid α
⊢ M.Finite

Tactic:
⟨Set.toFinite _⟩

Premises used: Matroid.Finite.mk, Set.toFinite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
inst : M.Finite
⊢ M.RankFinite

Tactic:
⟨M.exists_isBase.imp (fun B hB ↦ ⟨hB, M.set_finite B (M.subset_ground _ hB)⟩)⟩

Premises used: Matroid.subset_ground, Matroid.RankFinite.mk, Exists.imp, Matroid.exists_isBase, And.intro, Matroid.set_finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
inst : M.RankPos
obtain : ∀ (B : Set α) (hB : M.IsBase B), M.Nonempty
⊢ M.Nonempty

Tactic:
obtain ⟨B, hB⟩ := M.exists_isBase

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
inst : M.RankPos
B : Set α
hB : M.IsBase B
inl : ∀ (hB : M.IsBase ∅), M.Nonempty
inr : ∀ (e : α) (heB : e ∈ B), M.Nonempty
⊢ M.Nonempty

Tactic:
obtain rfl | ⟨e, heB⟩ := B.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
inst : M.RankPos
hB : M.IsBase ∅
⊢ M.Nonempty

Tactic:
False.elim <| RankPos.empty_not_isBase hB

Premises used: False.elim, Matroid.RankPos.empty_not_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
inst : M.RankPos
hB : M.IsBase ∅
⊢ M.Nonempty

Tactic:
exact False.elim <| RankPos.empty_not_isBase hB

Premises used: False.elim, Matroid.RankPos.empty_not_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
inst : M.RankPos
B : Set α
hB : M.IsBase B
e : α
heB : e ∈ B
⊢ M.Nonempty

Tactic:
⟨e, M.subset_ground B hB heB ⟩

Premises used: Matroid.subset_ground, Exists.intro, Matroid.Nonempty.mk
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
inst : M.RankPos
B : Set α
hB : M.IsBase B
e : α
heB : e ∈ B
⊢ M.Nonempty

Tactic:
exact ⟨e, M.subset_ground B hB heB ⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B B' : Set α
exch : ExchangeProperty IsBase
hB : IsBase B
hB' : IsBase B'
h : B ⊆ B'
⊢ B = B'

Tactic:
h.antisymm (fun x hx ↦ by_contra
    (fun hxB ↦ let ⟨_, hy, _⟩ := exch B' B hB' hB x ⟨hx, hxB⟩; hy.2 <| h hy.1))

Premises used: False, _private.0.Matroid.ExchangeProperty.antichain.match_1, And.right, And.left, HasSubset.Subset.antisymm, And.intro, by_contra
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
inl : ∀ (he : B₂ \ B₁ = ∅), (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
inr : ∀ (hinf : (B₂ \ B₁).encard = ⊤), (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
inr₁ :
  ∀ (e : α) (he : e ∈ B₂ \ B₁) (hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard),
    (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

Tactic:
obtain (he | hinf | ⟨e, he, hcard⟩) :=
    (B₂ \ B₁).eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt

Premises used: Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt, SDiff.sdiff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
he : B₂ \ B₁ = ∅
inl inl₁ : (B₁ \ B₁).encard ≤ (B₁ \ B₁).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

Tactic:
rw [exch.antichain hB₂ hB₁ (diff_eq_empty.mp he)]

Premises used: Matroid.ExchangeProperty.antichain, Iff.mp, Set.diff_eq_empty
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
hinf : (B₂ \ B₁).encard = ⊤
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

Tactic:
le_top.trans_eq hinf.symm

Premises used: LE.le.trans_eq, le_top, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
hinf : (B₂ \ B₁).encard = ⊤
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

Tactic:
exact le_top.trans_eq hinf.symm

Premises used: LE.le.trans_eq, le_top, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
inr : ∀ (f : α) (hf : f ∈ B₁ \ B₂) (hB' : IsBase (insert f (B₂ \ {e}))), (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

Tactic:
obtain ⟨f, hf, hB'⟩ := exch B₂ B₁ hB₂ hB₁ e he
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
rw : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
⊢ (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard

Tactic:
rw [insert_diff_of_mem _ hf.1, diff_diff_comm]

Premises used: Set.insert_diff_of_mem, Set.diff_diff_comm, And.left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
⊢ ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard

Tactic:
hcard
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
⊢ ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard

Tactic:
exact hcard
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
⊢ (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard

Tactic:
have : encard (insert f (B₂ \ {e}) \ B₁) < encard (B₂ \ B₁) := by
    rw [insert_diff_of_mem _ hf.1, diff_diff_comm]; exact hcard
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
⊢ (B₁ \ insert f (B₂ \ {e})).encard ≤ (insert f (B₂ \ {e}) \ B₁).encard

Tactic:
have hencard := encard_diff_le_aux exch hB₁ hB'
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
hencard : (B₁ \ insert f (B₂ \ {e})).encard ≤ (insert f (B₂ \ {e}) \ B₁).encard
⊢ ((B₁ \ B₂) \ {f}).encard ≤ ((B₂ \ B₁) \ {e}).encard

Tactic:
rw [insert_diff_of_mem _ hf.1, diff_diff_comm, ← union_singleton, ← diff_diff, diff_diff_right,
    inter_singleton_eq_empty.mpr he.2, union_empty] at hencard

Premises used: Iff.mpr, Set.union_empty, Set.inter_singleton_eq_empty, Set.insert_diff_of_mem, Set.diff_diff_comm, Set.diff_diff, And.right, And.left, Set.union_singleton, Set.diff_diff_right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
hencard : ((B₁ \ B₂) \ {f}).encard ≤ ((B₂ \ B₁) \ {e}).encard
inr : ((B₁ \ B₂) \ {f}).encard + 1 ≤ ((B₂ \ B₁) \ {e}).encard + 1
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

Tactic:
rw [← encard_diff_singleton_add_one he, ← encard_diff_singleton_add_one hf]

Premises used: Set.encard_diff_singleton_add_one
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
hencard : ((B₁ \ B₂) \ {f}).encard ≤ ((B₂ \ B₁) \ {e}).encard
⊢ ((B₁ \ B₂) \ {f}).encard + 1 ≤ ((B₂ \ B₁) \ {e}).encard + 1

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
⊢ (B₁ \ B₂).encard = (B₂ \ B₁).encard

Tactic:
(encard_diff_le_aux exch hB₁ hB₂).antisymm (encard_diff_le_aux exch hB₂ hB₁)

Premises used: LE.le.antisymm, Matroid.ExchangeProperty.encard_diff_le_aux
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
rw : (B₁ \ B₂).encard + (B₁ ∩ B₂).encard = B₂.encard
rw₁ : (B₂ \ B₁).encard + (B₁ ∩ B₂).encard = B₂.encard
rw₂ : (B₂ \ B₁).encard + (B₂ ∩ B₁).encard = B₂.encard
rw₃ rw₄ : B₂.encard = B₂.encard
⊢ B₁.encard = B₂.encard

Tactic:
rw [← encard_diff_add_encard_inter B₁ B₂, exch.encard_diff_eq hB₁ hB₂, inter_comm,
    encard_diff_add_encard_inter]

Premises used: Set.inter_comm, Set.encard_diff_add_encard_inter, Matroid.ExchangeProperty.encard_diff_eq
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : X ⊆ M.E
⊢ X ∩ Y ⊆ M.E

Tactic:
inter_subset_left.trans hX

Premises used: HasSubset.Subset.trans, Set.inter_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : X ⊆ M.E
⊢ Y ∩ X ⊆ M.E

Tactic:
inter_subset_right.trans hX

Premises used: HasSubset.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : X ⊆ M.E
⊢ X \ Y ⊆ M.E

Tactic:
diff_subset.trans hX

Premises used: Set.diff_subset, HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.E \ X ⊆ M.E

Tactic:
diff_subset_ground rfl.subset

Premises used: _private.0.Matroid.diff_subset_ground, Eq.subset, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ {e} ⊆ M.E

Tactic:
singleton_subset_iff.mpr he

Premises used: Iff.mpr, Set.singleton_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ X ⊆ M.E

Tactic:
hXY.trans hY

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
hX : X ⊆ M.E
heX : e ∈ X
⊢ e ∈ M.E

Tactic:
hX heX
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
e : α
X : Set α
M : Matroid α
he : e ∈ M.E
hX : X ⊆ M.E
⊢ insert e X ⊆ M.E

Tactic:
insert_subset he hX

Premises used: Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
⊢ M.E ⊆ M.E

Tactic:
rfl.subset

Premises used: Eq.subset, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B ⊆ M.E

Tactic:
M.subset_ground B hB

Premises used: Matroid.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
e : α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
hx : e ∈ B₁ \ B₂
⊢ ∃ y ∈ B₂ \ B₁, M.IsBase (insert y (B₁ \ {e}))

Tactic:
M.isBase_exchange B₁ B₂ hB₁ hB₂ _ hx

Premises used: Matroid.isBase_exchange
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
e : α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
hxB₁ : e ∈ B₁
hxB₂ : e ∉ B₂
⊢ ∃ (y : α), (y ∈ B₂ ∧ y ∉ B₁) ∧ M.IsBase (insert y (B₁ \ {e}))

Tactic:
simpa using hB₁.exchange hB₂ ⟨hxB₁, hxB₂⟩

Premises used: Matroid.IsBase.exchange, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
hB₁B₂ : B₁ ⊆ B₂
⊢ B₁ = B₂

Tactic:
M.isBase_exchange.antichain hB₁ hB₂ hB₁B₂

Premises used: Matroid.ExchangeProperty.antichain, Matroid.isBase_exchange
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : X ⊂ B
⊢ ¬M.IsBase X

Tactic:
fun h ↦ hX.ne (h.eq_of_subset_isBase hB hX.subset)

Premises used: HasSSubset.SSubset.subset, Matroid.IsBase.eq_of_subset_isBase, HasSSubset.SSubset.ne, Not
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e : α
hB : M.IsBase B
heB : e ∉ B
⊢ ¬M.IsBase (insert e B)

Tactic:
fun h ↦ h.not_isBase_of_ssubset (ssubset_insert heB) hB

Premises used: Set.ssubset_insert, Matroid.IsBase.not_isBase_of_ssubset, Not
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ (B₁ \ B₂).encard = (B₂ \ B₁).encard

Tactic:
M.isBase_exchange.encard_diff_eq hB₁ hB₂

Premises used: Matroid.isBase_exchange, Matroid.ExchangeProperty.encard_diff_eq
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
rw : (B₁ \ B₂).encard.toNat = (B₂ \ B₁).ncard
rw₁ : (B₂ \ B₁).encard.toNat = (B₂ \ B₁).ncard
rw₂ rw₃ : (B₂ \ B₁).ncard = (B₂ \ B₁).ncard
⊢ (B₁ \ B₂).ncard = (B₂ \ B₁).ncard

Tactic:
rw [ncard_def, hB₁.encard_diff_comm hB₂, ← ncard_def]

Premises used: Matroid.IsBase.encard_diff_comm, Set.ncard_def
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
rw rw₁ : B₂.encard = B₂.encard
⊢ B₁.encard = B₂.encard

Tactic:
rw [M.isBase_exchange.encard_isBase_eq hB₁ hB₂]

Premises used: Matroid.ExchangeProperty.encard_isBase_eq, Matroid.isBase_exchange
-- Module: Mathlib.Combinatorics.Matroid.Basic
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
rw₂ rw₃ : B₂.ncard = B₂.ncard
⊢ B₁.ncard = B₂.ncard

Tactic:
rw [ncard_def B₁, hB₁.encard_eq_encard_of_isBase hB₂, ← ncard_def]

Premises used: Set.ncard_def, Matroid.IsBase.encard_eq_encard_of_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B B' : Set α
hB : M.IsBase B
h : B.Finite
hB' : M.IsBase B'
⊢ B'.Finite

Tactic:
(finite_iff_finite_of_encard_eq_encard (hB.encard_eq_encard_of_isBase hB')).mp h

Premises used: Set.finite_iff_finite_of_encard_eq_encard, Matroid.IsBase.encard_eq_encard_of_isBase, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B B₁ : Set α
hB : M.IsBase B
h : B.Infinite
hB₁ : M.IsBase B₁
contrapose! : ∀ (h : B₁.Finite), B.Finite
⊢ B₁.Infinite

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B B₁ : Set α
hB : M.IsBase B
hB₁ : M.IsBase B₁
h : B₁.Finite
⊢ B.Finite

Tactic:
hB₁.finite_of_finite h hB

Premises used: Matroid.IsBase.finite_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B B₁ : Set α
hB : M.IsBase B
hB₁ : M.IsBase B₁
h : B₁.Finite
⊢ B.Finite

Tactic:
exact hB₁.finite_of_finite h hB

Premises used: Matroid.IsBase.finite_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
inst : M.RankFinite
hB : M.IsBase B
⊢ B.Finite

Tactic:
let ⟨_, hB₀⟩ := ‹RankFinite M›.exists_finite_isBase
  hB₀.1.finite_of_finite hB₀.2 hB

Premises used: Set.Finite, And.right, And.left, Matroid.RankFinite.exists_finite_isBase, _private.0.Matroid.IsBase.finite.match_1, Matroid.IsBase.finite_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
inst : M.RankInfinite
hB : M.IsBase B
⊢ B.Infinite

Tactic:
let ⟨_, hB₀⟩ := ‹RankInfinite M›.exists_infinite_isBase
  hB₀.1.infinite_of_infinite hB₀.2 hB

Premises used: Matroid.RankInfinite.exists_infinite_isBase, _private.0.Matroid.IsBase.infinite.match_1, And.right, And.left, Matroid.IsBase.infinite_of_infinite, Set.Infinite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
h : M.RankPos
⊢ ¬M.IsBase ∅

Tactic:
h.empty_not_isBase

Premises used: Matroid.RankPos.empty_not_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
inst : M.RankPos
hB : M.IsBase B
rw : B ≠ ∅
⊢ B.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.RankPos
hB : M.IsBase ∅
⊢ False

Tactic:
M.empty_not_isBase hB

Premises used: Matroid.empty_not_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.RankPos
hB : M.IsBase ∅
⊢ False

Tactic:
exact M.empty_not_isBase hB

Premises used: Matroid.empty_not_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
rw : ¬M.IsBase ∅
⊢ M.RankPos

Tactic:
rw [rankPos_iff]

Premises used: Matroid.rankPos_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
he : M.IsBase ∅
⊢ M.IsBase ∅

Tactic:
obtain rfl := he.eq_of_subset_isBase hB (empty_subset B)

Premises used: Matroid.IsBase.eq_of_subset_isBase, Set.empty_subset, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
he hB₁ : M.IsBase ∅
⊢ Set.Nonempty.{u_1} (α := α) ∅

Tactic:
obtain rfl := he.eq_of_subset_isBase hB (empty_subset B)

Premises used: Matroid.IsBase.eq_of_subset_isBase, Set.empty_subset, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
he hB : M.IsBase ∅
h : Set.Nonempty.{u_1} (α := α) ∅
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
hfin : B.Finite
⊢ M.RankFinite

Tactic:
⟨⟨B, hB, hfin⟩⟩

Premises used: Matroid.RankFinite.mk, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Infinite
⊢ M.RankInfinite

Tactic:
⟨⟨B, hB, h⟩⟩

Premises used: Matroid.RankInfinite.mk, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.RankInfinite
h : M.RankFinite
obtain : ∀ (B : Set α) (hB : M.IsBase B), False
⊢ False

Tactic:
obtain ⟨B, hB⟩ := M.exists_isBase

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.RankInfinite
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ False

Tactic:
hB.infinite hB.finite

Premises used: Matroid.IsBase.infinite, Matroid.IsBase.finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.RankInfinite
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ False

Tactic:
exact hB.infinite hB.finite

Premises used: Matroid.IsBase.infinite, Matroid.IsBase.finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.RankFinite
h : M.RankInfinite
obtain : ∀ (B : Set α) (hB : M.IsBase B), False
⊢ False

Tactic:
obtain ⟨B, hB⟩ := M.exists_isBase

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.RankFinite
h : M.RankInfinite
B : Set α
hB : M.IsBase B
⊢ False

Tactic:
hB.infinite hB.finite

Premises used: Matroid.IsBase.infinite, Matroid.IsBase.finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.RankFinite
h : M.RankInfinite
B : Set α
hB : M.IsBase B
⊢ False

Tactic:
exact hB.infinite hB.finite

Premises used: Matroid.IsBase.infinite, Matroid.IsBase.finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
⊢ M.RankFinite ∨ M.RankInfinite

Tactic:
let ⟨B, hB⟩ := M.exists_isBase
  B.finite_or_infinite.imp hB.rankFinite_of_finite hB.rankInfinite_of_infinite

Premises used: Set.finite_or_infinite, Matroid.RankInfinite, Matroid.IsBase.rankFinite_of_finite, Matroid.IsBase.rankInfinite_of_infinite, Matroid.exists_isBase, Or, Or.imp, Matroid.RankFinite, _private.0.Matroid.rankFinite_or_rankInfinite.match_1
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
h : M.RankFinite
⊢ ¬¬M.RankFinite

Tactic:
simpa