awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
rw : M.eRk I = I.encard
⊢ M.eRk X = I.encard
have rw₁ : I.encard = I.encard
Tactic: rw [← hIX.eRk_eq_eRk, hIX.indep.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.eRk B = M.eRank
have rw : B.encard = M.eRank
Tactic: rw [hB.indep.eRk_eq_encard, eRank_def, hB.isBasis_ground.encard_eq_eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
rw : B.encard = M.eRank
⊢ M.eRk B = M.eRank
have rw₁ : B.encard = M.eRk M.E
Tactic: rw [hB.indep.eRk_eq_encard, eRank_def, hB.isBasis_ground.encard_eq_eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
rw : B.encard = M.eRank
rw₁ : B.encard = M.eRk M.E
⊢ M.eRk B = M.eRank
have rw₂ : M.eRk M.E = M.eRk M.E
Tactic: rw [hB.indep.eRk_eq_encard, eRank_def, hB.isBasis_ground.encard_eq_eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (X ∩ M.E) = M.eRk X
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk (X ∩ M.E) = M.eRk X
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ M.eRk (X ∩ M.E) = M.eRk X
have rw : M.eRk (X ∩ M.E) = M.eRk I
Tactic: rw [← hI.eRk_eq_eRk, hI.isBasis_inter_ground.eRk_eq_eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
rw : M.eRk (X ∩ M.E) = M.eRk I
⊢ M.eRk (X ∩ M.E) = M.eRk X
have rw₁ : M.eRk (X ∩ M.E) = M.eRk (X ∩ M.E)
Tactic: rw [← hI.eRk_eq_eRk, hI.isBasis_inter_ground.eRk_eq_eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (M.E ∩ X) = M.eRk X
have rw : M.eRk (X ∩ M.E) = M.eRk X
Tactic: rw [inter_comm, eRk_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRk (X ∩ M.E) = M.eRk X
⊢ M.eRk (M.E ∩ X) = M.eRk X
have rw₁ : M.eRk X = M.eRk X
Tactic: rw [inter_comm, eRk_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (X ∪ M.E) = M.eRank
have rw : M.eRk ((X ∪ M.E) ∩ M.E) = M.eRank
Tactic: rw [← eRk_inter_ground, inter_eq_self_of_subset_right subset_union_right, eRank_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRk ((X ∪ M.E) ∩ M.E) = M.eRank
⊢ M.eRk (X ∪ M.E) = M.eRank
have rw₁ : M.eRk M.E = M.eRank
Tactic: rw [← eRk_inter_ground, inter_eq_self_of_subset_right subset_union_right, eRank_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ M.eRk (X ∪ M.E) = M.eRank
have rw₂ : M.eRk M.E = M.eRk M.E
Tactic: rw [← eRk_inter_ground, inter_eq_self_of_subset_right subset_union_right, eRank_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (M.E ∪ X) = M.eRank
have rw : M.eRk (X ∪ M.E) = M.eRank
Tactic: rw [union_comm, eRk_union_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRk (X ∪ M.E) = M.eRank
⊢ M.eRk (M.E ∪ X) = M.eRank
have rw₁ : M.eRank = M.eRank
Tactic: rw [union_comm, eRk_union_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
⊢ M.eRk (insert e X) = M.eRk X
have rw : M.eRk (insert e X ∩ M.E) = M.eRk X
Tactic: rw [← eRk_inter_ground, insert_inter_of_notMem he, eRk_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
rw : M.eRk (insert e X ∩ M.E) = M.eRk X
⊢ M.eRk (insert e X) = M.eRk X
have rw₁ : M.eRk (X ∩ M.E) = M.eRk X
Tactic: rw [← eRk_inter_ground, insert_inter_of_notMem he, eRk_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ M.eRk (insert e X) = M.eRk X
have rw₂ : M.eRk X = M.eRk X
Tactic: rw [← eRk_inter_ground, insert_inter_of_notMem he, eRk_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.E ⊆ X
⊢ M.eRk X = M.eRank
have rw : M.eRk (X ∩ M.E) = M.eRank
Tactic: rw [← eRk_inter_ground, inter_eq_self_of_subset_right hX, eRank_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.E ⊆ X
rw : M.eRk (X ∩ M.E) = M.eRank
⊢ M.eRk X = M.eRank
have rw₁ : M.eRk M.E = M.eRank
Tactic: rw [← eRk_inter_ground, inter_eq_self_of_subset_right hX, eRank_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ M.eRk X = M.eRank
have rw₂ : M.eRk M.E = M.eRk M.E
Tactic: rw [← eRk_inter_ground, inter_eq_self_of_subset_right hX, eRank_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : Disjoint X Y
⊢ M.eRk (M.E \ X ∪ Y) = M.eRk (M.E \ X)
have rw : M.eRk ((M.E \ X ∪ Y) ∩ M.E) = 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⟩)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (M.E \ X ∪ Y) = M.eRk (M.E \ X)
have rw₁ : M.eRk (M.E \ X ∩ M.E ∪ Y ∩ M.E) = 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⟩)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (M.E \ X ∪ Y) = M.eRk (M.E \ X)
have rw₂ : M.eRk (M.E \ X ∪ Y ∩ M.E) = 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⟩)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (M.E \ X ∪ Y) = M.eRk (M.E \ X)
have rw₃ : M.eRk (M.E \ X) = 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⟩)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
inst : M.RankPos
⊢ 1 ≤ M.eRank
have obtain : ∀ (B : Set α) (hB : M.IsBase B), 1 ≤ M.eRank
Tactic: obtain ⟨B, hB⟩ := M.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
inst : M.RankPos
B : Set α
hB : M.IsBase B
⊢ 1 ≤ M.eRank
have rw : B.Nonempty
Tactic: rw [← hB.encard_eq_eRank, one_le_encard_iff_nonempty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.eRk univ = M.eRank
have rw : M.eRk (univ ∩ M.E) = M.eRank
Tactic: rw [← eRk_inter_ground, univ_inter, eRank_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
rw : M.eRk (univ ∩ M.E) = M.eRank
⊢ M.eRk univ = M.eRank
have rw₁ : M.eRk M.E = M.eRank
Tactic: rw [← eRk_inter_ground, univ_inter, eRank_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
rw : M.eRk (univ ∩ M.E) = M.eRank
rw₁ : M.eRk M.E = M.eRank
⊢ M.eRk univ = M.eRank
have rw₂ : M.eRk M.E = M.eRk M.E
Tactic: rw [← eRk_inter_ground, univ_inter, eRank_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.eRk ∅ = 0
have rw : encard.{u_1} (α := α) ∅ = 0
Tactic: rw [← M.empty_indep.isBasis_self.encard_eq_eRk, encard_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
rw : encard.{u_1} (α := α) ∅ = 0
⊢ M.eRk ∅ = 0
have rw₁ : Eq (α := ℕ∞) 0 0
Tactic: rw [← M.empty_indep.isBasis_self.encard_eq_eRk, encard_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (M.closure X) = M.eRk X
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk (M.closure X) = M.eRk X
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ M.eRk (M.closure X) = M.eRk X
have rw : M.eRk (M.closure I) = M.eRk X
Tactic: rw [← hI.closure_eq_closure, ← hI.indep.isBasis_closure.encard_eq_eRk, hI.encard_eq_eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
rw : M.eRk (M.closure I) = M.eRk X
⊢ M.eRk (M.closure X) = M.eRk X
have rw₁ : I.encard = M.eRk X
Tactic: rw [← hI.closure_eq_closure, ← hI.indep.isBasis_closure.encard_eq_eRk, hI.encard_eq_eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ M.eRk (M.closure X) = M.eRk X
have rw₂ : M.eRk X = M.eRk X
Tactic: rw [← hI.closure_eq_closure, ← hI.indep.isBasis_closure.encard_eq_eRk, hI.encard_eq_eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (X ∪ M.closure Y) = M.eRk (X ∪ Y)
have rw : M.eRk (M.closure (X ∪ M.closure Y)) = M.eRk (X ∪ Y)
Tactic: rw [← eRk_closure_eq, closure_union_closure_right_eq, eRk_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
rw : M.eRk (M.closure (X ∪ M.closure Y)) = M.eRk (X ∪ Y)
⊢ M.eRk (X ∪ M.closure Y) = M.eRk (X ∪ Y)
have rw₁ : M.eRk (M.closure (X ∪ Y)) = M.eRk (X ∪ Y)
Tactic: rw [← eRk_closure_eq, closure_union_closure_right_eq, eRk_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (X ∪ M.closure Y) = M.eRk (X ∪ Y)
have rw₂ : M.eRk (X ∪ Y) = M.eRk (X ∪ Y)
Tactic: rw [← eRk_closure_eq, closure_union_closure_right_eq, eRk_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (M.closure X ∪ Y) = M.eRk (X ∪ Y)
have rw : M.eRk (M.closure (M.closure X ∪ Y)) = M.eRk (X ∪ Y)
Tactic: rw [← eRk_closure_eq, closure_union_closure_left_eq, eRk_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
rw : M.eRk (M.closure (M.closure X ∪ Y)) = M.eRk (X ∪ Y)
⊢ M.eRk (M.closure X ∪ Y) = M.eRk (X ∪ Y)
have rw₁ : M.eRk (M.closure (X ∪ Y)) = M.eRk (X ∪ Y)
Tactic: rw [← eRk_closure_eq, closure_union_closure_left_eq, eRk_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (M.closure X ∪ Y) = M.eRk (X ∪ Y)
have rw₂ : M.eRk (X ∪ Y) = M.eRk (X ∪ Y)
Tactic: rw [← eRk_closure_eq, closure_union_closure_left_eq, eRk_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk (insert e (M.closure X)) = M.eRk (insert e X)
have rw : M.eRk (M.closure X ∪ {e}) = M.eRk (insert e X)
Tactic: rw [← union_singleton, eRk_union_closure_left_eq, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
rw : M.eRk (M.closure X ∪ {e}) = M.eRk (insert e X)
⊢ M.eRk (insert e (M.closure X)) = M.eRk (insert e X)
have rw₁ : M.eRk (X ∪ {e}) = M.eRk (insert e X)
Tactic: rw [← union_singleton, eRk_union_closure_left_eq, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (insert e (M.closure X)) = M.eRk (insert e X)
have rw₂ : M.eRk (insert e X) = M.eRk (insert e X)
Tactic: rw [← union_singleton, eRk_union_closure_left_eq, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
⊢ (M ↾ R).eRk X = M.eRk (X ∩ R)
have obtain : ∀ (I : Set α) (hI : (M ↾ R).IsBasis' I X), (M ↾ R).eRk X = M.eRk (X ∩ R)
Tactic: obtain ⟨I, hI⟩ := (M ↾ R).exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
R X I : Set α
hI : (M ↾ R).IsBasis' I X
⊢ (M ↾ R).eRk X = M.eRk (X ∩ R)
have rw : I.encard = M.eRk (X ∩ R)
Tactic: rw [hI.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
Goal:
α : Type u_1
M : Matroid α
R X I : Set α
hI : (M ↾ R).IsBasis' I X
⊢ I.encard = M.eRk (X ∩ R)
have hI₁ : 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
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
R X I : Set α
hI : M.IsBasis I (X ∩ R ∩ M.E) ∧ X ∩ R ⊆ R
⊢ I.encard = M.eRk (X ∩ R)
have rw : I.encard = M.eRk (X ∩ R ∩ M.E)
Tactic: rw [← eRk_inter_ground, ← hI.1.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ I.encard = M.eRk (X ∩ R)
have rw₁ : M.eRk (X ∩ R ∩ M.E) = M.eRk (X ∩ R ∩ M.E)
Tactic: rw [← eRk_inter_ground, ← hI.1.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X : Set α
M : Matroid α
R : Set α
h : X ⊆ R
⊢ (M ↾ R).eRk X = M.eRk X
have rw : M.eRk (X ∩ R) = M.eRk X
Tactic: rw [restrict_eRk_eq', inter_eq_self_of_subset_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X : Set α
M : Matroid α
R : Set α
h : X ⊆ R
rw : M.eRk (X ∩ R) = M.eRk X
⊢ (M ↾ R).eRk X = M.eRk X
have rw₁ : M.eRk X = M.eRk X
Tactic: rw [restrict_eRk_eq', inter_eq_self_of_subset_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
Y : Set α
⊢ M.eRk (I ∪ Y) = M.eRk (X ∪ Y)
have rw : M.eRk (M.closure I ∪ Y) = M.eRk (X ∪ Y)
Tactic: rw [← eRk_union_closure_left_eq, hIX.closure_eq_closure, eRk_union_closure_left_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (I ∪ Y) = M.eRk (X ∪ Y)
have rw₁ : M.eRk (M.closure X ∪ Y) = M.eRk (X ∪ Y)
Tactic: rw [← eRk_union_closure_left_eq, hIX.closure_eq_closure, eRk_union_closure_left_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (I ∪ Y) = M.eRk (X ∪ Y)
have rw₂ : M.eRk (X ∪ Y) = M.eRk (X ∪ Y)
Tactic: rw [← eRk_union_closure_left_eq, hIX.closure_eq_closure, eRk_union_closure_left_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
e : α
⊢ M.eRk (insert e I) = M.eRk (insert e X)
have rw : M.eRk (I ∪ {e}) = M.eRk (insert e X)
Tactic: rw [← union_singleton, hIX.eRk_eq_eRk_union, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (insert e I) = M.eRk (insert e X)
have rw₁ : M.eRk (X ∪ {e}) = M.eRk (insert e X)
Tactic: rw [← union_singleton, hIX.eRk_eq_eRk_union, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (insert e I) = M.eRk (insert e X)
have rw₂ : M.eRk (insert e X) = M.eRk (insert e X)
Tactic: rw [← union_singleton, hIX.eRk_eq_eRk_union, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
e : α
⊢ M.eRk (insert e I) = M.eRk (insert e X)
have rw : M.eRk (I ∪ {e}) = M.eRk (insert e X)
Tactic: rw [← union_singleton, hIX.eRk_eq_eRk_union, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (insert e I) = M.eRk (insert e X)
have rw₁ : M.eRk (X ∪ {e}) = M.eRk (insert e X)
Tactic: rw [← union_singleton, hIX.eRk_eq_eRk_union, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M.eRk (insert e I) = M.eRk (insert e X)
have rw₂ : M.eRk (insert e X) = M.eRk (insert e X)
Tactic: rw [← union_singleton, hIX.eRk_eq_eRk_union, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X ≤ X.encard
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk X ≤ X.encard
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ M.eRk X ≤ X.encard
have rw : I.encard ≤ X.encard
Tactic: rw [hI.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
⊢ M.eRk X ≤ M.eRk Y
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk X ≤ M.eRk Y
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
⊢ M.eRk X ≤ M.eRk Y
have obtain : ∀ (J : Set α) (hJ : M.IsBasis' J Y) (hIJ : I ⊆ J), M.eRk X ≤ M.eRk Y
Tactic: obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis'_of_subset (hI.subset.trans hXY)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ M.eRk X ≤ M.eRk Y
have rw : I.encard ≤ J.encard
Tactic: rw [hI.eRk_eq_encard, hJ.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X ≤ M.eRank
have rw : M.eRk (X ∩ M.E) ≤ M.eRk M.E
Tactic: rw [eRank_def, ← eRk_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
⊢ n ≤ M.eRk X ↔ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
have refine_1 : ∀ (h : n ≤ M.eRk X), ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Tactic: refine ⟨fun h ↦ ?_, fun ⟨I, hIX, hI, hIc⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
refine_1 : ∀ (h : n ≤ M.eRk X), ∃ I ⊆ X, M.Indep I ∧ I.encard = n
⊢ n ≤ M.eRk X ↔ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
have 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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨I, hIX, hI, hIc⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : n ≤ M.eRk X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
have refine_1 : ∀ (J : Set α) (hJ : M.IsBasis' J X), ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Tactic: obtain ⟨J, hJ⟩ := M.exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : n ≤ M.eRk X
J : Set α
hJ : M.IsBasis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
have h₁ : n ≤ J.encard
Tactic: rw [← hJ.encard_eq_eRk] at h
Cleared hypotheses: h, hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
J : Set α
h : n ≤ J.encard
hJ : M.IsBasis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
have refine_1 : ∀ (I : Set α) (hIJ : I ⊆ J) (h : I.encard ≤ J.encard), ∃ I_1 ⊆ X, M.Indep I_1 ∧ I_1.encard = I.encard
Tactic: obtain ⟨I, hIJ, rfl⟩ := exists_subset_encard_eq h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ n ≤ M.eRk X
have refine_2 : M.eRk I ≤ M.eRk X
Tactic: rw [← hIc, ← hI.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
⊢ M.eRk X ≤ n ↔ ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
have refine : ∀ (h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n), M.eRk X ≤ n
Tactic: refine ⟨fun h I hIX hI ↦ (hI.eRk_eq_encard.symm.trans_le ((M.eRk_mono hIX).trans h)), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
⊢ M.eRk X ≤ n
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk X ≤ n
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ M.eRk X ≤ n
have rw : I.encard ≤ n
Tactic: rw [← hI.encard_eq_eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ I.encard ≤ M.eRank
have rw : M.eRk I ≤ M.eRk M.E
Tactic: rw [← hI.eRk_eq_encard, eRank_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X = 0 ↔ X ∩ M.E ⊆ M.loops
have obtain : ∀ (I : Set α) (hI : M.IsBasis I (X ∩ M.E)), M.eRk X = 0 ↔ X ∩ M.E ⊆ M.loops
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)