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 α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
rw : M.eRk (M.closure (insert e X)) = M.eRk X + 1
rw₁ : M.eRk (M.closure (insert e I)) = M.eRk X + 1
rw₂ : M.eRk (M.closure (insert e I)) = I.encard + 1
⊢ M.eRk (insert e X) = M.eRk X + 1
have rw₃ : M.eRk (insert e I) = I.encard + 1
Tactic: rw [← eRk_closure_eq, ← closure_insert_congr_right hI.closure_eq_closure, hI.eRk_eq_encard,
    eRk_closure_eq, Indep.eRk_eq_encard (by tauto), encard_insert_of_notMem (by tauto)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
rw : M.eRk (M.closure (insert e X)) = M.eRk X + 1
rw₁ : M.eRk (M.closure (insert e I)) = M.eRk X + 1
rw₂ : M.eRk (M.closure (insert e I)) = I.encard + 1
rw₃ : M.eRk (insert e I) = I.encard + 1
⊢ M.eRk (insert e X) = M.eRk X + 1
have rw₄ : (insert e I).encard = I.encard + 1
Tactic: rw [← eRk_closure_eq, ← closure_insert_congr_right hI.closure_eq_closure, hI.eRk_eq_encard,
    eRk_closure_eq, Indep.eRk_eq_encard (by tauto), encard_insert_of_notMem (by tauto)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
rw : M.eRk (M.closure (insert e X)) = M.eRk X + 1
rw₁ : M.eRk (M.closure (insert e I)) = M.eRk X + 1
rw₂ : M.eRk (M.closure (insert e I)) = I.encard + 1
rw₃ : M.eRk (insert e I) = I.encard + 1
rw₄ : (insert e I).encard = I.encard + 1
⊢ M.eRk (insert e X) = M.eRk X + 1
have rw₅ : I.encard + 1 = I.encard + 1
Tactic: rw [← eRk_closure_eq, ← closure_insert_congr_right hI.closure_eq_closure, hI.eRk_eq_encard,
    eRk_closure_eq, Indep.eRk_eq_encard (by tauto), encard_insert_of_notMem (by tauto)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.eRk X < M.eRk Y
⊢ ¬Y ∩ M.E ⊆ M.closure X
have contrapose! : ∀ (h : Y ∩ M.E ⊆ M.closure X), M.eRk Y ≤ M.eRk X
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.eRk X < M.eRk Y
⊢ ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1
have hz : ¬Y ∩ M.E ⊆ M.closure X
Tactic: have hz : ¬ Y ∩ M.E ⊆ M.closure X := by
    contrapose! h
    simpa using M.eRk_mono h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.eRk X < M.eRk Y
hz : ¬Y ∩ M.E ⊆ M.closure X
⊢ ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1
have obtain : ∀ (e : α) (heX : e ∉ M.closure X) (heZ : e ∈ Y) (heE : e ∈ M.E), ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1
Tactic: obtain ⟨e, ⟨heZ, heE⟩, heX⟩ := not_subset.1 hz
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (Insert.insert e X) ≤ M.eRk X
⊢ M.closure X = M.closure Y
have refine : ∀ (hlt : M.eRk X < M.eRk Y), False
Tactic: refine hX.closure_eq_closure_of_subset_of_eRk_ge_eRk hXY <| not_lt.1 fun hlt ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (Insert.insert e X) ≤ M.eRk X
hlt : M.eRk X < M.eRk Y
⊢ False
have obtain : ∀ (z : α) (hz : z ∈ Y \ X) (hr : M.eRk (Insert.insert z X) = M.eRk X + 1), False
Tactic: obtain ⟨z, hz, hr⟩ := exists_eRk_insert_eq_add_one_of_lt hlt
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
⊢ M.eRk X = M.eRk Y
have pos : ∀ (hX : M.IsRkFinite X), M.eRk X = M.eRk Y
Tactic: by_cases hX : M.IsRkFinite X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
pos : ∀ (hX : M.IsRkFinite X), M.eRk X = M.eRk Y
⊢ M.eRk X = M.eRk Y
have neg : ∀ (hX : ¬M.IsRkFinite X), M.eRk X = M.eRk Y
Tactic: by_cases hX : M.IsRkFinite X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : M.IsRkFinite X
⊢ M.eRk X = M.eRk Y
have pos : M.eRk (M.closure X) = M.eRk Y
Tactic: rw [← eRk_closure_eq, hX.closure_eq_closure_of_subset_of_forall_insert hXY hY, eRk_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : M.IsRkFinite X
pos : M.eRk (M.closure X) = M.eRk Y
⊢ M.eRk X = M.eRk Y
have pos₁ : M.eRk (M.closure Y) = M.eRk Y
Tactic: rw [← eRk_closure_eq, hX.closure_eq_closure_of_subset_of_forall_insert hXY hY, eRk_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : M.IsRkFinite X
pos : M.eRk (M.closure X) = M.eRk Y
pos₁ : M.eRk (M.closure Y) = M.eRk Y
⊢ M.eRk X = M.eRk Y
have pos₂ : M.eRk Y = M.eRk Y
Tactic: rw [← eRk_closure_eq, hX.closure_eq_closure_of_subset_of_forall_insert hXY hY, eRk_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : ¬M.IsRkFinite X
⊢ M.eRk X = M.eRk Y
have neg : ⊤ = M.eRk Y
Tactic: rw [eRk_eq_top_iff.2 hX, eRk_eq_top_iff.2 (mt (fun h ↦ h.subset hXY) hX)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : ¬M.IsRkFinite X
neg : ⊤ = M.eRk Y
⊢ M.eRk X = M.eRk Y
have neg₁ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [eRk_eq_top_iff.2 hX, eRk_eq_top_iff.2 (mt (fun h ↦ h.subset hXY) hX)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.Indep I
⊢ M.eRk I = I.encard
have rw : I.encard = I.encard
Tactic: rw [h.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
⊢ M.Indep I ↔ M.eRk I = I.encard
have refine : ∀ (h : M.eRk I = I.encard), M.Indep I
Tactic: refine ⟨fun h ↦ by rw [h.eRk_eq_encard], fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
⊢ M.Indep I
have obtain : ∀ (J : Set α) (hJ : M.IsBasis' J I), M.Indep I
Tactic: obtain ⟨J, hJ⟩ := M.exists_isBasis' I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
⊢ M.Indep I
have rw : M.Indep J
Tactic: rw [← hI.eq_of_subset_of_encard_le' hJ.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
rw : M.Indep J
⊢ M.Indep I
have rw₁ : I.encard ≤ J.encard
Tactic: rw [← hI.eq_of_subset_of_encard_le' hJ.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
⊢ I.encard ≤ J.encard
have rw : M.eRk I ≤ J.encard
Tactic: rw [← h, ← hJ.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
rw : M.eRk I ≤ J.encard
⊢ I.encard ≤ J.encard
have rw₁ : M.eRk I ≤ M.eRk I
Tactic: rw [← h, ← hJ.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
⊢ M.Indep I ↔ M.eRk I = I.encard
have refine : ∀ (h : M.eRk I = I.encard), M.Indep I
Tactic: refine ⟨Indep.eRk_eq_encard, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
h : M.eRk I = I.encard
⊢ M.Indep I
have inl : ∀ (hfin : I.Finite), M.Indep I
Tactic: obtain hfin | hinf := I.finite_or_infinite
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
h : M.eRk I = I.encard
inl : ∀ (hfin : I.Finite), M.Indep I
⊢ M.Indep I
have inr : ∀ (hinf : I.Infinite), M.Indep I
Tactic: obtain hfin | hinf := I.finite_or_infinite
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
h : M.eRk I = I.encard
hinf : I.Infinite
⊢ M.Indep I
have h₁ : M.eRk I = ⊤
Tactic: rw [hinf.encard_eq] at h
Cleared hypotheses: h, hinf
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
⊢ M.Indep I
have rw : M.eRk I = I.encard
Tactic: rw [indep_iff_eRk_eq_encard_of_finite _]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
rw : M.eRk I = I.encard
⊢ M.Indep I
have rw₁ : I.Finite
Tactic: rw [indep_iff_eRk_eq_encard_of_finite _]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
⊢ M.eRk X < X.encard ↔ M.Dep X
have refine : ∀ (h : M.eRk X < X.encard), M.Dep X
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ eRk_lt_encard_of_dep_of_finite hX h⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
h : M.eRk X < X.encard
⊢ M.Dep X
have rw : ¬M.eRk X = X.encard
Tactic: rw [← not_indep_iff, indep_iff_eRk_eq_encard_of_finite hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
hX : M.Dep X
⊢ M.eRk X < X.encard
have refine : M.eRk X ≠ X.encard
Tactic: refine (M.eRk_le_encard X).lt_of_ne ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
hX : M.Dep X
⊢ M.eRk X ≠ X.encard
have rw : ¬M.Indep X
Tactic: rw [ne_eq, ← indep_iff_eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
⊢ M.IsBasis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
have refine : I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X → ∀ (hIX : I ⊆ X) (hI : M.Indep I) (hcard : I.encard = M.eRk X), M.IsBasis' I X
Tactic: refine ⟨fun h ↦ ⟨h.subset,h.indep, h.eRk_eq_encard.symm⟩, fun ⟨hIX, hI, hcard⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
h : I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.eRk X
⊢ M.IsBasis' I X
have obtain : ∀ (J : Set α) (hJ : M.IsBasis' J X) (hIJ : I ⊆ J), M.IsBasis' I X
Tactic: obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis'_of_subset hIX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
hX : X ⊆ M.E
⊢ M.IsBasis I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
have rw : M.IsBasis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
Tactic: rw [← isBasis'_iff_isBasis, isBasis'_iff_indep_encard_eq_of_finite hIfin]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
hX : X ⊆ M.E
rw : M.IsBasis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
⊢ M.IsBasis I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
have rw₁ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
Tactic: rw [← isBasis'_iff_isBasis, isBasis'_iff_indep_encard_eq_of_finite hIfin]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIfin : I.Finite
hIX : I ⊆ X
h : M.eRk X ≤ M.eRk I
⊢ I.encard = M.eRk X
have rw : I.encard = M.eRk I
Tactic: rw [h.antisymm (M.eRk_mono hIX), hI.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIfin : I.Finite
hIX : I ⊆ X
h : M.eRk X ≤ M.eRk I
rw : I.encard = M.eRk I
⊢ I.encard = M.eRk X
have rw₁ : I.encard = I.encard
Tactic: rw [h.antisymm (M.eRk_mono hIX), hI.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ M.eRk C + 1 = C.encard
have obtain : ∀ (I : Set α) (hI : M.IsBasis I C), M.eRk C + 1 = C.encard
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis C
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
I : Set α
hI : M.IsBasis I C
⊢ M.eRk C + 1 = C.encard
have obtain : ∀ (e : α) (heI : e ∉ I) (hC : M.IsCircuit (insert e I)) (hI : M.IsBasis I (insert e I)) (heC : e ∈ insert e I),
  M.eRk (insert e I) + 1 = (insert e I).encard
Tactic: obtain ⟨e, ⟨heC, heI⟩, rfl⟩ := hC.isBasis_iff_insert_eq.1 hI
Cleared hypotheses: C, hC, hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
heI : e ∉ I
hC : M.IsCircuit (insert e I)
hI : M.IsBasis I (insert e I)
heC : e ∈ insert e I
⊢ M.eRk (insert e I) + 1 = (insert e I).encard
have rw : I.encard + 1 = (insert e I).encard
Tactic: rw [hI.eRk_eq_encard, encard_insert_of_notMem heI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
heI : e ∉ I
hC : M.IsCircuit (insert e I)
hI : M.IsBasis I (insert e I)
heC : e ∈ insert e I
rw : I.encard + 1 = (insert e I).encard
⊢ M.eRk (insert e I) + 1 = (insert e I).encard
have rw₁ : I.encard + 1 = I.encard + 1
Tactic: rw [hI.eRk_eq_encard, encard_insert_of_notMem heI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
⊢ M.eRk {e} = 0
have rw : M.eRk (M.closure {e}) = 0
Tactic: rw [← eRk_closure_eq, he.closure, loops, eRk_closure_eq, eRk_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
rw : M.eRk (M.closure {e}) = 0
⊢ M.eRk {e} = 0
have rw₁ : M.eRk M.loops = 0
Tactic: rw [← eRk_closure_eq, he.closure, loops, eRk_closure_eq, eRk_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
rw : M.eRk (M.closure {e}) = 0
rw₁ : M.eRk M.loops = 0
⊢ M.eRk {e} = 0
have rw₂ : M.eRk (M.closure ∅) = 0
Tactic: rw [← eRk_closure_eq, he.closure, loops, eRk_closure_eq, eRk_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
rw : M.eRk (M.closure {e}) = 0
rw₁ : M.eRk M.loops = 0
rw₂ : M.eRk (M.closure ∅) = 0
⊢ M.eRk {e} = 0
have rw₃ : M.eRk ∅ = 0
Tactic: rw [← eRk_closure_eq, he.closure, loops, eRk_closure_eq, eRk_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
rw : M.eRk (M.closure {e}) = 0
rw₁ : M.eRk M.loops = 0
rw₂ : M.eRk (M.closure ∅) = 0
rw₃ : M.eRk ∅ = 0
⊢ M.eRk {e} = 0
have rw₄ : Eq (α := ℕ∞) 0 0
Tactic: rw [← eRk_closure_eq, he.closure, loops, eRk_closure_eq, eRk_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
⊢ M.eRk {e} = 1
have rw : encard (α := α) {e} = 1
Tactic: rw [← he.indep.isBasis_self.encard_eq_eRk, encard_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
rw : encard (α := α) {e} = 1
⊢ M.eRk {e} = 1
have rw₁ : Eq (α := ℕ∞) 1 1
Tactic: rw [← he.indep.isBasis_self.encard_eq_eRk, encard_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.eRk {e} = 1 ↔ M.IsNonloop e
have refine : ∀ (h : M.eRk {e} = 1), M.IsNonloop e
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.eRk_eq⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.eRk {e} = 1
⊢ M.IsNonloop e
have rwa : M.Indep {e}
Tactic: rwa [← indep_singleton, indep_iff_eRk_eq_encard_of_finite (by simp), encard_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.eRk {e} = 1
rwa : M.Indep {e}
⊢ M.IsNonloop e
have rwa₁ : M.eRk {e} = encard (α := α) {e}
Tactic: rwa [← indep_singleton, indep_iff_eRk_eq_encard_of_finite (by simp), encard_singleton]
-- 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 = 1 ↔ ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
have refine_1 : M.eRk X = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
Tactic: refine ⟨?_, fun ⟨e, heX, he, hXe⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
refine_1 : M.eRk X = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
⊢ M.eRk X = 1 ↔ ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
have refine_2 : (∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}) →
  ∀ (e : α) (heX : e ∈ X) (he : M.IsNonloop e) (hXe : X ⊆ M.closure {e}), M.eRk X = 1
Tactic: refine ⟨?_, fun ⟨e, heX, he, hXe⟩ ↦ ?_⟩
-- 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 = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
have refine_1 : ∀ (I : Set α) (hI : M.IsBasis I X), M.eRk X = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
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 = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
have refine_1 : (∃ (x : α), I = {x}) → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
Tactic: rw [hI.eRk_eq_encard, encard_eq_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
h : ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
e : α
heX : e ∈ X
he : M.IsNonloop e
hXe : X ⊆ M.closure {e}
⊢ M.eRk X = 1
have refine_2 : M.eRk X = M.eRk {e}
Tactic: rw [← he.eRk_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
⊢ M.eRk X ≤ 1 ↔ ∃ e ∈ M.E, X ⊆ M.closure {e}
have refine_1 : ∀ (h : M.eRk X ≤ 1), ∃ e ∈ M.E, X ⊆ M.closure {e}
Tactic: refine ⟨fun h ↦ ?_, fun ⟨e, _, he⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
refine_1 : ∀ (h : M.eRk X ≤ 1), ∃ e ∈ M.E, X ⊆ M.closure {e}
⊢ M.eRk X ≤ 1 ↔ ∃ e ∈ M.E, X ⊆ M.closure {e}
have refine_2 : (∃ e ∈ M.E, X ⊆ M.closure {e}) → ∀ e ∈ M.E, ∀ (he : X ⊆ M.closure {e}), M.eRk X ≤ 1
Tactic: refine ⟨fun h ↦ ?_, fun ⟨e, _, he⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
h : M.eRk X ≤ 1
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}
have refine_1 : ∀ (I : Set α) (hI : M.IsBasis I X), ∃ e ∈ M.E, X ⊆ M.closure {e}
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
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
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}
have h₁ : I = ∅ ∨ ∃ (x : α), I = {x}
Tactic: rw [hI.eRk_eq_encard, encard_le_one_iff_eq] at h
Cleared hypotheses: h, hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}
have refine_1 : ∀ (hI : M.IsBasis ∅ X), ∃ e ∈ M.E, X ⊆ M.closure {e}
Tactic: obtain (rfl | ⟨e, rfl⟩) := h
Cleared hypotheses: I, h, hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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}
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}
have refine_1₁ : ∀ (e : α) (hI : M.IsBasis {e} X), ∃ e ∈ M.E, X ⊆ M.closure {e}
Tactic: obtain (rfl | ⟨e, rfl⟩) := h
Cleared hypotheses: I, h, hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.Nonempty
hX : X ⊆ M.E
hI : M.IsBasis ∅ X
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}
have refine_1 : ∀ (e : α) (he : e ∈ M.E), ∃ e ∈ M.E, X ⊆ M.closure {e}
Tactic: obtain ⟨e, he⟩ := M.ground_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
have refine_2 : M.eRk (M.closure {e}) ≤ 1
Tactic: refine (M.eRk_mono he).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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 (M.closure {e}) ≤ 1
have refine_2 : M.eRk {e} ≤ encard (α := α) {e}
Tactic: rw [eRk_closure_eq, ← encard_singleton e]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ M.eRk X = M.eRank
have obtain : ∀ (B : Set α) (hB : M.IsBasis B X), M.eRk X = M.eRank
Tactic: obtain ⟨B, hB⟩ := M.exists_isBasis X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
B : Set α
hB : M.IsBasis B X
⊢ M.eRank ≤ M.eRk X
have rw : M.eRank ≤ B.encard
Tactic: rw [← hB.encard_eq_eRk, ← (hB.isBase_of_spanning hX).encard_eq_eRank]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
B : Set α
hB : M.IsBasis B X
rw : M.eRank ≤ B.encard
⊢ M.eRank ≤ M.eRk X
have rw₁ : B.encard ≤ B.encard
Tactic: rw [← hB.encard_eq_eRk, ← (hB.isBase_of_spanning hX).encard_eq_eRank]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
inst : M.RankFinite
⊢ M.Spanning X ↔ M.eRank ≤ M.eRk X ∧ X ⊆ M.E
have refine : M.eRank ≤ M.eRk X ∧ X ⊆ M.E → ∀ (h : M.eRank ≤ M.eRk X) (hX : X ⊆ M.E), M.Spanning X
Tactic: refine ⟨fun h ↦ ⟨h.eRk_eq.symm.le, h.subset_ground⟩, fun ⟨h, hX⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
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
⊢ M.Spanning X
have obtain : ∀ (I : Set α) (hI : M.IsBasis I X), M.Spanning 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 : Set α
inst : M.RankFinite
hX : X ⊆ M.E
⊢ M.Spanning X ↔ M.eRank ≤ M.eRk X
have rw : M.eRank ≤ M.eRk X ∧ X ⊆ M.E ↔ M.eRank ≤ M.eRk X
Tactic: rw [spanning_iff_eRk_le', and_iff_left hX]