awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₁ : I = ∅ ∨ ∃ (x : α), I = {x}
⊢ M.IsBasis 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
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
I : Set α
h : I = ∅ ∨ ∃ (x : α), I = {x}
hI : M.IsBasis I X
refine_1 : ∀ (hI : M.IsBasis ∅ X), ∃ e ∈ M.E, X ⊆ M.closure {e}
refine_1₁ : ∀ (e : α) (hI : M.IsBasis {e} X), ∃ e ∈ M.E, X ⊆ M.closure {e}
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
obtain (rfl | ⟨e, rfl⟩) := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
hI : M.IsBasis ∅ X
refine_1 : ∀ (e : α) (he : e ∈ M.E), ∃ e ∈ M.E, X ⊆ M.closure {e}
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
obtain ⟨e, he⟩ := M.ground_nonempty

Premises used: Matroid.ground_nonempty
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
hI : M.IsBasis ∅ X
e : α
he : e ∈ M.E
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
⟨e, he, hI.subset_closure.trans ((M.closure_subset_closure (empty_subset _)))⟩

Premises used: HasSubset.Subset.trans, Matroid.closure_subset_closure, And.intro, Set.empty_subset, Exists.intro, Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
hI : M.IsBasis ∅ X
e : α
he : e ∈ M.E
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
exact ⟨e, he, hI.subset_closure.trans ((M.closure_subset_closure (empty_subset _)))⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
e : α
hI : M.IsBasis {e} X
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
⟨e, hI.indep.subset_ground rfl,  hI.subset_closure⟩

Premises used: Matroid.Indep.subset_ground, And.intro, Exists.intro, Matroid.IsBasis.indep, Matroid.IsBasis.subset_closure, rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
e : α
hI : M.IsBasis {e} X
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
exact ⟨e, hI.indep.subset_ground rfl,  hI.subset_closure⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
h : ∃ e ∈ M.E, X ⊆ M.closure {e}
e : α
left : e ∈ M.E
he : X ⊆ M.closure {e}
⊢ M.eRk X ≤ 1

Tactic:
(M.eRk_mono he).trans ?_

Premises used: Matroid.eRk_mono, LE.le.trans
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
h : ∃ e ∈ M.E, X ⊆ M.closure {e}
e : α
left : e ∈ M.E
he : X ⊆ M.closure {e}
refine_2 : M.eRk (M.closure {e}) ≤ 1
⊢ M.eRk X ≤ 1

Tactic:
refine (M.eRk_mono he).trans ?_

Premises used: Matroid.eRk_mono, LE.le.trans
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
h : ∃ e ∈ M.E, X ⊆ M.closure {e}
e : α
left : e ∈ M.E
he : X ⊆ M.closure {e}
refine_2 : M.eRk {e} ≤ encard (α := α) {e}
⊢ M.eRk (M.closure {e}) ≤ 1

Tactic:
rw [eRk_closure_eq, ← encard_singleton e]

Premises used: Set.encard_singleton, 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
h : ∃ e ∈ M.E, X ⊆ M.closure {e}
e : α
left : e ∈ M.E
he : X ⊆ M.closure {e}
⊢ M.eRk {e} ≤ encard (α := α) {e}

Tactic:
M.eRk_le_encard {e}

Premises used: Matroid.eRk_le_encard, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
h : ∃ e ∈ M.E, X ⊆ M.closure {e}
e : α
left : e ∈ M.E
he : X ⊆ M.closure {e}
⊢ M.eRk {e} ≤ encard (α := α) {e}

Tactic:
exact M.eRk_le_encard {e}

Premises used: Matroid.eRk_le_encard, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
obtain : ∀ (B : Set α) (hB : M.IsBasis B X), M.eRk X = M.eRank
⊢ M.eRk X = M.eRank

Tactic:
obtain ⟨B, hB⟩ := M.exists_isBasis X

Premises used: Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
B : Set α
hB : M.IsBasis B X
rw : M.eRank ≤ B.encard
rw₁ rw₂ : B.encard ≤ B.encard
⊢ M.eRank ≤ M.eRk X

