awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : M.Indep I
hNM : N ≤r M
hIN : I ⊆ N.E
⊢ N.Indep I
have obtain : ∀ (R : Set α) (hIN : I ⊆ (M ↾ R).E), (M ↾ R).Indep I
Tactic: obtain ⟨R, -, rfl⟩ := hNM
Cleared hypotheses: N, hNM, hIN
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : M.IsBasis I X
hNM : N ≤r M
hX : X ⊆ N.E
⊢ N.IsBasis I X
have obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hX : X ⊆ (M ↾ R).E), (M ↾ R).IsBasis I X
Tactic: obtain ⟨R, hR, rfl⟩ := hNM
Cleared hypotheses: N, hNM, hX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
R : Set α
hR : R ⊆ M.E
hX : X ⊆ (M ↾ R).E
⊢ (M ↾ R).IsBasis I X
have rwa : M.IsBasis I X ∧ X ⊆ R
Tactic: rwa [isBasis_restrict_iff, and_iff_left (show X ⊆ R from hX)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : N.IsBasis I X
hNM : N ≤r M
⊢ M.IsBasis I X
have obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hI : (M ↾ R).IsBasis I X), M.IsBasis I X
Tactic: obtain ⟨R, hR, rfl⟩ := hNM
Cleared hypotheses: N, hI, hNM
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : N.IsBase I
hNM : N ≤r M
⊢ M.IsBasis I N.E
have obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hI : (M ↾ R).IsBase I), M.IsBasis I (M ↾ R).E
Tactic: obtain ⟨R, hR, rfl⟩ := hNM
Cleared hypotheses: N, hI, hNM
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBase I
⊢ M.IsBasis I (M ↾ R).E
have rwa : ∀ (hI : M.IsBasis I R), M.IsBasis I (M ↾ R).E
Tactic: rwa [isBase_restrict_iff] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
N : Matroid α
hX : N.Dep X
hNM : N ≤r M
⊢ M.Dep X
have obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hX : (M ↾ R).Dep X), M.Dep X
Tactic: obtain ⟨R, hR, rfl⟩ := hNM
Cleared hypotheses: N, hX, hNM
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
X R : Set α
hR : R ⊆ M.E
hX : (M ↾ R).Dep X
⊢ M.Dep X
have hX₁ : ¬M.Indep X ∧ X ⊆ R
Tactic: rw [restrict_dep_iff] at hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
N : Matroid α
hX : M.Dep X
hNM : N ≤r M
hXE : X ⊆ N.E
⊢ N.Dep X
have obtain : ∀ (R : Set α) (hXE : X ⊆ (M ↾ R).E), (M ↾ R).Dep X
Tactic: obtain ⟨R, -, rfl⟩ := hNM
Cleared hypotheses: N, hNM, hXE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : M.IsBasis J Y
⊢ M.IsBasis I Y
have rw : (M ↾ Y).IsBase I
Tactic: rw [← isBase_restrict_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : M.IsBasis J Y
⊢ (M ↾ Y).IsBase I
have hJY₁ : (M ↾ Y).IsBase J
Tactic: rw [← isBase_restrict_iff] at hJY
Cleared hypotheses: hJY
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
⊢ M.IsBasis I Y
have hI' : M.IsBasis I (X ∩ Y)
Tactic: have hI' := hI.isBasis_subset (subset_inter hI.subset hIY) inter_subset_left
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
hI' : M.IsBasis I (X ∩ Y)
⊢ M.IsBasis I Y
have hJ' : M.IsBasis J (X ∩ Y)
Tactic: have hJ' := hJ.isBasis_subset (subset_inter hJX hJ.subset) inter_subset_right
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
⊢ ∃ (I' : Set α), M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
have obtain : ∀ (I' : Set α) (hI' : (M ↾ X).IsBase I') (hII' : I ⊆ I') (hI'IJ : I' ⊆ I ∪ J),
  ∃ (I' : Set α), M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
Tactic: obtain ⟨I', hI', hII', hI'IJ⟩ :=
    (hI.indep_restrict_of_subset hIX).exists_isBase_subset_union_isBase (IsBasis.isBase_restrict hJ)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
I' : Set α
hI' : (M ↾ X).IsBase I'
hII' : I ⊆ I'
hI'IJ : I' ⊆ I ∪ J
⊢ ∃ (I' : Set α), M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
have hI'₁ : M.IsBasis I' X
Tactic: rw [isBase_restrict_iff] at hI'
Cleared hypotheses: hI', hII', hI'IJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬M.IsBasis I X
hJ : M.IsBasis J X
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
have hI'₁ : ¬(M ↾ X).IsBase I
Tactic: rw [← isBase_restrict_iff] at hI'
Cleared hypotheses: hI', hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : M.IsBasis J X
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
have hJ₁ : (M ↾ X).IsBase J
Tactic: rw [← isBase_restrict_iff] at hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
have obtain : ∀ (e : α) (he : e ∈ J \ I) (hi : (M ↾ X).Indep (insert e I)), ∃ e ∈ J \ I, M.Indep (insert e I)
Tactic: obtain ⟨e, he, hi⟩ := (hI.indep_restrict_of_subset hIX).exists_insert_of_not_isBase hI' hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
⊢ ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X
have obtain : ∀ (y : α) (hy : y ∈ J \ I) (h : (M ↾ X).IsBase (insert y (I \ {e}))), ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X
Tactic: obtain ⟨y, hy, h⟩ := hIX.restrict_isBase.exchange hJX.restrict_isBase he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
y : α
hy : y ∈ J \ I
h : (M ↾ X).IsBase (insert y (I \ {e}))
⊢ M.IsBasis (insert y (I \ {e})) X
have rwa : ∀ (h : M.IsBasis (insert y (I \ {e})) X), M.IsBasis (insert y (I \ {e})) X
Tactic: rwa [isBase_restrict_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hI : M.IsBasis I X
hJ : M.IsBasis J X
hIJ : I \ J = {e}
⊢ ∃ f ∈ J \ I, J = insert f I \ {e}
have hI₁ : (M ↾ X).IsBase I
Tactic: rw [← isBase_restrict_iff] at hI hJ
Cleared hypotheses: hI, hJ, hIJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hI : M.IsBasis I X
hJ : M.IsBasis J X
hIJ : I \ J = {e}
hI₁ : (M ↾ X).IsBase I
⊢ ∃ f ∈ J \ I, J = insert f I \ {e}
have hJ₁ : (M ↾ X).IsBase J
Tactic: rw [← isBase_restrict_iff] at hI hJ
Cleared hypotheses: hI, hJ, hIJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.IsBasis' I X
hJ : M.IsBasis' J X
⊢ I.encard = J.encard
have hI₁ : (M ↾ X).IsBase I
Tactic: rw [← isBase_restrict_iff'] at hI hJ
Cleared hypotheses: hI, hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.IsBasis' I X
hJ : M.IsBasis' J X
hI₁ : (M ↾ X).IsBase I
⊢ I.encard = J.encard
have hJ₁ : (M ↾ X).IsBase J
Tactic: rw [← isBase_restrict_iff'] at hI hJ
Cleared hypotheses: hI, hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
have by_contra! : ∀ (he : ∀ (e : α) (_ : e ∈ J \ I), ¬M.Indep (insert e I)), False
Tactic: by_contra! he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ (e : α) (_ : e ∈ J \ I), ¬M.Indep (insert e I)
⊢ M.IsBasis I (I ∪ J)
have simp_rw : ∀ e ∈ J, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
Tactic: simp_rw [hI.isBasis_iff_forall_insert_dep subset_union_left, union_diff_left, mem_diff,
      and_imp, dep_iff, insert_subset_iff, and_iff_left hI.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ (e : α) (_ : e ∈ J \ I), ¬M.Indep (insert e I)
⊢ False
have hb : M.IsBasis I (I ∪ J)
Tactic: have hb : M.IsBasis I (I ∪ J) := by
    simp_rw [hI.isBasis_iff_forall_insert_dep subset_union_left, union_diff_left, mem_diff,
      and_imp, dep_iff, insert_subset_iff, and_iff_left hI.subset_ground]
    exact fun e heJ heI ↦ ⟨he e ⟨heJ, heI⟩, hJ.subset_ground heJ⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ (e : α) (_ : e ∈ J \ I), ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
⊢ False
have obtain : ∀ (J' : Set α) (hJ' : M.IsBasis J' (I ∪ J)) (hJJ' : J ⊆ J'), False
Tactic: obtain ⟨J', hJ', hJJ'⟩ := hJ.subset_isBasis_of_subset I.subset_union_right
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ (e : α) (_ : e ∈ J \ I), ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
J' : Set α
hJ' : M.IsBasis J' (I ∪ J)
hJJ' : J ⊆ J'
⊢ False
have hIJ₁ : J'.encard < J.encard
Tactic: rw [← hJ'.encard_eq_encard hb] at hIJ
Cleared hypotheses: hIJ, hJ', hJJ'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep (↑I : Set α)
hJ : M.Indep (↑J : Set α)
hIJ : I.card < J.card
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e (↑I : Set α))
have obtain : ∀ (x : α) (hx : x ∈ (↑J : Set α) \ (↑I : Set α)) (hxI : M.Indep (insert x (↑I : Set α))),
  ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e (↑I : Set α))
Tactic: obtain ⟨x, hx, hxI⟩ := hI.augment hJ (by simpa [encard_eq_coe_toFinset_card])
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep (↑I : Set α)
hJ : M.Indep (↑J : Set α)
hIJ : I.card < J.card
x : α
hx : x ∈ (↑J : Set α) \ (↑I : Set α)
hxI : M.Indep (insert x (↑I : Set α))
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e (↑I : Set α))
have hx₁ : x ∈ J ∧ x ∉ I
Tactic: simp only [mem_diff, Finset.mem_coe] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
⊢ M.cRk X ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #(↑I : Type u) ≤ κ
have simp_rw : (M ↾ X).cRank ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #(↑I : Type u) ≤ κ
Tactic: simp_rw [cRk, cRank_le_iff, isBase_restrict_iff']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
simp_rw : (M ↾ X).cRank ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #(↑I : Type u) ≤ κ
⊢ M.cRk X ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #(↑I : Type u) ≤ κ
have simp_rw₁ : (∀ ⦃B : Set α⦄, (M ↾ X).IsBase B → #(↑B : Type u) ≤ κ) ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #(↑I : Type u) ≤ κ
Tactic: simp_rw [cRk, cRank_le_iff, isBase_restrict_iff']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
⊢ M.cRk M.E = M.cRank
have rw : (M ↾ M.E).cRank = M.cRank
Tactic: rw [cRk, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
rw : (M ↾ M.E).cRank = M.cRank
⊢ M.cRk M.E = M.cRank
have rw₁ : M.cRank = M.cRank
Tactic: rw [cRk, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
⊢ Monotone M.cRk
have simp : ∀ ⦃a b : Set α⦄, a ⊆ b → ∀ ⦃I : Set α⦄, M.IsBasis' I a → #(↑I : Type u) ≤ M.cRk b
Tactic: simp only [Monotone, le_eq_subset, cRk_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
⊢ #(↑I : Type u) ≤ M.cRk Y
have obtain : ∀ (J : Set α) (hJ : M.IsBasis' J Y) (hIJ : I ⊆ J), #(↑I : Type u) ≤ M.cRk Y
Tactic: obtain ⟨J, hJ, hIJ⟩ := hIX.indep.subset_isBasis'_of_subset (hIX.subset.trans hXY)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
have simp_rw : ∀ ⦃I : Set α⦄, M.IsBasis' I Y → I ⊆ X
Tactic: simp_rw [isBasis'_restrict_iff, inter_eq_self_of_subset_left hYX, iff_self_and]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
Goal:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ (M ↾ X).cRk Y = M.cRk Y
have aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
Tactic: have aux : ∀ ⦃I⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y := by
    simp_rw [isBasis'_restrict_iff, inter_eq_self_of_subset_left hYX, iff_self_and]
    exact fun I h ↦ h.subset.trans hYX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (M ↾ X).cRk Y = M.cRk Y
have simp_rw : (∀ ⦃I : Set α⦄, (M ↾ X).IsBasis' I Y → #(↑I : Type u) ≤ M.cRk Y) ∧
  ∀ ⦃I : Set α⦄, M.IsBasis' I Y → #(↑I : Type u) ≤ (M ↾ X).cRk Y
Tactic: simp_rw [le_antisymm_iff, cRk_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X Y : Set α
⊢ (M ↾ X).cRk Y = M.cRk (X ∩ Y)
have rw : (M ↾ X).cRk (Y ∩ (M ↾ X).E) = M.cRk (X ∩ Y)
Tactic: rw [← cRk_inter_ground, restrict_ground_eq, cRk_restrict_subset _ inter_subset_right,
    inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X Y : Set α
rw : (M ↾ X).cRk (Y ∩ (M ↾ X).E) = M.cRk (X ∩ Y)
⊢ (M ↾ X).cRk Y = M.cRk (X ∩ Y)
have rw₁ : (M ↾ X).cRk (Y ∩ X) = M.cRk (X ∩ Y)
Tactic: rw [← cRk_inter_ground, restrict_ground_eq, cRk_restrict_subset _ inter_subset_right,
    inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X Y : Set α
rw : (M ↾ X).cRk (Y ∩ (M ↾ X).E) = M.cRk (X ∩ Y)
rw₁ : (M ↾ X).cRk (Y ∩ X) = M.cRk (X ∩ Y)
⊢ (M ↾ X).cRk Y = M.cRk (X ∩ Y)
have rw₂ : M.cRk (Y ∩ X) = M.cRk (X ∩ Y)
Tactic: rw [← cRk_inter_ground, restrict_ground_eq, cRk_restrict_subset _ inter_subset_right,
    inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X Y : Set α
rw : (M ↾ X).cRk (Y ∩ (M ↾ X).E) = M.cRk (X ∩ Y)
rw₁ : (M ↾ X).cRk (Y ∩ X) = M.cRk (X ∩ Y)
rw₂ : M.cRk (Y ∩ X) = M.cRk (X ∩ Y)
⊢ (M ↾ X).cRk Y = M.cRk (X ∩ Y)
have rw₃ : M.cRk (X ∩ Y) = M.cRk (X ∩ Y)
Tactic: rw [← cRk_inter_ground, restrict_ground_eq, cRk_restrict_subset _ inter_subset_right,
    inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ lift.{u, v} ((M.map f hf).cRk (f '' X)) = lift.{v, u} (M.cRk X)
have nth_rw : ⨆ (i : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), lift.{u, v} #(↑(↑i : Set β) : Type v) ≤
    lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)) ∧
  lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)) ≤
    lift.{u, v} (⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))
Tactic: nth_rw 1 [cRk, cRank, le_antisymm_iff, lift_iSup bddAbove_of_small, cRk, cRank, cRk, cRank]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ ⨆ (i : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), lift.{u, v} #(↑(↑i : Set β) : Type v) ≤
      lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)) ∧
    lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)) ≤
      lift.{u, v} (⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))
have nth_rw : ⨆ (i : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), lift.{u, v} #(↑(↑i : Set β) : Type v) ≤
    lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)) ∧
  ⨆ (i : { B : Set α // (M ↾ X).IsBase B }), lift.{v, u} #(↑(↑i : Set α) : Type u) ≤
    lift.{u, v} (⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))
Tactic: nth_rw 2 [lift_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ ⨆ (i : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), lift.{u, v} #(↑(↑i : Set β) : Type v) ≤
      lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)) ∧
    ⨆ (i : { B : Set α // (M ↾ X).IsBase B }), lift.{v, u} #(↑(↑i : Set α) : Type u) ≤
      lift.{u, v} (⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))
have simp : (∀ (a : Set β) (b : (M.map f hf).IsBasis a (f '' X)),
    lift.{u, v} #(↑a : Type v) ≤ lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))) ∧
  ∀ (a : Set α) (b : M.IsBasis a X),
    lift.{v, u} #(↑a : Type u) ≤
      lift.{u, v} (⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))
Tactic: simp only [ciSup_le_iff bddAbove_of_small, Subtype.forall, isBase_restrict_iff',
    isBasis'_iff_isBasis hX, isBasis'_iff_isBasis (show f '' X ⊆ (M.map f hf).E from image_mono hX)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ (∀ (a : Set β) (b : (M.map f hf).IsBasis a (f '' X)),
      lift.{u, v} #(↑a : Type v) ≤ lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))) ∧
    ∀ (a : Set α) (b : M.IsBasis a X),
      lift.{v, u} #(↑a : Type u) ≤
        lift.{u, v} (⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))
have refine_1 : ∀ (I : Set β) (hI : (M.map f hf).IsBasis I (f '' X)),
  lift.{u, v} #(↑I : Type v) ≤ lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
Tactic: refine ⟨fun I hI ↦ ?_, fun I hI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
refine_1 :
  ∀ (I : Set β) (hI : (M.map f hf).IsBasis I (f '' X)),
    lift.{u, v} #(↑I : Type v) ≤ lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
⊢ (∀ (a : Set β) (b : (M.map f hf).IsBasis a (f '' X)),
      lift.{u, v} #(↑a : Type v) ≤ lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))) ∧
    ∀ (a : Set α) (b : M.IsBasis a X),
      lift.{v, u} #(↑a : Type u) ≤
        lift.{u, v} (⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))
have refine_2 : ∀ (I : Set α) (hI : M.IsBasis I X),
  lift.{v, u} #(↑I : Type u) ≤
    lift.{u, v} (⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))
Tactic: refine ⟨fun I hI ↦ ?_, fun I hI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set β
hI : (M.map f hf).IsBasis I (f '' X)
⊢ lift.{u, v} #(↑I : Type v) ≤ lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
have refine_1 : ∀ (I X' : Set α) (hIX : M.IsBasis I X') (hXX' : f '' X = f '' X') (hI : (M.map f hf).IsBasis (f '' I) (f '' X)),
  lift.{u, v} #(↑(f '' I) : Type v) ≤ lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
Tactic: obtain ⟨I, X', hIX, rfl, hXX'⟩ := map_isBasis_iff'.1 hI
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ lift.{u, v} #(↑(f '' I) : Type v) ≤ lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
have refine_1 : #(↑I : Type u) ≤ ⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)
Tactic: rw [mk_image_eq_of_injOn_lift _ _ (hf.mono hIX.indep.subset_ground), lift_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ X = X'
have rwa : ∀ (hXX' : X = X') (hI : (M.map f hf).IsBasis (f '' I) (f '' X)), X = X'
Tactic: rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'
Cleared hypotheses: hXX', hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ #(↑I : Type u) ≤ ⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)
have hIX₁ : M.IsBasis I X
Tactic: obtain rfl : X = X' := by rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'
Cleared hypotheses: X', hIX, hXX'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
hIX₁ : M.IsBasis I X
⊢ #(↑I : Type u) ≤ ⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)
have hXX'₁ : f '' X = f '' X
Tactic: obtain rfl : X = X' := by rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'
Cleared hypotheses: X', hIX, hXX'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ lift.{v, u} #(↑I : Type u) ≤
    lift.{u, v} (⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))
have refine_2 : #(↑(f '' I) : Type v) ≤ ⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)
Tactic: rw [← mk_image_eq_of_injOn_lift _ _ (hf.mono hI.indep.subset_ground), lift_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α β : Type u
f : α → β
X : Set β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf).cRk X = M.cRk (f ⁻¹' X)
have rw : (M.map f hf).cRk X = M.cRk (f ⁻¹' X ∩ M.E)
Tactic: rw [← M.cRk_inter_ground, ← M.cRk_map_image hf _, image_preimage_inter, ← map_ground _ _ hf,
    cRk_inter_ground]