awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.eRk X < M.eRk Y
hz : ¬Y ∩ M.E ⊆ M.closure X
e : α
heX : e ∉ M.closure X
heZ : e ∈ Y
heE : e ∈ M.E
⊢ ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1

Tactic:
⟨e, ⟨heZ, fun heX' ↦ heX (mem_closure_of_mem' _ heX')⟩, eRk_insert_eq_add_one ⟨heE, heX⟩⟩

Premises used: Matroid.mem_closure_of_mem', And.intro, Exists.intro, Matroid.eRk_insert_eq_add_one
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.eRk X < M.eRk Y
hz : ¬Y ∩ M.E ⊆ M.closure X
e : α
heX : e ∉ M.closure X
heZ : e ∈ Y
heE : e ∈ M.E
⊢ ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1

Tactic:
refine ⟨e, ⟨heZ, fun heX' ↦ heX (mem_closure_of_mem' _ heX')⟩, eRk_insert_eq_add_one ⟨heE, heX⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (Insert.insert e X) ≤ M.eRk X
⊢ M.closure X = M.closure Y

Tactic:
hX.closure_eq_closure_of_subset_of_eRk_ge_eRk hXY <| not_lt.1 fun hlt ↦ ?_

Premises used: not_lt, Iff.mp, Matroid.IsRkFinite.closure_eq_closure_of_subset_of_eRk_ge_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (Insert.insert e X) ≤ M.eRk X
refine : ∀ (hlt : M.eRk X < M.eRk Y), False
⊢ M.closure X = M.closure Y

Tactic:
refine hX.closure_eq_closure_of_subset_of_eRk_ge_eRk hXY <| not_lt.1 fun hlt ↦ ?_

Premises used: not_lt, Iff.mp, Matroid.IsRkFinite.closure_eq_closure_of_subset_of_eRk_ge_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (Insert.insert e X) ≤ M.eRk X
hlt : M.eRk X < M.eRk Y
obtain : ∀ (z : α) (hz : z ∈ Y \ X) (hr : M.eRk (Insert.insert z X) = M.eRk X + 1), False
⊢ False

Tactic:
obtain ⟨z, hz, hr⟩ := exists_eRk_insert_eq_add_one_of_lt hlt

Premises used: Matroid.exists_eRk_insert_eq_add_one_of_lt
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (Insert.insert e X) ≤ M.eRk X
hlt : M.eRk X < M.eRk Y
z : α
hz : z ∈ Y \ X
hr : M.eRk (Insert.insert z X) = M.eRk X + 1
⊢ False

Tactic:
simpa [hr, ENat.add_one_le_iff hX.eRk_lt_top.ne] using hY z hz

Premises used: ENat.add_one_le_iff, Matroid.IsRkFinite.eRk_lt_top, LT.lt.ne
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
pos : ∀ (hX : M.IsRkFinite X), M.eRk X = M.eRk Y
neg : ∀ (hX : ¬M.IsRkFinite X), M.eRk X = M.eRk Y
⊢ M.eRk X = M.eRk Y

Tactic:
by_cases hX : M.IsRkFinite X

Premises used: Matroid.IsRkFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : M.IsRkFinite X
pos : M.eRk (M.closure X) = M.eRk Y
pos₁ : M.eRk (M.closure Y) = M.eRk Y
pos₂ pos₃ : M.eRk Y = M.eRk Y
⊢ M.eRk X = M.eRk Y

Tactic:
rw [← eRk_closure_eq, hX.closure_eq_closure_of_subset_of_forall_insert hXY hY, eRk_closure_eq]

Premises used: Matroid.IsRkFinite.closure_eq_closure_of_subset_of_forall_insert, Matroid.eRk_closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : ¬M.IsRkFinite X
neg : ⊤ = M.eRk Y
neg₁ neg₂ : Eq (α := ℕ∞) ⊤ ⊤
⊢ M.eRk X = M.eRk Y

