awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
hX : X ⊆ M.E
h : M.eRk X = n
I : Set α
hI : M.IsBasis I X
rw : M.eRk X = n
rw₁ rw₂ : M.eRk X = M.eRk X
⊢ I.encard = n

Tactic:
rw [hI.encard_eq_eRk, ← h]

Premises used: Matroid.IsBasis.encard_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
hX : X ⊆ M.E
h : ∃ (I : Set α), M.IsBasis I X ∧ I.encard = n
I : Set α
hI : M.IsBasis I X
hIc rw : I.encard = n
rw₁ rw₂ : n = n
⊢ M.eRk X = n

Tactic:
rw [← hI.encard_eq_eRk, hIc]

Premises used: Matroid.IsBasis.encard_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.eRk I = I.encard

Tactic:
(eq_eRk_iff hI.subset_ground).mpr ⟨I, hI.isBasis_self, rfl⟩

Premises used: Iff.mpr, Matroid.Indep.subset_ground, And.intro, Exists.intro, Matroid.eq_eRk_iff, rfl, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
rw : M.eRk I = I.encard
rw₁ rw₂ : I.encard = I.encard
⊢ M.eRk I = M.eRk X

Tactic:
rw [← hIX.encard_eq_eRk, hIX.indep.eRk_eq_encard]

Premises used: Matroid.Indep.eRk_eq_encard, Matroid.IsBasis'.encard_eq_eRk, Matroid.IsBasis'.indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
rw : M.eRk I = I.encard
rw₁ rw₂ : I.encard = I.encard
⊢ M.eRk I = M.eRk X

Tactic:
rw [← hIX.encard_eq_eRk, hIX.indep.eRk_eq_encard]

Premises used: Matroid.Indep.eRk_eq_encard, Matroid.IsBasis.encard_eq_eRk, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
rw : M.eRk I = I.encard
rw₁ rw₂ : I.encard = I.encard
⊢ M.eRk X = I.encard

Tactic:
rw [← hIX.eRk_eq_eRk, hIX.indep.eRk_eq_encard]

Premises used: Matroid.Indep.eRk_eq_encard, Matroid.IsBasis'.indep, Matroid.IsBasis'.eRk_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
rw : M.eRk I = I.encard
rw₁ rw₂ : I.encard = I.encard
⊢ M.eRk X = I.encard

Tactic:
rw [← hIX.eRk_eq_eRk, hIX.indep.eRk_eq_encard]

Premises used: Matroid.Indep.eRk_eq_encard, Matroid.IsBasis.eRk_eq_eRk, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
rw : B.encard = M.eRank
rw₁ : B.encard = M.eRk M.E
rw₂ rw₃ : M.eRk M.E = M.eRk M.E
⊢ M.eRk B = M.eRank

Tactic:
rw [hB.indep.eRk_eq_encard, eRank_def, hB.isBasis_ground.encard_eq_eRk]

Premises used: Matroid.Indep.eRk_eq_encard, Matroid.IsBase.isBasis_ground, Matroid.IsBasis.encard_eq_eRk, Matroid.eRank_def, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk (X ∩ M.E) = M.eRk X
⊢ M.eRk (X ∩ M.E) = 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
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
rw : M.eRk (X ∩ M.E) = M.eRk I
rw₁ rw₂ : M.eRk (X ∩ M.E) = M.eRk (X ∩ M.E)
⊢ M.eRk (X ∩ M.E) = M.eRk X

Tactic:
rw [← hI.eRk_eq_eRk, hI.isBasis_inter_ground.eRk_eq_eRk]

Premises used: Matroid.IsBasis'.isBasis_inter_ground, Matroid.IsBasis.eRk_eq_eRk, Matroid.IsBasis'.eRk_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRk (X ∩ M.E) = M.eRk X
rw₁ rw₂ : M.eRk X = M.eRk X
⊢ M.eRk (M.E ∩ X) = M.eRk X

Tactic:
rw [inter_comm, eRk_inter_ground]

