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 I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ M.eRk X = 0 ↔ X ∩ M.E ⊆ M.loops
have rw : I = ∅ ↔ X ∩ M.E ⊆ M.loops
Tactic: rw [← eRk_inter_ground, ← hI.encard_eq_eRk, encard_eq_zero]
-- 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.E)
⊢ I = ∅ ↔ X ∩ M.E ⊆ M.loops
have refine : ∀ (h : X ∩ M.E ⊆ M.loops) (e : α) (heI : e ∈ I), False
Tactic: refine ⟨fun h ↦ by simpa [h] using hI, fun h ↦ eq_empty_iff_forall_notMem.2 fun e heI ↦ ?_⟩
-- 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 = 0 ↔ X ⊆ M.loops
have rw : X ∩ M.E ⊆ M.loops ↔ X ⊆ M.loops
Tactic: rw [eRk_eq_zero_iff', inter_eq_self_of_subset_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : X ∩ M.E ⊆ M.loops ↔ X ⊆ M.loops
⊢ M.eRk X = 0 ↔ X ⊆ M.loops
have rw₁ : X ⊆ M.loops ↔ X ⊆ M.loops
Tactic: rw [eRk_eq_zero_iff', inter_eq_self_of_subset_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
have obtain : ∀ (Ii : Set α) (hIi : M.IsBasis' Ii (X ∩ Y)), M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
Tactic: obtain ⟨Ii, hIi⟩ := M.exists_isBasis' (X ∩ Y)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
have obtain : ∀ (IX : Set α) (hIX : M.IsBasis' IX X) (hIX' : Ii ⊆ IX), M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
Tactic: obtain ⟨IX, hIX, hIX'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_left)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
have obtain : ∀ (IY : Set α) (hIY : M.IsBasis' IY Y) (hIY' : Ii ⊆ IY), M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
Tactic: obtain ⟨IY, hIY, hIY'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_right)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
have rw : M.eRk (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard
Tactic: rw [← hIX.eRk_eq_eRk_union, union_comm, ← hIY.eRk_eq_eRk_union, ← hIi.encard_eq_eRk,
    ← hIX.encard_eq_eRk, ← hIY.encard_eq_eRk, union_comm, ← encard_union_add_encard_inter, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (insert e (X ∩ Y)) + M.eRk (insert e (X ∪ Y)) ≤ M.eRk (insert e X) + M.eRk (insert e Y)
have rw : M.eRk (insert e X ∩ insert e Y) + M.eRk (insert e X ∪ insert e Y) ≤ M.eRk (insert e X) + M.eRk (insert e Y)
Tactic: rw [insert_inter_distrib, insert_union_distrib]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (M.E \ (X ∪ Y)) + M.eRk (M.E \ (X ∩ Y)) ≤ M.eRk (M.E \ X) + M.eRk (M.E \ Y)
have rw : M.eRk (M.E \ X ∩ (M.E \ Y)) + M.eRk (M.E \ X ∪ M.E \ Y) ≤ M.eRk (M.E \ X) + M.eRk (M.E \ Y)
Tactic: rw [← diff_inter_diff, diff_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (M.E \ insert e (X ∪ Y)) + M.eRk (M.E \ insert e (X ∩ Y)) ≤ M.eRk (M.E \ insert e X) + M.eRk (M.E \ insert e Y)
have rw : M.eRk (M.E \ (insert e X ∪ insert e Y)) + M.eRk (M.E \ (insert e X ∩ insert e Y)) ≤
  M.eRk (M.E \ insert e X) + M.eRk (M.E \ insert e Y)
Tactic: rw [insert_union_distrib, insert_inter_distrib]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
Y X : Set α
hY : M.eRk Y ≤ 0
⊢ M.eRk (X \ Y) = M.eRk X
have rw : M.eRk (X \ Y ∪ Y) = M.eRk X
Tactic: rw [← eRk_eq_eRk_union_eRk_le_zero (X \ Y) hY, diff_union_self, eRk_eq_eRk_union_eRk_le_zero _ hY]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
Y X : Set α
hY : M.eRk Y ≤ 0
rw : M.eRk (X \ Y ∪ Y) = M.eRk X
⊢ M.eRk (X \ Y) = M.eRk X
have rw₁ : M.eRk (X ∪ Y) = M.eRk X
Tactic: rw [← eRk_eq_eRk_union_eRk_le_zero (X \ Y) hY, diff_union_self, eRk_eq_eRk_union_eRk_le_zero _ hY]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
Y X : Set α
hY : M.eRk Y ≤ 0
rw : M.eRk (X \ Y ∪ Y) = M.eRk X
rw₁ : M.eRk (X ∪ Y) = M.eRk X
⊢ M.eRk (X \ Y) = M.eRk X
have rw₂ : M.eRk X = M.eRk X
Tactic: rw [← eRk_eq_eRk_union_eRk_le_zero (X \ Y) hY, diff_union_self, eRk_eq_eRk_union_eRk_le_zero _ hY]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk X ≤ M.eRk (X ∩ Y) + M.eRk (X \ Y)
have nth_rw : M.eRk (X ∩ Y ∪ X \ Y) ≤ M.eRk (X ∩ Y) + M.eRk (X \ Y)
Tactic: nth_rw 1 [← inter_union_diff X Y]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
X Y : Set α
M : Matroid α
h : Y ⊆ X
⊢ M.eRk X ≤ M.eRk Y + M.eRk (X \ Y)
have nth_rw : M.eRk (Y ∪ X \ Y) ≤ M.eRk Y + M.eRk (X \ Y)
Tactic: nth_rw 1 [← union_diff_cancel h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk X + M.eRk Y ≤ X.encard + M.eRk Y
have grw : X.encard + M.eRk Y ≤ X.encard + M.eRk Y
Tactic: grw [M.eRk_le_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk X + M.eRk Y ≤ M.eRk X + Y.encard
have grw : M.eRk X + M.eRk Y ≤ M.eRk X + M.eRk Y
Tactic: grw [← M.eRk_le_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRank ≤ M.eRk (X ∪ M.E \ X)
have rw : M.eRank ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)
Tactic: rw [← eRk_inter_ground, eRank_def, union_diff_self,
    union_inter_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRank ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)
⊢ M.eRank ≤ M.eRk (X ∪ M.E \ X)
have rw₁ : M.eRk M.E ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)
Tactic: rw [← eRk_inter_ground, eRank_def, union_diff_self,
    union_inter_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRank ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)
rw₁ : M.eRk M.E ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)
⊢ M.eRank ≤ M.eRk (X ∪ M.E \ X)
have rw₂ : M.eRk M.E ≤ M.eRk ((X ∪ M.E) ∩ M.E)
Tactic: rw [← eRk_inter_ground, eRank_def, union_diff_self,
    union_inter_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRank ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)
rw₁ : M.eRk M.E ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)
rw₂ : M.eRk M.E ≤ M.eRk ((X ∪ M.E) ∩ M.E)
⊢ M.eRank ≤ M.eRk (X ∪ M.E \ X)
have rw₃ : M.eRk M.E ≤ M.eRk M.E
Tactic: rw [← eRk_inter_ground, eRank_def, union_diff_self,
    union_inter_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.eRank ≠ ⊤ ↔ M.RankFinite
have obtain : ∀ (B : Set α) (hB : M.IsBase B), M.eRank ≠ ⊤ ↔ M.RankFinite
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.RankFinite
have rw : B.Finite ↔ M.RankFinite
Tactic: rw [← hB.encard_eq_eRank, encard_ne_top_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.eRank = ⊤ ↔ M.RankInfinite
have rw : M.eRank = ⊤ ↔ ¬M.RankFinite
Tactic: rw [← not_rankFinite_iff, ← eRank_ne_top_iff, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
rw : M.eRank = ⊤ ↔ ¬M.RankFinite
⊢ M.eRank = ⊤ ↔ M.RankInfinite
have rw₁ : M.eRank = ⊤ ↔ ¬M.eRank ≠ ⊤
Tactic: rw [← not_rankFinite_iff, ← eRank_ne_top_iff, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
rw : M.eRank = ⊤ ↔ ¬M.RankFinite
rw₁ : M.eRank = ⊤ ↔ ¬M.eRank ≠ ⊤
⊢ M.eRank = ⊤ ↔ M.RankInfinite
have rw₂ : M.eRank = ⊤ ↔ M.eRank = ⊤
Tactic: rw [← not_rankFinite_iff, ← eRank_ne_top_iff, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X = ⊤ ↔ ¬M.IsRkFinite X
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk X = ⊤ ↔ ¬M.IsRkFinite 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.IsRkFinite X
have rw : I.encard = ⊤ ↔ ¬M.IsRkFinite X
Tactic: rw [hI.eRk_eq_encard, encard_eq_top_iff, ← hI.finite_iff_isRkFinite, Set.Infinite]
-- 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 : I.encard = ⊤ ↔ ¬M.IsRkFinite X
⊢ M.eRk X = ⊤ ↔ ¬M.IsRkFinite X
have rw₁ : I.Infinite ↔ ¬M.IsRkFinite X
Tactic: rw [hI.eRk_eq_encard, encard_eq_top_iff, ← hI.finite_iff_isRkFinite, Set.Infinite]
-- 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 : I.encard = ⊤ ↔ ¬M.IsRkFinite X
rw₁ : I.Infinite ↔ ¬M.IsRkFinite X
⊢ M.eRk X = ⊤ ↔ ¬M.IsRkFinite X
have rw₂ : I.Infinite ↔ ¬I.Finite
Tactic: rw [hI.eRk_eq_encard, encard_eq_top_iff, ← hI.finite_iff_isRkFinite, Set.Infinite]
-- 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 : I.encard = ⊤ ↔ ¬M.IsRkFinite X
rw₁ : I.Infinite ↔ ¬M.IsRkFinite X
rw₂ : I.Infinite ↔ ¬I.Finite
⊢ M.eRk X = ⊤ ↔ ¬M.IsRkFinite X
have rw₃ : ¬I.Finite ↔ ¬I.Finite
Tactic: rw [hI.eRk_eq_encard, encard_eq_top_iff, ← hI.finite_iff_isRkFinite, Set.Infinite]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X < ⊤ ↔ M.IsRkFinite X
have rw : M.eRk X ≠ ⊤ ↔ M.IsRkFinite X
Tactic: rw [lt_top_iff_ne_top, eRk_ne_top_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRk X ≠ ⊤ ↔ M.IsRkFinite X
⊢ M.eRk X < ⊤ ↔ M.IsRkFinite X
have rw₁ : M.IsRkFinite X ↔ M.IsRkFinite X
Tactic: rw [lt_top_iff_ne_top, eRk_ne_top_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure I
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
⊢ M.IsBasis I X
have obtain : ∀ (J : Set α) (hJ : M.IsBasis J (I ∩ M.E)), M.IsBasis I X
Tactic: obtain ⟨J, hJ⟩ := M.exists_isBasis (I ∩ M.E)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure I
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
⊢ M.IsBasis I X
have hIJ : J ⊆ I
Tactic: have hIJ := hJ.subset.trans inter_subset_left
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure I
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.IsBasis I X
have rw : ∀ (hXI : X ⊆ M.closure (I ∩ M.E)) (hIX : I ⊆ X) (hI : I.encard ≤ M.eRk X) (J : Set α) (hJ : M.IsBasis J (I ∩ M.E))
  (hIJ : J ⊆ I), M.IsBasis I X
Tactic: rw [← closure_inter_ground] at hXI
Cleared hypotheses: hXI, hIX, hI, J, hJ, hIJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure (I ∩ M.E)
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.IsBasis I X
have hXI₁ : X ⊆ M.closure J
Tactic: replace hXI := hXI.trans <| M.closure_subset_closure_of_subset_closure hJ.subset_closure
Cleared hypotheses: hXI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
⊢ M.IsBasis I X
have hJX : M.IsBasis J X
Tactic: have hJX := hJ.indep.isBasis_of_subset_of_subset_closure (hIJ.trans hIX) hXI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
⊢ M.IsBasis I X
have hI₁ : I.encard ≤ J.encard
Tactic: rw [← hJX.encard_eq_eRk] at hI
Cleared hypotheses: hI, hJ, hIJ, hXI, hJX
-- 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
hr : M.eRk Y ≤ M.eRk X
⊢ M.closure X = M.closure Y
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.closure X = M.closure 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 α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hr : M.eRk Y ≤ M.eRk X
I : Set α
hI : M.IsBasis' I X
⊢ M.closure X = M.closure Y
have obtain : ∀ (J : Set α) (hJ : M.IsBasis' J Y) (hIJ : I ⊆ J), M.closure X = M.closure 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 α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hr : M.eRk Y ≤ M.eRk X
I : Set α
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure X = M.closure Y
have rw : ∀ (hI : M.IsBasis' I X) (J : Set α) (hr : J.encard ≤ I.encard) (hJ : M.IsBasis' J Y) (hIJ : I ⊆ J),
  M.closure X = M.closure Y
Tactic: rw [hI.eRk_eq_encard, hJ.eRk_eq_encard] at hr
Cleared hypotheses: hr, hI, J, hJ, hIJ
-- 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
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure X = M.closure Y
have rw : M.closure (X ∩ M.E) = M.closure Y
Tactic: rw [← closure_inter_ground, ← M.closure_inter_ground Y,
    ← hI.isBasis_inter_ground.closure_eq_closure,
    ← hJ.isBasis_inter_ground.closure_eq_closure, Finite.eq_of_subset_of_encard_le
      (hI.indep.finite_of_subset_isRkFinite hI.subset hX) hIJ hr]
-- 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
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
rw : M.closure (X ∩ M.E) = M.closure Y
⊢ M.closure X = M.closure Y
have rw₁ : M.closure (X ∩ M.E) = M.closure (Y ∩ M.E)
Tactic: rw [← closure_inter_ground, ← M.closure_inter_ground Y,
    ← hI.isBasis_inter_ground.closure_eq_closure,
    ← hJ.isBasis_inter_ground.closure_eq_closure, Finite.eq_of_subset_of_encard_le
      (hI.indep.finite_of_subset_isRkFinite hI.subset hX) hIJ hr]
-- 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
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
rw : M.closure (X ∩ M.E) = M.closure Y
rw₁ : M.closure (X ∩ M.E) = M.closure (Y ∩ M.E)
⊢ M.closure X = M.closure Y
have rw₂ : M.closure I = M.closure (Y ∩ M.E)
Tactic: rw [← closure_inter_ground, ← M.closure_inter_ground Y,
    ← hI.isBasis_inter_ground.closure_eq_closure,
    ← hJ.isBasis_inter_ground.closure_eq_closure, Finite.eq_of_subset_of_encard_le
      (hI.indep.finite_of_subset_isRkFinite hI.subset hX) hIJ hr]
-- 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
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
rw : M.closure (X ∩ M.E) = M.closure Y
rw₁ : M.closure (X ∩ M.E) = M.closure (Y ∩ M.E)
rw₂ : M.closure I = M.closure (Y ∩ M.E)
⊢ M.closure X = M.closure Y
have rw₃ : M.closure I = M.closure J
Tactic: rw [← closure_inter_ground, ← M.closure_inter_ground Y,
    ← hI.isBasis_inter_ground.closure_eq_closure,
    ← hJ.isBasis_inter_ground.closure_eq_closure, Finite.eq_of_subset_of_encard_le
      (hI.indep.finite_of_subset_isRkFinite hI.subset hX) hIJ hr]
-- 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
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
rw : M.closure (X ∩ M.E) = M.closure Y
rw₁ : M.closure (X ∩ M.E) = M.closure (Y ∩ M.E)
rw₂ : M.closure I = M.closure (Y ∩ M.E)
rw₃ : M.closure I = M.closure J
⊢ M.closure X = M.closure Y
have rw₄ : M.closure J = M.closure J
Tactic: rw [← closure_inter_ground, ← M.closure_inter_ground Y,
    ← hI.isBasis_inter_ground.closure_eq_closure,
    ← hJ.isBasis_inter_ground.closure_eq_closure, Finite.eq_of_subset_of_encard_le
      (hI.indep.finite_of_subset_isRkFinite hI.subset hX) hIJ hr]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk X + M.eRk {e} ≤ M.eRk X + 1
have bc : M.eRk {e} ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∈ M.E \ M.closure X
⊢ M.eRk (insert e X) = M.eRk X + 1
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk (insert e X) = M.eRk X + 1
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 α
e : α
he : e ∈ M.E \ M.closure X
I : Set α
hI : M.IsBasis' I X
⊢ M.eRk (insert e X) = M.eRk X + 1
have he₁ : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
Tactic: rw [← hI.closure_eq_closure, mem_diff, hI.indep.mem_closure_iff', not_and] at he
Cleared hypotheses: he, hI
-- 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
⊢ M.Indep (insert e I)
have tauto : e ∈ M.E → (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I)) → M.Indep (insert e I)
Tactic: tauto
Cleared hypotheses: he
-- 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
tauto tauto₁ tauto₂ : e ∈ M.E → (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I)) → M.Indep (insert e I)
⊢ M.Indep (insert e I)
have inl : e ∈ M.E → e ∉ M.E → M.Indep (insert e I)
Tactic: tauto
Cleared hypotheses: he
-- 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
tauto tauto₁ tauto₂ : e ∈ M.E → (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I)) → M.Indep (insert e I)
inl : e ∈ M.E → e ∉ M.E → M.Indep (insert e I)
⊢ M.Indep (insert e I)
have inr : e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I) → M.Indep (insert e I)
Tactic: tauto
Cleared hypotheses: he
-- 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
tauto tauto₁ tauto₂ : e ∈ M.E → (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I)) → M.Indep (insert e I)
inl : e ∈ M.E → e ∉ M.E → M.Indep (insert e I)
inr inr₁ inr₂ : e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I) → M.Indep (insert e I)
⊢ M.Indep (insert e I)
have inr₃ : e ∈ M.E → M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
Tactic: tauto
Cleared hypotheses: he
-- 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
⊢ e ∉ I
have tauto : e ∈ I → e ∈ M.E → (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I)) → False
Tactic: tauto
Cleared hypotheses: he
-- 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
tauto tauto₁ tauto₂ : e ∈ I → e ∈ M.E → (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I)) → False
⊢ e ∉ I
have inl : e ∈ I → e ∈ M.E → e ∉ M.E → False
Tactic: tauto
Cleared hypotheses: he
-- 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
tauto tauto₁ tauto₂ : e ∈ I → e ∈ M.E → (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I)) → False
inl : e ∈ I → e ∈ M.E → e ∉ M.E → False
⊢ e ∉ I
have inr : e ∈ I → e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I) → False
Tactic: tauto
Cleared hypotheses: he
-- 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
tauto tauto₁ tauto₂ : e ∈ I → e ∈ M.E → (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I)) → False
inl : e ∈ I → e ∈ M.E → e ∉ M.E → False
inr inr₁ inr₂ : e ∈ I → e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I) → False
⊢ e ∉ I
have inr₃ : e ∈ I → e ∈ M.E → M.Indep (insert e I) → e ∉ I → False
Tactic: tauto
Cleared hypotheses: he
-- 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
⊢ M.eRk (insert e X) = M.eRk X + 1
have rw : M.eRk (M.closure (insert e X)) = M.eRk X + 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
⊢ M.eRk (insert e X) = M.eRk X + 1
have rw₁ : M.eRk (M.closure (insert e I)) = M.eRk X + 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
⊢ M.eRk (insert e X) = M.eRk X + 1
have rw₂ : M.eRk (M.closure (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)]