Tactic:
rw [eRk_eq_top_iff.2 hX, eRk_eq_top_iff.2 (mt (fun h ↦ h.subset hXY) hX)]

Premises used: Iff.mpr, Matroid.IsRkFinite.subset, mt, Matroid.eRk_eq_top_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.Indep I
rw rw₁ : I.encard = I.encard
⊢ M.eRk I = I.encard

Tactic:
rw [h.eRk_eq_encard]

Premises used: Matroid.Indep.eRk_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
refine : ∀ (h : M.eRk I = I.encard), M.Indep I
⊢ M.Indep I ↔ M.eRk I = I.encard

Tactic:
refine ⟨fun h ↦ by rw [h.eRk_eq_encard], fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
obtain : ∀ (J : Set α) (hJ : M.IsBasis' J I), M.Indep I
⊢ M.Indep I

Tactic:
obtain ⟨J, hJ⟩ := M.exists_isBasis' I

Premises used: Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
rw : M.Indep J
rw₁ : I.encard ≤ J.encard
⊢ M.Indep I

Tactic:
rw [← hI.eq_of_subset_of_encard_le' hJ.subset]

Premises used: Set.Finite.eq_of_subset_of_encard_le', Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
⊢ M.Indep J

Tactic:
hJ.indep

Premises used: Matroid.IsBasis'.indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
⊢ M.Indep J

Tactic:
exact hJ.indep

Premises used: Matroid.IsBasis'.indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
rw : M.eRk I ≤ J.encard
rw₁ rw₂ : M.eRk I ≤ M.eRk I
⊢ I.encard ≤ J.encard

Tactic:
rw [← h, ← hJ.eRk_eq_encard]

Premises used: Matroid.IsBasis'.eRk_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
⊢ M.Indep I ↔ M.eRk I = I.encard

Tactic:
⟨Indep.eRk_eq_encard, fun h ↦ ?_⟩

Premises used: Matroid.Indep.eRk_eq_encard, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
refine : ∀ (h : M.eRk I = I.encard), M.Indep I
⊢ M.Indep I ↔ M.eRk I = I.encard

Tactic:
refine ⟨Indep.eRk_eq_encard, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
h : M.eRk I = I.encard
inl : ∀ (hfin : I.Finite), M.Indep I
inr : ∀ (hinf : I.Infinite), M.Indep I
⊢ M.Indep I

Tactic:
obtain hfin | hinf := I.finite_or_infinite

Premises used: Set.finite_or_infinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
h : M.eRk I = I.encard
hfin : I.Finite
inl inl₁ inl₂ inl₃ : M.eRk I = I.encard
⊢ M.Indep I

Tactic:
rwa [indep_iff_eRk_eq_encard_of_finite hfin]

Premises used: Matroid.indep_iff_eRk_eq_encard_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
h : M.eRk I = I.encard
hinf : I.Infinite
⊢ M.eRk I = ⊤

Tactic:
rw [hinf.encard_eq] at h

Premises used: Set.Infinite.encard_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
h : M.eRk I = I.encard
hinf : I.Infinite
h₁ : M.eRk I = ⊤
⊢ I.Infinite

Tactic:
rw [hinf.encard_eq] at h

Premises used: Set.Infinite.encard_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
h : M.eRk I = ⊤
hinf : I.Infinite
⊢ M.Indep I

Tactic:
False.elim <| (M.isRkFinite_set I).eRk_lt_top.ne h

Premises used: False.elim, Matroid.isRkFinite_set, Matroid.IsRkFinite.eRk_lt_top, LT.lt.ne
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
h : M.eRk I = ⊤
hinf : I.Infinite
⊢ M.Indep I

Tactic:
exact False.elim <| (M.isRkFinite_set I).eRk_lt_top.ne h

Premises used: False.elim, Matroid.isRkFinite_set, Matroid.IsRkFinite.eRk_lt_top, LT.lt.ne
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
rw : M.eRk I = I.encard
rw₁ : I.Finite
⊢ M.Indep I

Tactic:
rw [indep_iff_eRk_eq_encard_of_finite _]

Premises used: Matroid.indep_iff_eRk_eq_encard_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
⊢ M.eRk I = I.encard

Tactic:
(M.eRk_le_encard I).antisymm h

Premises used: LE.le.antisymm, Matroid.eRk_le_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
⊢ M.eRk I = I.encard

Tactic:
exact (M.eRk_le_encard I).antisymm h

Premises used: LE.le.antisymm, Matroid.eRk_le_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
⊢ I.Finite

Tactic:
simpa using h.trans_lt hX.eRk_lt_top

Premises used: Matroid.IsRkFinite.eRk_lt_top, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : X.Finite
hX : M.Dep X
⊢ M.eRk X < X.encard

Tactic:
lt_of_le_of_ne (M.eRk_le_encard X) fun h' ↦
    ((indep_iff_eRk_eq_encard_of_finite h).mpr h').not_dep hX

Premises used: Iff.mpr, Matroid.indep_iff_eRk_eq_encard_of_finite, Matroid.Indep.not_dep, Matroid.eRk_le_encard, lt_of_le_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
⊢ M.eRk X < X.encard ↔ M.Dep X

Tactic:
⟨fun h ↦ ?_, fun h ↦ eRk_lt_encard_of_dep_of_finite hX h⟩

Premises used: Matroid.eRk_lt_encard_of_dep_of_finite, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
refine : ∀ (h : M.eRk X < X.encard), M.Dep X
⊢ M.eRk X < X.encard ↔ M.Dep X

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ eRk_lt_encard_of_dep_of_finite hX h⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
h : M.eRk X < X.encard
rw : ¬M.eRk X = X.encard
⊢ M.Dep X

Tactic:
rw [← not_indep_iff, indep_iff_eRk_eq_encard_of_finite hX]

Premises used: Matroid.indep_iff_eRk_eq_encard_of_finite, Matroid.not_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
h : M.eRk X < X.encard
⊢ ¬M.eRk X = X.encard

Tactic:
h.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
h : M.eRk X < X.encard
⊢ ¬M.eRk X = X.encard

Tactic:
exact h.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
hX : M.Dep X
⊢ M.eRk X < X.encard

Tactic:
(M.eRk_le_encard X).lt_of_ne ?_

Premises used: LE.le.lt_of_ne, Matroid.eRk_le_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
hX : M.Dep X
refine : M.eRk X ≠ X.encard
⊢ M.eRk X < X.encard

Tactic:
refine (M.eRk_le_encard X).lt_of_ne ?_

Premises used: LE.le.lt_of_ne, Matroid.eRk_le_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
hX : M.Dep X
rw : ¬M.Indep X
⊢ M.eRk X ≠ X.encard

Tactic:
rw [ne_eq, ← indep_iff_eRk_eq_encard]

Premises used: ne_eq, Matroid.indep_iff_eRk_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
hX : M.Dep X
⊢ ¬M.Indep X

Tactic:
hX.not_indep

Premises used: Matroid.Dep.not_indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
hX : M.Dep X
⊢ ¬M.Indep X

Tactic:
exact hX.not_indep

Premises used: Matroid.Dep.not_indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
hXE : X ⊆ M.E
⊢ M.eRk X < X.encard ↔ M.Dep X

Tactic:
⟨fun h ↦ (not_indep_iff).1 fun hi ↦ h.ne hi.eRk_eq_encard, Dep.eRk_lt_encard⟩

Premises used: Matroid.Indep.eRk_eq_encard, Iff.intro, Iff.mp, Matroid.Dep.eRk_lt_encard, Matroid.not_indep_iff, LT.lt.ne
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : I.encard < J.encard
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
augment hI hJ hcard

Premises used: Matroid.Indep.augment
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
⊢ M.IsBasis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X

Tactic:
⟨fun h ↦ ⟨h.subset,h.indep, h.eRk_eq_encard.symm⟩, fun ⟨hIX, hI, hcard⟩ ↦ ?_⟩

Premises used: Matroid.IsBasis', Matroid.IsBasis'.eRk_eq_encard, Matroid.IsBasis'.indep, _private.0.Matroid.isBasis'_iff_indep_encard_eq_of_finite.match_1, And.intro, Iff.intro, Matroid.IsBasis'.subset, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
refine :
  I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X → ∀ (hIX : I ⊆ X) (hI : M.Indep I) (hcard : I.encard = M.eRk X), M.IsBasis' I X
⊢ M.IsBasis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X

Tactic:
refine ⟨fun h ↦ ⟨h.subset,h.indep, h.eRk_eq_encard.symm⟩, fun ⟨hIX, hI, hcard⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
h : I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.eRk X
obtain : ∀ (J : Set α) (hJ : M.IsBasis' J X) (hIJ : I ⊆ J), M.IsBasis' I X
⊢ M.IsBasis' I X

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis'_of_subset hIX

Premises used: Matroid.Indep.subset_isBasis'_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
h : I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.eRk X
J : Set α
hJ : M.IsBasis' J X
hIJ : I ⊆ J
rwa rwa₁ rwa₂ rwa₃ : M.IsBasis' J X
⊢ M.IsBasis' I X

Tactic:
rwa [hIfin.eq_of_subset_of_encard_le hIJ (hJ.encard_eq_eRk.trans hcard.symm).le]

Premises used: Matroid.IsBasis'.encard_eq_eRk, Eq.le, Eq.symm, Set.Finite.eq_of_subset_of_encard_le, Eq.trans
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
hX : X ⊆ M.E
rw : M.IsBasis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
rw₁ rw₂ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
⊢ M.IsBasis I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X

Tactic:
rw [← isBasis'_iff_isBasis, isBasis'_iff_indep_encard_eq_of_finite hIfin]

Premises used: Matroid.isBasis'_iff_isBasis, Matroid.isBasis'_iff_indep_encard_eq_of_finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIfin : I.Finite
hIX : I ⊆ X
h : M.eRk X ≤ M.eRk I
rw : I.encard = M.eRk I
rw₁ rw₂ : I.encard = I.encard
⊢ I.encard = M.eRk X

Tactic:
rw [h.antisymm (M.eRk_mono hIX), hI.eRk_eq_encard]

Premises used: Matroid.eRk_mono, Matroid.Indep.eRk_eq_encard, LE.le.antisymm
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIfin : I.Finite
hIX : I ⊆ X
h : M.eRk X ≤ M.eRk I
hX : X ⊆ M.E
⊢ M.IsBasis I X

Tactic:
(hI.isBasis'_of_eRk_ge hIfin hIX h).isBasis

Premises used: Matroid.Indep.isBasis'_of_eRk_ge, Matroid.IsBasis'.isBasis
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hIfin : I.Finite
h : M.eRank ≤ M.eRk I
⊢ M.IsBase I

Tactic:
simpa using hI.isBasis_of_eRk_ge hIfin hI.subset_ground (M.eRk_ground.trans_le h)

Premises used: Matroid.Indep.isBasis_of_eRk_ge, Eq.trans_le, Matroid.eRk_ground, Matroid.Indep.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
obtain : ∀ (I : Set α) (hI : M.IsBasis I C), M.eRk C + 1 = C.encard
⊢ M.eRk C + 1 = C.encard

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis C

Premises used: Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
I : Set α
hI : M.IsBasis I C
obtain :
  ∀ (e : α) (heI : e ∉ I) (hC : M.IsCircuit (insert e I)) (hI : M.IsBasis I (insert e I)) (heC : e ∈ insert e I),
    M.eRk (insert e I) + 1 = (insert e I).encard
⊢ M.eRk C + 1 = C.encard

Tactic:
obtain ⟨e, ⟨heC, heI⟩, rfl⟩ := hC.isBasis_iff_insert_eq.1 hI

Premises used: Iff.mp, rfl, Matroid.IsCircuit.isBasis_iff_insert_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
heI : e ∉ I
hC : M.IsCircuit (insert e I)
hI : M.IsBasis I (insert e I)
heC : e ∈ insert e I
rw : I.encard + 1 = (insert e I).encard
rw₁ rw₂ : I.encard + 1 = I.encard + 1
⊢ M.eRk (insert e I) + 1 = (insert e I).encard

Tactic:
rw [hI.eRk_eq_encard, encard_insert_of_notMem heI]

Premises used: Matroid.IsBasis.eRk_eq_encard, Set.encard_insert_of_notMem
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
rw : M.eRk (M.closure {e}) = 0
rw₁ : M.eRk M.loops = 0
rw₂ : M.eRk (M.closure ∅) = 0
rw₃ : M.eRk ∅ = 0
rw₄ rw₅ : Eq (α := ℕ∞) 0 0
⊢ M.eRk {e} = 0

Tactic:
rw [← eRk_closure_eq, he.closure, loops, eRk_closure_eq, eRk_empty]

Premises used: Matroid.eRk_empty, Matroid.IsLoop.closure, Matroid.loops, Matroid.eRk_closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
rw : encard (α := α) {e} = 1
rw₁ rw₂ : Eq (α := ℕ∞) 1 1
⊢ M.eRk {e} = 1

Tactic:
rw [← he.indep.isBasis_self.encard_eq_eRk, encard_singleton]

Premises used: Matroid.IsBasis.encard_eq_eRk, Set.encard_singleton, Matroid.IsNonloop.indep, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
inst : M.Loopless
he : e ∈ M.E
⊢ M.eRk {e} = 1

Tactic:
(M.isNonloop_of_loopless he).eRk_eq

Premises used: Matroid.IsNonloop.eRk_eq, Matroid.isNonloop_of_loopless
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.eRk {e} ≤ 1

Tactic:
(M.eRk_le_encard {e}).trans_eq <| encard_singleton e

Premises used: LE.le.trans_eq, Matroid.eRk_le_encard, Singleton.singleton, Set.encard_singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.eRk {e} = 1 ↔ M.IsNonloop e

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.eRk_eq⟩

Premises used: Matroid.IsNonloop.eRk_eq, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
refine : ∀ (h : M.eRk {e} = 1), M.IsNonloop e
⊢ M.eRk {e} = 1 ↔ M.IsNonloop e

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.eRk_eq⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.eRk {e} = 1
⊢ Set.Finite (α := α) {e}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.eRk {e} = 1
rwa : M.Indep {e}
rwa₁ : M.eRk {e} = encard (α := α) {e}
rwa₂ rwa₃ rwa₄ rwa₅ : M.eRk {e} = 1
⊢ M.IsNonloop e

Tactic:
rwa [← indep_singleton, indep_iff_eRk_eq_encard_of_finite (by simp), encard_singleton]

Premises used: Matroid.indep_iff_eRk_eq_encard_of_finite, Matroid.indep_singleton, Set.encard_singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.eRk X = 1 ↔ ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}

Tactic:
⟨?_, fun ⟨e, heX, he, hXe⟩ ↦ ?_⟩

Premises used: Iff.intro, Matroid.eRk, OfNat.ofNat, Eq, _private.0.Matroid.eRk_eq_one_iff.match_1
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
refine_1 : M.eRk X = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
refine_2 :
  (∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}) →
    ∀ (e : α) (heX : e ∈ X) (he : M.IsNonloop e) (hXe : X ⊆ M.closure {e}), M.eRk X = 1
⊢ M.eRk X = 1 ↔ ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}

Tactic:
refine ⟨?_, fun ⟨e, heX, he, hXe⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
refine_1 : ∀ (I : Set α) (hI : M.IsBasis I X), M.eRk X = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
⊢ M.eRk X = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis X

Premises used: Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
refine_1 : (∃ (x : α), I = {x}) → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
⊢ M.eRk X = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}

Tactic:
rw [hI.eRk_eq_encard, encard_eq_one]

Premises used: Matroid.IsBasis.eRk_eq_encard, Set.encard_eq_one
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
e : α
hI : M.IsBasis {e} X
⊢ ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}

