awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ M.Spanning X ↔ M.eRank ≤ M.eRk X
have rw₁ : M.eRank ≤ M.eRk X ↔ M.eRank ≤ M.eRk X
Tactic: rw [spanning_iff_eRk_le', and_iff_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ (M ↾ X).eRank = M.eRank
have rw : (M ↾ X).eRk (M ↾ X).E = M.eRank
Tactic: rw [eRank_def, restrict_ground_eq, restrict_eRk_eq _ rfl.subset, hX.eRk_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
rw : (M ↾ X).eRk (M ↾ X).E = M.eRank
⊢ (M ↾ X).eRank = M.eRank
have rw₁ : (M ↾ X).eRk X = M.eRank
Tactic: rw [eRank_def, restrict_ground_eq, restrict_eRk_eq _ rfl.subset, hX.eRk_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ (M ↾ X).eRank = M.eRank
have rw₂ : M.eRk X = M.eRank
Tactic: rw [eRank_def, restrict_ground_eq, restrict_eRk_eq _ rfl.subset, hX.eRk_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ (M ↾ X).eRank = M.eRank
have rw₃ : M.eRank = M.eRank
Tactic: rw [eRank_def, restrict_ground_eq, restrict_eRk_eq _ rfl.subset, hX.eRk_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf).eRank = M.eRank
have obtain : ∀ (B : Set α) (hB : M.IsBase B), (M.map f hf).eRank = M.eRank
Tactic: obtain ⟨B, hB⟩ := M.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
⊢ (M.map f hf).eRank = M.eRank
have rw : (f '' B).encard = M.eRank
Tactic: rw [← (hB.map hf).encard_eq_eRank, ← hB.encard_eq_eRank, (hf.mono hB.subset_ground).encard_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ (M.map f hf).eRank = M.eRank
have rw₁ : (f '' B).encard = B.encard
Tactic: rw [← (hB.map hf).encard_eq_eRank, ← hB.encard_eq_eRank, (hf.mono hB.subset_ground).encard_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ (M.map f hf).eRank = M.eRank
have rw₂ : B.encard = B.encard
Tactic: rw [← (hB.map hf).encard_eq_eRank, ← hB.encard_eq_eRank, (hf.mono hB.subset_ground).encard_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X : Set α
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
hX : X ⊆ M.E
⊢ (M.map f hf).eRk (f '' X) = M.eRk X
have obtain : ∀ (I : Set α) (hI : M.IsBasis I X), (M.map f hf).eRk (f '' 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
X : Set α
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ (M.map f hf).eRk (f '' X) = M.eRk X
have rw : (M.map f hf).eRk (f '' X) = I.encard
Tactic: rw [hI.eRk_eq_encard, (hI.map hf).eRk_eq_encard, (hf.mono hI.indep.subset_ground).encard_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ (M.map f hf).eRk (f '' X) = M.eRk X
have rw₁ : (f '' I).encard = I.encard
Tactic: rw [hI.eRk_eq_encard, (hI.map hf).eRk_eq_encard, (hf.mono hI.indep.subset_ground).encard_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ (M.map f hf).eRk (f '' X) = M.eRk X
have rw₂ : I.encard = I.encard
Tactic: rw [hI.eRk_eq_encard, (hI.map hf).eRk_eq_encard, (hf.mono hI.indep.subset_ground).encard_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X : Set α
⊢ (M.comap f).eRk X = M.eRk (f '' X)
have obtain : ∀ (I : Set α) (hI : (M.comap f).IsBasis' I X), (M.comap f).eRk X = M.eRk (f '' X)
Tactic: obtain ⟨I, hI⟩ := (M.comap f).exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X I : Set α
hI : (M.comap f).IsBasis' I X
⊢ (M.comap f).eRk X = M.eRk (f '' X)
have hI' : M.IsBasis' (f '' I) (f '' X)
Tactic: obtain ⟨hI', hinj, -⟩ := comap_isBasis'_iff.1 hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
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)
⊢ (M.comap f).eRk X = M.eRk (f '' X)
have hinj : InjOn f I
Tactic: obtain ⟨hI', hinj, -⟩ := comap_isBasis'_iff.1 hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ (M.comap f).eRk X = M.eRk (f '' X)
have rw : I.encard = M.eRk (f '' X)
Tactic: rw [← hI.encard_eq_eRk, ← hI'.encard_eq_eRk, hinj.encard_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ (M.comap f).eRk X = M.eRk (f '' X)
have rw₁ : I.encard = (f '' I).encard
Tactic: rw [← hI.encard_eq_eRk, ← hI'.encard_eq_eRk, hinj.encard_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ (M.comap f).eRk X = M.eRk (f '' X)
have rw₂ : I.encard = I.encard
Tactic: rw [← hI.encard_eq_eRk, ← hI'.encard_eq_eRk, hinj.encard_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X Y : Set α
⊢ (loopyOn Y).eRk X = 0
have obtain : ∀ (I : Set α) (hI : (loopyOn Y).IsBasis' I X), (loopyOn Y).eRk X = 0
Tactic: obtain ⟨I, hI⟩ := (loopyOn Y).exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X Y I : Set α
hI : (loopyOn Y).IsBasis' I X
⊢ (loopyOn Y).eRk X = 0
have rw : I.encard = 0
Tactic: rw [hI.eRk_eq_encard, loopyOn_indep_iff.1 hI.indep, encard_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X Y I : Set α
hI : (loopyOn Y).IsBasis' I X
rw : I.encard = 0
⊢ (loopyOn Y).eRk X = 0
have rw₁ : encard.{u_1} (α := α) ∅ = 0
Tactic: rw [hI.eRk_eq_encard, loopyOn_indep_iff.1 hI.indep, encard_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X Y I : Set α
hI : (loopyOn Y).IsBasis' I X
rw : I.encard = 0
rw₁ : encard.{u_1} (α := α) ∅ = 0
⊢ (loopyOn Y).eRk X = 0
have rw₂ : Eq (α := ℕ∞) 0 0
Tactic: rw [hI.eRk_eq_encard, loopyOn_indep_iff.1 hI.indep, encard_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X : Set α
⊢ (loopyOn X).eRank = 0
have rw : (loopyOn X).eRk (loopyOn X).E = 0
Tactic: rw [eRank_def, eRk_loopyOn]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X : Set α
rw : (loopyOn X).eRk (loopyOn X).E = 0
⊢ (loopyOn X).eRank = 0
have rw₁ : Eq (α := ℕ∞) 0 0
Tactic: rw [eRank_def, eRk_loopyOn]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
h : M = loopyOn M.E
⊢ M.eRank = 0
have rw : (loopyOn M.E).eRank = 0
Tactic: rw [h, eRank_loopyOn]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
h : M = loopyOn M.E
rw : (loopyOn M.E).eRank = 0
⊢ M.eRank = 0
have rw₁ : Eq (α := ℕ∞) 0 0
Tactic: rw [h, eRank_loopyOn]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.eRank = 0 ↔ M = loopyOn M.E
have refine : ∀ (h : M.eRank = 0), M.closure ∅ = M.E
Tactic: refine ⟨fun h ↦ closure_empty_eq_ground_iff.1 ?_, fun h ↦ by rw [h, eRank_loopyOn]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
h : M.eRank = 0
⊢ M.closure ∅ = M.E
have obtain : ∀ (B : Set α) (hB : M.IsBase B), M.closure ∅ = M.E
Tactic: obtain ⟨B, hB⟩ := M.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
Goal:
α : Type u_1
M : Matroid α
h : M.eRank = 0
B : Set α
hB : M.IsBase B
⊢ M.closure ∅ = M.E
have h₁ : B = ∅
Tactic: rw [← hB.encard_eq_eRank, encard_eq_zero] at h
Cleared hypotheses: h, hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : B = ∅
hB : M.IsBase B
⊢ M.closure ∅ = M.E
have rw : M.closure B = M.E
Tactic: rw [← h, hB.closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : B = ∅
hB : M.IsBase B
rw : M.closure B = M.E
⊢ M.closure ∅ = M.E
have rw₁ : M.E = M.E
Tactic: rw [← h, hB.closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_2
⊢ (emptyOn α).eRank = 0
have rw : emptyOn α = loopyOn (emptyOn α).E
Tactic: rw [eRank_eq_zero_iff, emptyOn_ground, loopyOn_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_2
rw : emptyOn α = loopyOn (emptyOn α).E
⊢ (emptyOn α).eRank = 0
have rw₁ : emptyOn α = loopyOn ∅
Tactic: rw [eRank_eq_zero_iff, emptyOn_ground, loopyOn_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_2
rw : emptyOn α = loopyOn (emptyOn α).E
rw₁ : emptyOn α = loopyOn ∅
⊢ (emptyOn α).eRank = 0
have rw₂ : emptyOn α = emptyOn α
Tactic: rw [eRank_eq_zero_iff, emptyOn_ground, loopyOn_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : M = loopyOn X
⊢ M.eRank = 0 ∧ M.E = X
have rw : (loopyOn X).eRank = 0 ∧ (loopyOn X).E = X
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
h_1 : M.eRank = 0 ∧ M.E = X
h : M.eRank = 0
h' : M.E = X
⊢ M = loopyOn X
have rw : M = loopyOn M.E
Tactic: rw [← h', ← eRank_eq_zero_iff, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ M = loopyOn X
have rw₂ : Eq (α := ℕ∞) 0 0
Tactic: rw [← h', ← eRank_eq_zero_iff, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X : Set α
⊢ (freeOn X).eRank = X.encard
have rw : (freeOn X).eRk (freeOn X).E = X.encard
Tactic: rw [eRank_def, freeOn_ground, (freeOn_indep_iff.2 rfl.subset).eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X : Set α
rw : (freeOn X).eRk (freeOn X).E = X.encard
⊢ (freeOn X).eRank = X.encard
have rw₁ : (freeOn X).eRk X = X.encard
Tactic: rw [eRank_def, freeOn_ground, (freeOn_indep_iff.2 rfl.subset).eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X : Set α
rw : (freeOn X).eRk (freeOn X).E = X.encard
rw₁ : (freeOn X).eRk X = X.encard
⊢ (freeOn X).eRank = X.encard
have rw₂ : X.encard = X.encard
Tactic: rw [eRank_def, freeOn_ground, (freeOn_indep_iff.2 rfl.subset).eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X Y : Set α
hXY : X ⊆ Y
⊢ (freeOn Y).eRk X = X.encard
have obtain : ∀ (I : Set α) (hI : (freeOn Y).IsBasis I X), (freeOn Y).eRk X = X.encard
Tactic: obtain ⟨I, hI⟩ := (freeOn Y).exists_isBasis X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : (freeOn Y).IsBasis I X
⊢ (freeOn Y).eRk X = X.encard
have rw : I.encard = X.encard
Tactic: rw [hI.eRk_eq_encard, (freeOn_indep hXY).eq_of_isBasis hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : (freeOn Y).IsBasis I X
rw : I.encard = X.encard
⊢ (freeOn Y).eRk X = X.encard
have rw₁ : X.encard = X.encard
Tactic: rw [hI.eRk_eq_encard, (freeOn_indep hXY).eq_of_isBasis hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard
have obtain : ∀ (I : Set α) (hI : M✶.IsBasis I X), M✶.eRk X + M.eRank = M.eRk (M.E \ 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 : Set α
hX : X ⊆ M.E
I : Set α
hI : M✶.IsBasis I X
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard
have 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
Tactic: obtain ⟨B, hB, rfl⟩ := hI.exists_isBasis_inter_eq_of_superset hX
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
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✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard
have hB' : M✶.IsBase B
Tactic: have hB' : M✶.IsBase B := isBasis_ground_iff.1 hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
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✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard
have hd : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ Disjoint (B ∩ X) (M.E \ B)
have 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
Tactic: tauto_set
Cleared hypotheses: hX, hB, hI, hB', hd
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ Disjoint (M.E \ B ∩ (M.E \ X)) X
have 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
Tactic: tauto_set
Cleared hypotheses: hX, hB, hI, hB', hd
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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)
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard
have rw : (B ∩ X ∪ M.E \ B).encard = (M.E \ B ∩ (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)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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 = M.E \ B ∩ (M.E \ X) ∪ X
have 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
Tactic: tauto_set
Cleared hypotheses: hX, hB, hI, hB', hd
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + (X ∩ M.E).encard
have rw : M✶.eRk X + M.eRank = M.eRk (M.E \ (X ∩ M.E)) + (X ∩ M.E).encard
Tactic: rw [← diff_inter_self_eq_diff, ← eRk_dual_add_eRank .., ← dual_ground, 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.eRank = M.eRk (M.E \ (X ∩ M.E)) + (X ∩ M.E).encard
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + (X ∩ M.E).encard
have rw₁ : M✶.eRk X + M.eRank = M✶.eRk (X ∩ M.E) + M.eRank
Tactic: rw [← diff_inter_self_eq_diff, ← eRk_dual_add_eRank .., ← dual_ground, 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.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
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + (X ∩ M.E).encard
have rw₂ : M✶.eRk X + M.eRank = M✶.eRk (X ∩ M✶.E) + M.eRank
Tactic: rw [← diff_inter_self_eq_diff, ← eRk_dual_add_eRank .., ← dual_ground, 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.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
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + (X ∩ M.E).encard
have rw₃ : M✶.eRk X + M.eRank = M✶.eRk X + M.eRank
Tactic: rw [← diff_inter_self_eq_diff, ← eRk_dual_add_eRank .., ← dual_ground, eRk_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.eRank + M✶.eRank = M.E.encard
have obtain : ∀ (B : Set α) (hB : M.IsBase B), M.eRank + M✶.eRank = M.E.encard
Tactic: obtain ⟨B, hB⟩ := M.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.eRank + M✶.eRank = M.E.encard
have rw : B.encard + 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]
-- 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.E.encard
⊢ M.eRank + M✶.eRank = M.E.encard
have rw₁ : B.encard + (M.E \ B).encard = 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]
-- 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.E.encard
rw₁ : B.encard + (M.E \ B).encard = M.E.encard
⊢ M.eRank + M✶.eRank = M.E.encard
have rw₂ : (B ∪ M.E \ B).encard = 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]
-- 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.E.encard
rw₁ : B.encard + (M.E \ B).encard = M.E.encard
rw₂ : (B ∪ M.E \ B).encard = M.E.encard
⊢ M.eRank + M✶.eRank = M.E.encard
have rw₃ : M.E.encard = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
⊢ M.IsRkFinite Y
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I Y), M.IsRkFinite Y
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis' Y
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
I : Set α
hI : M.IsBasis' I Y
⊢ M.IsRkFinite Y
have obtain : ∀ (J : Set α) (hJ : M.IsBasis' J X) (hIJ : I ⊆ J), M.IsRkFinite 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.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.IsRkFinite X ↔ ∃ (I : Set α), M.IsBasis I X ∧ I.Finite
have simp_rw : (∃ (I : Set α), M.IsBasis' I X ∧ I.Finite) ↔ ∃ (I : Set α), M.IsBasis I X ∧ I.Finite
Tactic: simp_rw [isRkFinite_iff_exists_isBasis', M.isBasis'_iff_isBasis hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.IsRkFinite M.E ↔ M.RankFinite
have rw : (M ↾ M.E).RankFinite ↔ M.RankFinite
Tactic: rw [IsRkFinite, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
rw : (M ↾ M.E).RankFinite ↔ M.RankFinite
⊢ M.IsRkFinite M.E ↔ M.RankFinite
have rw₁ : M.RankFinite ↔ M.RankFinite
Tactic: rw [IsRkFinite, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.IsRkFinite (M.closure X) ↔ M.IsRkFinite X
have rw : M.IsRkFinite (M.closure X) ↔ M.IsRkFinite (X ∩ M.E)
Tactic: rw [← isRkFinite_inter_ground_iff (X := X)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
⊢ M.IsRkFinite (X ∪ Y)
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I X) (hIfin : I.Finite), M.IsRkFinite (X ∪ Y)
Tactic: obtain ⟨I, hI, hIfin⟩ := hX.exists_finite_isBasis'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
⊢ M.IsRkFinite (X ∪ Y)
have obtain : ∀ (J : Set α) (hJ : M.IsBasis' J Y) (hJfin : J.Finite), M.IsRkFinite (X ∪ Y)
Tactic: obtain ⟨J, hJ, hJfin⟩ := hY.exists_finite_isBasis'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ M.IsRkFinite (X ∪ Y)
have rw : M.IsRkFinite ((X ∪ Y) ∩ M.E)
Tactic: rw [← isRkFinite_inter_ground_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ M.IsRkFinite ((X ∪ Y) ∩ M.E)
have refine : (X ∪ Y) ∩ M.E ⊆ M.closure (I ∪ J)
Tactic: refine (M.isRkFinite_of_finite (hIfin.union hJfin)).closure.subset ?_