Tactic:
rw [← hB.encard_eq_eRk, ← (hB.isBase_of_spanning hX).encard_eq_eRank]

Premises used: Matroid.IsBase.encard_eq_eRank, Matroid.IsBasis.isBase_of_spanning, Matroid.IsBasis.encard_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
B : Set α
hB : M.IsBasis B X
⊢ M.eRk X = M.eRank

Tactic:
exact (M.eRk_le_eRank X).antisymm <| by
    rw [← hB.encard_eq_eRk, ← (hB.isBase_of_spanning hX).encard_eq_eRank]

Premises used: LE.le.antisymm, Matroid.eRk_le_eRank
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
⊢ M.Spanning X ↔ M.eRank ≤ M.eRk X ∧ X ⊆ M.E

Tactic:
⟨fun h ↦ ⟨h.eRk_eq.symm.le, h.subset_ground⟩, fun ⟨h, hX⟩ ↦ ?_⟩

Premises used: Eq.le, Matroid.Spanning.eRk_eq, Matroid.Spanning.subset_ground, Matroid.Spanning, And.intro, _private.0.Matroid.spanning_iff_eRk_le'.match_1, Iff.intro, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
refine : M.eRank ≤ M.eRk X ∧ X ⊆ M.E → ∀ (h : M.eRank ≤ M.eRk X) (hX : X ⊆ M.E), M.Spanning X
⊢ M.Spanning X ↔ M.eRank ≤ M.eRk X ∧ X ⊆ M.E

Tactic:
refine ⟨fun h ↦ ⟨h.eRk_eq.symm.le, h.subset_ground⟩, fun ⟨h, hX⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
h_1 : M.eRank ≤ M.eRk X ∧ X ⊆ M.E
h : M.eRank ≤ M.eRk X
hX : X ⊆ M.E
obtain : ∀ (I : Set α) (hI : M.IsBasis I X), M.Spanning X
⊢ M.Spanning X

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.RankFinite
h_1 : M.eRank ≤ M.eRk X ∧ X ⊆ M.E
h : M.eRank ≤ M.eRk X
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ M.Spanning X

Tactic:
(hI.indep.isBase_of_eRk_ge
    hI.indep.finite (h.trans hI.eRk_eq_eRk.symm.le)).spanning_of_superset hI.subset

Premises used: Matroid.IsBase.spanning_of_superset, Matroid.Indep.isBase_of_eRk_ge, Matroid.Indep.finite, Eq.le, Matroid.IsBasis.subset, Matroid.IsBasis.eRk_eq_eRk, Matroid.IsBasis.indep, LE.le.trans, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
h_1 : M.eRank ≤ M.eRk X ∧ X ⊆ M.E
h : M.eRank ≤ M.eRk X
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ M.Spanning X

Tactic:
exact (hI.indep.isBase_of_eRk_ge
    hI.indep.finite (h.trans hI.eRk_eq_eRk.symm.le)).spanning_of_superset hI.subset

Premises used: Matroid.IsBase.spanning_of_superset, Matroid.Indep.isBase_of_eRk_ge, Matroid.Indep.finite, Eq.le, Matroid.IsBasis.subset, Matroid.IsBasis.eRk_eq_eRk, Matroid.IsBasis.indep, LE.le.trans, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
hX : X ⊆ M.E
rw : M.eRank ≤ M.eRk X ∧ X ⊆ M.E ↔ M.eRank ≤ M.eRk X
rw₁ rw₂ : M.eRank ≤ M.eRk X ↔ M.eRank ≤ M.eRk X
⊢ M.Spanning X ↔ M.eRank ≤ M.eRk X