Premises used: Matroid.eRk_inter_ground, Set.inter_comm
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRk ((X ∪ M.E) ∩ M.E) = M.eRank
rw₁ : M.eRk M.E = M.eRank
rw₂ rw₃ : M.eRk M.E = M.eRk M.E
⊢ M.eRk (X ∪ M.E) = M.eRank

Tactic:
rw [← eRk_inter_ground, inter_eq_self_of_subset_right subset_union_right, eRank_def]

Premises used: Set.subset_union_right, Matroid.eRank_def, Matroid.eRk_inter_ground, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRk (X ∪ M.E) = M.eRank
rw₁ rw₂ : M.eRank = M.eRank
⊢ M.eRk (M.E ∪ X) = M.eRank

Tactic:
rw [union_comm, eRk_union_ground]

Premises used: Matroid.eRk_union_ground, Set.union_comm
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
rw : M.eRk (insert e X ∩ M.E) = M.eRk X
rw₁ : M.eRk (X ∩ M.E) = M.eRk X
rw₂ rw₃ : M.eRk X = M.eRk X
⊢ M.eRk (insert e X) = M.eRk X

Tactic:
rw [← eRk_inter_ground, insert_inter_of_notMem he, eRk_inter_ground]

Premises used: Matroid.eRk_inter_ground, Set.insert_inter_of_notMem
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.E ⊆ X
rw : M.eRk (X ∩ M.E) = M.eRank
rw₁ : M.eRk M.E = M.eRank
rw₂ rw₃ : M.eRk M.E = M.eRk M.E
⊢ M.eRk X = M.eRank

Tactic:
rw [← eRk_inter_ground, inter_eq_self_of_subset_right hX, eRank_def]

Premises used: Matroid.eRank_def, Matroid.eRk_inter_ground, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : Disjoint X Y
rw : M.eRk ((M.E \ X ∪ Y) ∩ M.E) = M.eRk (M.E \ X)
rw₁ : M.eRk (M.E \ X ∩ M.E ∪ Y ∩ M.E) = M.eRk (M.E \ X)
rw₂ : M.eRk (M.E \ X ∪ Y ∩ M.E) = M.eRk (M.E \ X)
rw₃ rw₄ : M.eRk (M.E \ X) = M.eRk (M.E \ X)
⊢ M.eRk (M.E \ X ∪ Y) = M.eRk (M.E \ X)

Tactic:
rw [← eRk_inter_ground, union_inter_distrib_right, inter_eq_self_of_subset_left diff_subset,
    union_eq_self_of_subset_right
      (subset_diff.2 ⟨inter_subset_right, hXY.symm.mono_left inter_subset_left⟩)]

Premises used: Iff.mpr, Set.diff_subset, Set.union_eq_self_of_subset_right, Set.subset_diff, Set.inter_subset_left, Matroid.eRk_inter_ground, Disjoint.mono_left, Disjoint.symm, And.intro, Set.union_inter_distrib_right, Set.inter_subset_right, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
inst : M.RankPos
obtain : ∀ (B : Set α) (hB : M.IsBase B), 1 ≤ M.eRank
⊢ 1 ≤ M.eRank

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

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
inst : M.RankPos
B : Set α
hB : M.IsBase B
rw : B.Nonempty
⊢ 1 ≤ M.eRank

Tactic:
rw [← hB.encard_eq_eRank, one_le_encard_iff_nonempty]

Premises used: Matroid.IsBase.encard_eq_eRank, Set.one_le_encard_iff_nonempty
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
inst : M.RankPos
B : Set α
hB : M.IsBase B
⊢ B.Nonempty

Tactic:
hB.nonempty

Premises used: Matroid.IsBase.nonempty
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
inst : M.RankPos
B : Set α
hB : M.IsBase B
⊢ B.Nonempty

Tactic:
exact hB.nonempty

Premises used: Matroid.IsBase.nonempty
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
rw : M.eRk (univ ∩ M.E) = M.eRank
rw₁ : M.eRk M.E = M.eRank
rw₂ rw₃ : M.eRk M.E = M.eRk M.E
⊢ M.eRk univ = M.eRank

Tactic:
rw [← eRk_inter_ground, univ_inter, eRank_def]