Tactic:
⟨e, singleton_subset_iff.1 hI.subset, indep_singleton.1 hI.indep, hI.subset_closure⟩

Premises used: Set.singleton_subset_iff, Matroid.IsBasis.subset, Matroid.indep_singleton, And.intro, Exists.intro, Iff.mp, Matroid.IsBasis.indep, Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
e : α
hI : M.IsBasis {e} X
⊢ ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}

Tactic:
exact ⟨e, singleton_subset_iff.1 hI.subset, indep_singleton.1 hI.indep, hI.subset_closure⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
h : ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
e : α
heX : e ∈ X
he : M.IsNonloop e
hXe : X ⊆ M.closure {e}
refine_2 : M.eRk X = M.eRk {e}
⊢ M.eRk X = 1

Tactic:
rw [← he.eRk_eq]

Premises used: Matroid.IsNonloop.eRk_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
h : ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
e : α
heX : e ∈ X
he : M.IsNonloop e
hXe : X ⊆ M.closure {e}
⊢ M.eRk X = M.eRk {e}

Tactic:
((M.eRk_mono hXe).trans (M.eRk_closure_eq _).le).antisymm
    (M.eRk_mono (singleton_subset_iff.2 heX))

Premises used: Iff.mpr, Set.singleton_subset_iff, Matroid.eRk_mono, LE.le.antisymm, Eq.le, LE.le.trans, Matroid.eRk_closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
h : ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
e : α
heX : e ∈ X
he : M.IsNonloop e
hXe : X ⊆ M.closure {e}
⊢ M.eRk X = M.eRk {e}