Tactic:
rw [spanning_iff_eRk_le', and_iff_left hX]

Premises used: and_iff_left, Matroid.spanning_iff_eRk_le'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
rw : (M ↾ X).eRk (M ↾ X).E = M.eRank
rw₁ : (M ↾ X).eRk X = M.eRank
rw₂ : M.eRk X = M.eRank
rw₃ rw₄ : M.eRank = M.eRank
⊢ (M ↾ X).eRank = M.eRank

Tactic:
rw [eRank_def, restrict_ground_eq, restrict_eRk_eq _ rfl.subset, hX.eRk_eq]

Premises used: Matroid.restrict_ground_eq, Matroid.eRank_def, Matroid.Spanning.eRk_eq, Eq.subset, Matroid.restrict_eRk_eq, rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
obtain : ∀ (B : Set α) (hB : M.IsBase B), (M.map f hf).eRank = M.eRank
⊢ (M.map f hf).eRank = M.eRank

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

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
rw : (f '' B).encard = M.eRank
rw₁ : (f '' B).encard = B.encard
rw₂ rw₃ : B.encard = B.encard
⊢ (M.map f hf).eRank = M.eRank

Tactic:
rw [← (hB.map hf).encard_eq_eRank, ← hB.encard_eq_eRank, (hf.mono hB.subset_ground).encard_image]

Premises used: Matroid.IsBase.encard_eq_eRank, Matroid.IsBase.map, Matroid.IsBase.subset_ground, Set.InjOn.encard_image, Set.InjOn.mono
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X : Set α
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
hX : X ⊆ M.E
obtain : ∀ (I : Set α) (hI : M.IsBasis I X), (M.map f hf).eRk (f '' X) = M.eRk X
⊢ (M.map f hf).eRk (f '' X) = M.eRk X

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

Premises used: Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X : Set α
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
rw : (M.map f hf).eRk (f '' X) = I.encard
rw₁ : (f '' I).encard = I.encard
rw₂ rw₃ : I.encard = I.encard
⊢ (M.map f hf).eRk (f '' X) = M.eRk X

Tactic:
rw [hI.eRk_eq_encard, (hI.map hf).eRk_eq_encard, (hf.mono hI.indep.subset_ground).encard_image]

Premises used: Matroid.IsBasis.eRk_eq_encard, Matroid.Indep.subset_ground, Matroid.IsBasis.map, Set.InjOn.encard_image, Set.InjOn.mono, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X : Set α
obtain : ∀ (I : Set α) (hI : (M.comap f).IsBasis' I X), (M.comap f).eRk X = M.eRk (f '' X)
⊢ (M.comap f).eRk X = M.eRk (f '' X)

Tactic:
obtain ⟨I, hI⟩ := (M.comap f).exists_isBasis' X

Premises used: Matroid.comap, Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X I : Set α
hI : (M.comap f).IsBasis' I X
⊢ M.IsBasis' (f '' I) (f '' X)

Tactic:
obtain ⟨hI', hinj, -⟩ := comap_isBasis'_iff.1 hI

Premises used: Matroid.comap_isBasis'_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
⊢ InjOn f I

Tactic:
obtain ⟨hI', hinj, -⟩ := comap_isBasis'_iff.1 hI

Premises used: Matroid.comap_isBasis'_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hinj : InjOn f I
rw : I.encard = M.eRk (f '' X)
rw₁ : I.encard = (f '' I).encard
rw₂ rw₃ : I.encard = I.encard
⊢ (M.comap f).eRk X = M.eRk (f '' X)

Tactic:
rw [← hI.encard_eq_eRk, ← hI'.encard_eq_eRk, hinj.encard_image]

Premises used: Matroid.IsBasis'.encard_eq_eRk, Set.InjOn.encard_image
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X Y : Set α
obtain : ∀ (I : Set α) (hI : (loopyOn Y).IsBasis' I X), (loopyOn Y).eRk X = 0
⊢ (loopyOn Y).eRk X = 0

Tactic:
obtain ⟨I, hI⟩ := (loopyOn Y).exists_isBasis' X

Premises used: Matroid.loopyOn, Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X Y I : Set α
hI : (loopyOn Y).IsBasis' I X
rw : I.encard = 0
rw₁ : encard.{u_1} (α := α) ∅ = 0
rw₂ rw₃ : Eq (α := ℕ∞) 0 0
⊢ (loopyOn Y).eRk X = 0

Tactic:
rw [hI.eRk_eq_encard, loopyOn_indep_iff.1 hI.indep, encard_empty]

Premises used: Matroid.loopyOn_indep_iff, Set.encard_empty, Matroid.IsBasis'.eRk_eq_encard, Matroid.IsBasis'.indep, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X : Set α
rw : (loopyOn X).eRk (loopyOn X).E = 0
rw₁ rw₂ : Eq (α := ℕ∞) 0 0
⊢ (loopyOn X).eRank = 0

Tactic:
rw [eRank_def, eRk_loopyOn]

Premises used: Matroid.eRank_def, Matroid.eRk_loopyOn
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
h : M = loopyOn M.E
rw : (loopyOn M.E).eRank = 0
rw₁ rw₂ : Eq (α := ℕ∞) 0 0
⊢ M.eRank = 0

Tactic:
rw [h, eRank_loopyOn]

Premises used: Matroid.eRank_loopyOn
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
refine : ∀ (h : M.eRank = 0), M.closure ∅ = M.E
⊢ M.eRank = 0 ↔ M = loopyOn M.E

Tactic:
refine ⟨fun h ↦ closure_empty_eq_ground_iff.1 ?_, fun h ↦ by rw [h, eRank_loopyOn]⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
h : M.eRank = 0
obtain : ∀ (B : Set α) (hB : M.IsBase B), M.closure ∅ = M.E
⊢ M.closure ∅ = M.E

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

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
h : M.eRank = 0
B : Set α
hB : M.IsBase B
⊢ B = ∅

Tactic:
rw [← hB.encard_eq_eRank, encard_eq_zero] at h

Premises used: Matroid.IsBase.encard_eq_eRank, Set.encard_eq_zero
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
h : M.eRank = 0
B : Set α
hB : M.IsBase B
h₁ : B = ∅
⊢ M.IsBase B

Tactic:
rw [← hB.encard_eq_eRank, encard_eq_zero] at h

Premises used: Matroid.IsBase.encard_eq_eRank, Set.encard_eq_zero
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : B = ∅
hB : M.IsBase B
rw : M.closure B = M.E
rw₁ rw₂ : M.E = M.E
⊢ M.closure ∅ = M.E

Tactic:
rw [← h, hB.closure_eq]

Premises used: Matroid.IsBase.closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
h : M.eRank = 0
⊢ M = loopyOn M.E

Tactic:
simpa [eRank_eq_zero_iff] using h

Premises used: Matroid.eRank_eq_zero_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_2
rw : emptyOn α = loopyOn (emptyOn α).E
rw₁ : emptyOn α = loopyOn ∅
rw₂ rw₃ : emptyOn α = emptyOn α
⊢ (emptyOn α).eRank = 0

Tactic:
rw [eRank_eq_zero_iff, emptyOn_ground, loopyOn_empty]

Premises used: Matroid.emptyOn_ground, Matroid.loopyOn_empty, Matroid.eRank_eq_zero_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : M = loopyOn X
rw : (loopyOn X).eRank = 0 ∧ (loopyOn X).E = X
⊢ M.eRank = 0 ∧ M.E = X

Tactic:
rw [h]
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : M = loopyOn X
⊢ (loopyOn X).eRank = 0 ∧ (loopyOn X).E = X

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
h_1 : M.eRank = 0 ∧ M.E = X
h : M.eRank = 0
h' : M.E = X
rw : M = loopyOn M.E
rw₁ : M.eRank = 0
rw₂ rw₃ : Eq (α := ℕ∞) 0 0
⊢ M = loopyOn X

Tactic:
rw [← h', ← eRank_eq_zero_iff, h]

Premises used: Matroid.eRank_eq_zero_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X : Set α
rw : (freeOn X).eRk (freeOn X).E = X.encard
rw₁ : (freeOn X).eRk X = X.encard
rw₂ rw₃ : X.encard = X.encard
⊢ (freeOn X).eRank = X.encard

Tactic:
rw [eRank_def, freeOn_ground, (freeOn_indep_iff.2 rfl.subset).eRk_eq_encard]

Premises used: Iff.mpr, Matroid.Indep.eRk_eq_encard, Matroid.eRank_def, Matroid.freeOn_ground, Eq.subset, Matroid.freeOn_indep_iff, rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X Y : Set α
hXY : X ⊆ Y
obtain : ∀ (I : Set α) (hI : (freeOn Y).IsBasis I X), (freeOn Y).eRk X = X.encard
⊢ (freeOn Y).eRk X = X.encard

Tactic:
obtain ⟨I, hI⟩ := (freeOn Y).exists_isBasis X

Premises used: Matroid.exists_isBasis, Matroid.freeOn
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : (freeOn Y).IsBasis I X
rw : I.encard = X.encard
rw₁ rw₂ : X.encard = X.encard
⊢ (freeOn Y).eRk X = X.encard

Tactic:
rw [hI.eRk_eq_encard, (freeOn_indep hXY).eq_of_isBasis hI]

Premises used: Matroid.IsBasis.eRk_eq_encard, Matroid.freeOn_indep, Matroid.Indep.eq_of_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ (M.E \ B).encard = M✶.eRank

Tactic:
(hB.compl_isBase_dual).encard_eq_eRank

Premises used: Matroid.IsBase.encard_eq_eRank, Matroid.IsBase.compl_isBase_dual
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
obtain : ∀ (I : Set α) (hI : M✶.IsBasis I X), M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard

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

Premises used: Matroid.dual, 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
obtain :
  ∀ (B : Set α) (hB : M✶.IsBasis B M.E) (hI : M✶.IsBasis (B ∩ X) X), M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard

Tactic:
obtain ⟨B, hB, rfl⟩ := hI.exists_isBasis_inter_eq_of_superset hX

Premises used: Matroid.IsBasis.exists_isBasis_inter_eq_of_superset, rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
⊢ M✶.IsBase B

Tactic:
have hB' : M✶.IsBase B := isBasis_ground_iff.1 hB
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
⊢ M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
simpa using hB'.inter_isBasis_iff_compl_inter_isBasis_dual.1 hI

Premises used: Iff.mp, Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
⊢ M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
have hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X) := by
    simpa using hB'.inter_isBasis_iff_compl_inter_isBasis_dual.1 hI
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
tauto_set tauto_set₁ tauto_set₂ tauto_set₃ :
  ∀ (hX : ∀ x ∈ X, x ∈ M.E) (hB : M✶.IsBasis B M.E) (hI : M✶.IsBasis (B ∩ X) X) (hB' : M✶.IsBase B)
    (hd : M.IsBasis (M.E ∩ Bᶜ ∩ (M.E ∩ Xᶜ)) (M.E ∩ Xᶜ)) (x : α),
    (x ∈ B ∧ x ∈ X) ∧ x ∈ M.E ∧ x ∉ B → Membership.mem (γ := Set α) ∅ x
⊢ Disjoint (B ∩ X) (M.E \ B)

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
tauto_set tauto_set₁ tauto_set₂ tauto_set₃ :
  ∀ (hX : ∀ x ∈ X, x ∈ M.E) (hB : M✶.IsBasis B M.E) (hI : M✶.IsBasis (B ∩ X) X) (hB' : M✶.IsBase B)
    (hd : M.IsBasis (M.E ∩ Bᶜ ∩ (M.E ∩ Xᶜ)) (M.E ∩ Xᶜ)) (x : α),
    ((x ∈ M.E ∧ x ∉ B) ∧ x ∈ M.E ∧ x ∉ X) ∧ x ∈ X → Membership.mem (γ := Set α) ∅ x
⊢ Disjoint (M.E \ B ∩ (M.E \ X)) X

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
rw : (B ∩ X ∪ M.E \ B).encard = (M.E \ B ∩ (M.E \ X) ∪ X).encard
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard

Tactic:
rw [← hB'.compl_isBase_of_dual.encard_eq_eRank, hI.eRk_eq_encard, hd.eRk_eq_encard,
    ← encard_union_eq (by tauto_set), ← encard_union_eq (by tauto_set)]

Premises used: Matroid.IsBase.encard_eq_eRank, Set.encard_union_eq, Matroid.IsBase.compl_isBase_of_dual, Matroid.IsBasis.eRk_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
tauto_set tauto_set₁ tauto_set₂ tauto_set₃ :
  ∀ (hX : ∀ x ∈ X, x ∈ M.E) (hB : M✶.IsBasis B M.E) (hI : M✶.IsBasis (B ∩ X) X) (hB' : M✶.IsBase B)
    (hd : M.IsBasis (M.E ∩ Bᶜ ∩ (M.E ∩ Xᶜ)) (M.E ∩ Xᶜ)) (x : α),
    x ∈ B ∧ x ∈ X ∨ x ∈ M.E ∧ x ∉ B ↔ (x ∈ M.E ∧ x ∉ B) ∧ x ∈ M.E ∧ x ∉ X ∨ x ∈ X
⊢ B ∩ X ∪ M.E \ B = M.E \ B ∩ (M.E \ X) ∪ X

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ (B ∩ X ∪ M.E \ B).encard = (M.E \ B ∩ (M.E \ X) ∪ X).encard

Tactic:
exact congr_arg _ (by tauto_set)

Premises used: congr_arg
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M✶.eRk X + M.eRank = M.eRk (M.E \ (X ∩ M.E)) + (X ∩ M.E).encard
rw₁ : M✶.eRk X + M.eRank = M✶.eRk (X ∩ M.E) + M.eRank
rw₂ : M✶.eRk X + M.eRank = M✶.eRk (X ∩ M✶.E) + M.eRank
rw₃ rw₄ : M✶.eRk X + M.eRank = M✶.eRk X + M.eRank
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + (X ∩ M.E).encard

Tactic:
rw [← diff_inter_self_eq_diff, ← eRk_dual_add_eRank .., ← dual_ground, eRk_inter_ground]

Premises used: Matroid.eRk_dual_add_eRank, Matroid.eRk_inter_ground, Set.diff_inter_self_eq_diff, Matroid.dual_ground
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
obtain : ∀ (B : Set α) (hB : M.IsBase B), M.eRank + M✶.eRank = M.E.encard
⊢ M.eRank + M✶.eRank = M.E.encard

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

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
rw : B.encard + M✶.eRank = M.E.encard
rw₁ : B.encard + (M.E \ B).encard = M.E.encard
rw₂ : (B ∪ M.E \ B).encard = M.E.encard
rw₃ rw₄ : M.E.encard = M.E.encard
⊢ M.eRank + M✶.eRank = M.E.encard

Tactic:
rw [← hB.encard_eq_eRank, ← hB.compl_isBase_dual.encard_eq_eRank,
    ← encard_union_eq disjoint_sdiff_right, union_diff_cancel hB.subset_ground]

Premises used: Matroid.IsBase.encard_eq_eRank, Set.encard_union_eq, Matroid.IsBase.subset_ground, Matroid.IsBase.compl_isBase_dual, Set.union_diff_cancel, Set.disjoint_sdiff_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.IsRkFinite X
⊢ (M ↾ X).RankFinite

Tactic:
hX

Premises used: Matroid.IsRkFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
inst : M.RankFinite
X : Set α
⊢ M.IsRkFinite X

Tactic:
inferInstanceAs (M ↾ X).RankFinite

Premises used: Matroid.restrict_rankFinite, Matroid.IsRkFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ I.Finite ↔ M.IsRkFinite X

Tactic:
⟨fun h ↦ ⟨I, hI, h⟩, fun (_ : (M ↾ X).RankFinite) ↦ hI.isBase_restrict.finite⟩

Premises used: Matroid.IsBasis'.isBase_restrict, Matroid.RankFinite.mk, And.intro, Iff.intro, Exists.intro, Matroid.IsBase.finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I X
⊢ I.Finite ↔ M.IsRkFinite X

Tactic:
hI.isBasis'.finite_iff_isRkFinite

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.finite_iff_isRkFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
⊢ M.IsRkFinite X

Tactic:
⟨I, hI, hIfin⟩

Premises used: Matroid.RankFinite.mk, And.intro, Exists.intro, Matroid.IsRkFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Finite
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I X
hIfin : I.Finite
⊢ M.IsRkFinite X

Tactic:
⟨I, hI.isBasis', hIfin⟩

Premises used: Matroid.IsBasis.isBasis', Matroid.RankFinite.mk, And.intro, Exists.intro, Matroid.IsRkFinite