Premises used: Matroid.eRank_def, Matroid.eRk_inter_ground, Set.univ_inter
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
rw : encard.{u_1} (α := α) ∅ = 0
rw₁ rw₂ : Eq (α := ℕ∞) 0 0
⊢ M.eRk ∅ = 0

Tactic:
rw [← M.empty_indep.isBasis_self.encard_eq_eRk, encard_empty]

Premises used: Set.encard_empty, Matroid.IsBasis.encard_eq_eRk, Matroid.empty_indep, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk (M.closure X) = M.eRk X
⊢ M.eRk (M.closure 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
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
rw : M.eRk (M.closure I) = M.eRk X
rw₁ : I.encard = M.eRk X
rw₂ rw₃ : M.eRk X = M.eRk X
⊢ M.eRk (M.closure X) = M.eRk X

Tactic:
rw [← hI.closure_eq_closure, ← hI.indep.isBasis_closure.encard_eq_eRk, hI.encard_eq_eRk]

Premises used: Matroid.IsBasis'.closure_eq_closure, Matroid.Indep.isBasis_closure, Matroid.IsBasis'.encard_eq_eRk, Matroid.IsBasis.encard_eq_eRk, Matroid.IsBasis'.indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
rw : M.eRk (M.closure (X ∪ M.closure Y)) = M.eRk (X ∪ Y)
rw₁ : M.eRk (M.closure (X ∪ Y)) = M.eRk (X ∪ Y)
rw₂ rw₃ : M.eRk (X ∪ Y) = M.eRk (X ∪ Y)
⊢ M.eRk (X ∪ M.closure Y) = M.eRk (X ∪ Y)

Tactic:
rw [← eRk_closure_eq, closure_union_closure_right_eq, eRk_closure_eq]

Premises used: Matroid.closure_union_closure_right_eq, Matroid.eRk_closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
rw : M.eRk (M.closure (M.closure X ∪ Y)) = M.eRk (X ∪ Y)
rw₁ : M.eRk (M.closure (X ∪ Y)) = M.eRk (X ∪ Y)
rw₂ rw₃ : M.eRk (X ∪ Y) = M.eRk (X ∪ Y)
⊢ M.eRk (M.closure X ∪ Y) = M.eRk (X ∪ Y)

Tactic:
rw [← eRk_closure_eq, closure_union_closure_left_eq, eRk_closure_eq]

Premises used: Matroid.closure_union_closure_left_eq, Matroid.eRk_closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
rw : M.eRk (M.closure X ∪ {e}) = M.eRk (insert e X)
rw₁ : M.eRk (X ∪ {e}) = M.eRk (insert e X)
rw₂ rw₃ : M.eRk (insert e X) = M.eRk (insert e X)
⊢ M.eRk (insert e (M.closure X)) = M.eRk (insert e X)

Tactic:
rw [← union_singleton, eRk_union_closure_left_eq, union_singleton]

Premises used: Matroid.eRk_union_closure_left_eq, Set.union_singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
R X : Set α
obtain : ∀ (I : Set α) (hI : (M ↾ R).IsBasis' I X), (M ↾ R).eRk X = M.eRk (X ∩ R)
⊢ (M ↾ R).eRk X = M.eRk (X ∩ R)

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

Premises used: Matroid.restrict, Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
R X I : Set α
hI : (M ↾ R).IsBasis' I X
rw : I.encard = M.eRk (X ∩ R)
⊢ (M ↾ R).eRk X = M.eRk (X ∩ R)

Tactic:
rw [hI.eRk_eq_encard]

Premises used: Matroid.IsBasis'.eRk_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
R X I : Set α
hI : (M ↾ R).IsBasis' I X
⊢ M.IsBasis I (X ∩ R ∩ M.E) ∧ X ∩ R ⊆ R

Tactic:
rw [isBasis'_iff_isBasis_inter_ground, isBasis_restrict_iff', restrict_ground_eq] at hI

Premises used: Matroid.restrict_ground_eq, Matroid.isBasis'_iff_isBasis_inter_ground, Matroid.isBasis_restrict_iff'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
R X I : Set α
hI : M.IsBasis I (X ∩ R ∩ M.E) ∧ X ∩ R ⊆ R
rw : I.encard = M.eRk (X ∩ R ∩ M.E)
rw₁ rw₂ : M.eRk (X ∩ R ∩ M.E) = M.eRk (X ∩ R ∩ M.E)
⊢ I.encard = M.eRk (X ∩ R)

Tactic:
rw [← eRk_inter_ground, ← hI.1.eRk_eq_encard]

Premises used: Matroid.IsBasis.eRk_eq_encard, Matroid.eRk_inter_ground, And.left
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X : Set α
M : Matroid α
R : Set α
h : X ⊆ R
rw : M.eRk (X ∩ R) = M.eRk X
rw₁ rw₂ : M.eRk X = M.eRk X
⊢ (M ↾ R).eRk X = M.eRk X

Tactic:
rw [restrict_eRk_eq', inter_eq_self_of_subset_left h]

Premises used: Matroid.restrict_eRk_eq', Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
Y : Set α
rw : M.eRk (M.closure I ∪ Y) = M.eRk (X ∪ Y)
rw₁ : M.eRk (M.closure X ∪ Y) = M.eRk (X ∪ Y)
rw₂ rw₃ : M.eRk (X ∪ Y) = M.eRk (X ∪ Y)
⊢ M.eRk (I ∪ Y) = M.eRk (X ∪ Y)

Tactic:
rw [← eRk_union_closure_left_eq, hIX.closure_eq_closure, eRk_union_closure_left_eq]

Premises used: Matroid.IsBasis'.closure_eq_closure, Matroid.eRk_union_closure_left_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
e : α
rw : M.eRk (I ∪ {e}) = M.eRk (insert e X)
rw₁ : M.eRk (X ∪ {e}) = M.eRk (insert e X)
rw₂ rw₃ : M.eRk (insert e X) = M.eRk (insert e X)
⊢ M.eRk (insert e I) = M.eRk (insert e X)

Tactic:
rw [← union_singleton, hIX.eRk_eq_eRk_union, union_singleton]

Premises used: Matroid.IsBasis'.eRk_eq_eRk_union, Set.union_singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
Y : Set α
⊢ M.eRk (I ∪ Y) = M.eRk (X ∪ Y)

Tactic:
hIX.isBasis'.eRk_eq_eRk_union Y

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.eRk_eq_eRk_union
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
e : α
rw : M.eRk (I ∪ {e}) = M.eRk (insert e X)
rw₁ : M.eRk (X ∪ {e}) = M.eRk (insert e X)
rw₂ rw₃ : M.eRk (insert e X) = M.eRk (insert e X)
⊢ M.eRk (insert e I) = M.eRk (insert e X)

Tactic:
rw [← union_singleton, hIX.eRk_eq_eRk_union, union_singleton]

Premises used: Matroid.IsBasis.eRk_eq_eRk_union, Set.union_singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk X ≤ X.encard
⊢ M.eRk X ≤ X.encard

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 I : Set α
hI : M.IsBasis' I X
rw : I.encard ≤ X.encard
⊢ M.eRk X ≤ X.encard

Tactic:
rw [hI.eRk_eq_encard]

Premises used: Matroid.IsBasis'.eRk_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ I.encard ≤ X.encard

Tactic:
encard_mono hI.subset

Premises used: Set.encard_mono, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ I.encard ≤ X.encard

Tactic:
exact encard_mono hI.subset

Premises used: Set.encard_mono, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
⊢ M.eRank ≤ M.E.encard

Tactic:
M.eRank_def.trans_le <| M.eRk_le_encard M.E

Premises used: Matroid.E, Matroid.eRank_def, Eq.trans_le, Matroid.eRk_le_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk X ≤ M.eRk Y
⊢ M.eRk X ≤ M.eRk Y

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 Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
obtain : ∀ (J : Set α) (hJ : M.IsBasis' J Y) (hIJ : I ⊆ J), M.eRk X ≤ M.eRk Y
⊢ M.eRk X ≤ M.eRk Y

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis'_of_subset (hI.subset.trans hXY)

Premises used: HasSubset.Subset.trans, Matroid.IsBasis'.indep, Matroid.Indep.subset_isBasis'_of_subset, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
rw : I.encard ≤ J.encard
⊢ M.eRk X ≤ M.eRk Y

Tactic:
rw [hI.eRk_eq_encard, hJ.eRk_eq_encard]

Premises used: Matroid.IsBasis'.eRk_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ I.encard ≤ J.encard

Tactic:
encard_mono hIJ

Premises used: Set.encard_mono
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ I.encard ≤ J.encard

Tactic:
exact encard_mono hIJ

Premises used: Set.encard_mono
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRk (X ∩ M.E) ≤ M.eRk M.E
⊢ M.eRk X ≤ M.eRank

Tactic:
rw [eRank_def, ← eRk_inter_ground]

Premises used: Matroid.eRank_def, Matroid.eRk_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (X ∩ M.E) ≤ M.eRk M.E

Tactic:
M.eRk_mono inter_subset_right

Premises used: Matroid.eRk_mono, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (X ∩ M.E) ≤ M.eRk M.E

Tactic:
exact M.eRk_mono inter_subset_right

Premises used: Matroid.eRk_mono, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hYX : M.eRk Y ≤ M.eRk X
⊢ M.eRk X = M.eRk Y

Tactic:
(M.eRk_mono hXY).antisymm hYX

Premises used: Matroid.eRk_mono, LE.le.antisymm
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
⊢ n ≤ M.eRk X ↔ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

Tactic:
⟨fun h ↦ ?_, fun ⟨I, hIX, hI, hIc⟩ ↦ ?_⟩

Premises used: LE.le, _private.0.Matroid.le_eRk_iff.match_1, Iff.intro, Matroid.eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
refine_1 : ∀ (h : n ≤ M.eRk X), ∃ I ⊆ X, M.Indep I ∧ I.encard = n
refine_2 :
  (∃ I ⊆ X, M.Indep I ∧ I.encard = n) → ∀ (I : Set α) (hIX : I ⊆ X) (hI : M.Indep I) (hIc : I.encard = n), n ≤ M.eRk X
⊢ n ≤ M.eRk X ↔ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨I, hIX, hI, hIc⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : n ≤ M.eRk X
refine_1 : ∀ (J : Set α) (hJ : M.IsBasis' J X), ∃ I ⊆ X, M.Indep I ∧ I.encard = n
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

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

Premises used: Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : n ≤ M.eRk X
J : Set α
hJ : M.IsBasis' J X
⊢ n ≤ J.encard

Tactic:
rw [← hJ.encard_eq_eRk] at h

Premises used: Matroid.IsBasis'.encard_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : n ≤ M.eRk X
J : Set α
hJ : M.IsBasis' J X
h₁ : n ≤ J.encard
⊢ M.IsBasis' J X

Tactic:
rw [← hJ.encard_eq_eRk] at h

Premises used: Matroid.IsBasis'.encard_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
J : Set α
h : n ≤ J.encard
hJ : M.IsBasis' J X
refine_1 : ∀ (I : Set α) (hIJ : I ⊆ J) (h : I.encard ≤ J.encard), ∃ I_1 ⊆ X, M.Indep I_1 ∧ I_1.encard = I.encard
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

Tactic:
obtain ⟨I, hIJ, rfl⟩ := exists_subset_encard_eq h

Premises used: Set.exists_subset_encard_eq, rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X J : Set α
hJ : M.IsBasis' J X
I : Set α
hIJ : I ⊆ J
h : I.encard ≤ J.encard
⊢ ∃ I_1 ⊆ X, M.Indep I_1 ∧ I_1.encard = I.encard

Tactic:
⟨_, hIJ.trans hJ.subset, hJ.indep.subset hIJ, rfl⟩

Premises used: HasSubset.Subset.trans, Matroid.Indep.subset, Matroid.IsBasis'.indep, And.intro, Exists.intro, Matroid.IsBasis'.subset, rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X J : Set α
hJ : M.IsBasis' J X
I : Set α
hIJ : I ⊆ J
h : I.encard ≤ J.encard
⊢ ∃ I_1 ⊆ X, M.Indep I_1 ∧ I_1.encard = I.encard

Tactic:
exact ⟨_, hIJ.trans hJ.subset, hJ.indep.subset hIJ, rfl⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
refine_2 : M.eRk I ≤ M.eRk X
⊢ n ≤ M.eRk X

Tactic:
rw [← hIc, ← hI.eRk_eq_encard]

Premises used: Matroid.Indep.eRk_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ M.eRk I ≤ M.eRk X

Tactic:
M.eRk_mono hIX

Premises used: Matroid.eRk_mono
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ M.eRk I ≤ M.eRk X

Tactic:
exact M.eRk_mono hIX

Premises used: Matroid.eRk_mono
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
⊢ M.eRk X ≤ n ↔ ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n

Tactic:
⟨fun h I hIX hI ↦ (hI.eRk_eq_encard.symm.trans_le ((M.eRk_mono hIX).trans h)), fun h ↦ ?_⟩

Premises used: Matroid.eRk_mono, Matroid.Indep.eRk_eq_encard, Eq.trans_le, Iff.intro, LE.le.trans, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
refine : ∀ (h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n), M.eRk X ≤ n
⊢ M.eRk X ≤ n ↔ ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n

Tactic:
refine ⟨fun h I hIX hI ↦ (hI.eRk_eq_encard.symm.trans_le ((M.eRk_mono hIX).trans h)), fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk X ≤ n
⊢ M.eRk X ≤ n

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 α
n : ℕ∞
h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.IsBasis' I X
rw : I.encard ≤ n
⊢ M.eRk X ≤ n

Tactic:
rw [← hI.encard_eq_eRk]

Premises used: Matroid.IsBasis'.encard_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.IsBasis' I X
⊢ I.encard ≤ n

Tactic:
h hI.subset hI.indep

Premises used: Matroid.IsBasis'.indep, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.IsBasis' I X
⊢ I.encard ≤ n

Tactic:
exact h hI.subset hI.indep

Premises used: Matroid.IsBasis'.indep, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ I.encard ≤ M.eRk X

Tactic:
hI.eRk_eq_encard ▸ M.eRk_mono hIX

Premises used: Matroid.eRk_mono, Matroid.Indep.eRk_eq_encard, Eq.rec
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
rw : M.eRk I ≤ M.eRk M.E
⊢ I.encard ≤ M.eRank

Tactic:
rw [← hI.eRk_eq_encard, eRank_def]

Premises used: Matroid.Indep.eRk_eq_encard, Matroid.eRank_def
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.eRk I ≤ M.eRk M.E

Tactic:
M.eRk_mono hI.subset_ground

Premises used: Matroid.eRk_mono, Matroid.Indep.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.eRk I ≤ M.eRk M.E

Tactic:
exact M.eRk_mono hI.subset_ground

Premises used: Matroid.eRk_mono, Matroid.Indep.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
obtain : ∀ (I : Set α) (hI : M.IsBasis I (X ∩ M.E)), M.eRk X = 0 ↔ X ∩ M.E ⊆ M.loops
⊢ M.eRk X = 0 ↔ X ∩ M.E ⊆ M.loops

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)

Premises used: Matroid.E, Inter.inter, Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
rw : I = ∅ ↔ X ∩ M.E ⊆ M.loops
⊢ M.eRk X = 0 ↔ X ∩ M.E ⊆ M.loops

Tactic:
rw [← eRk_inter_ground, ← hI.encard_eq_eRk, encard_eq_zero]

Premises used: Set.encard_eq_zero, Matroid.IsBasis.encard_eq_eRk, Matroid.eRk_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
h : I = ∅
⊢ X ∩ M.E ⊆ M.loops

Tactic:
simpa [h] using hI
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
refine : ∀ (h : X ∩ M.E ⊆ M.loops) (e : α) (heI : e ∈ I), False
⊢ I = ∅ ↔ X ∩ M.E ⊆ M.loops

Tactic:
refine ⟨fun h ↦ by simpa [h] using hI, fun h ↦ eq_empty_iff_forall_notMem.2 fun e heI ↦ ?_⟩