Tactic:
exact ((M.eRk_mono hXe).trans (M.eRk_closure_eq _).le).antisymm
    (M.eRk_mono (singleton_subset_iff.2 heX))

Premises used: Iff.mpr, Set.singleton_subset_iff, Matroid.eRk_mono, LE.le.antisymm, Eq.le, LE.le.trans, Matroid.eRk_closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
⊢ M.eRk X ≤ 1 ↔ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
⟨fun h ↦ ?_, fun ⟨e, _, he⟩ ↦ ?_⟩

Premises used: LE.le, Iff.intro, Matroid.eRk, OfNat.ofNat, _private.0.Matroid.eRk_le_one_iff.match_1
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
refine_1 : ∀ (h : M.eRk X ≤ 1), ∃ e ∈ M.E, X ⊆ M.closure {e}
refine_2 : (∃ e ∈ M.E, X ⊆ M.closure {e}) → ∀ e ∈ M.E, ∀ (he : X ⊆ M.closure {e}), M.eRk X ≤ 1
⊢ M.eRk X ≤ 1 ↔ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨e, _, he⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
h : M.eRk X ≤ 1
refine_1 : ∀ (I : Set α) (hI : M.IsBasis I X), ∃ e ∈ M.E, X ⊆ M.closure {e}
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis X

Premises used: Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
h : M.eRk X ≤ 1
I : Set α
hI : M.IsBasis I X
⊢ I = ∅ ∨ ∃ (x : α), I = {x}

Tactic:
rw [hI.eRk_eq_encard, encard_le_one_iff_eq] at h

Premises used: Matroid.IsBasis.eRk_eq_encard, Set.encard_le_one_iff_eq