awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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}))
⊢ ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X

Tactic:
exact ⟨y, hy, by rwa [isBase_restrict_iff] at h⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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}
⊢ (M ↾ X).IsBase I

Tactic:
rw [← isBase_restrict_iff] at hI hJ

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
⊢ (M ↾ X).IsBase J

Tactic:
rw [← isBase_restrict_iff] at hI hJ

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
hJ₁ : (M ↾ X).IsBase J
⊢ I \ J = {e}

Tactic:
rw [← isBase_restrict_iff] at hI hJ

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
hIJ : I \ J = {e}
⊢ ∃ f ∈ J \ I, J = insert f I \ {e}

Tactic:
hI.eq_exchange_of_diff_eq_singleton hJ hIJ

Premises used: Matroid.IsBase.eq_exchange_of_diff_eq_singleton
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
hIJ : I \ J = {e}
⊢ ∃ f ∈ J \ I, J = insert f I \ {e}

Tactic:
exact hI.eq_exchange_of_diff_eq_singleton hJ hIJ

Premises used: Matroid.IsBase.eq_exchange_of_diff_eq_singleton
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.IsBasis' I X
hJ : M.IsBasis' J X
⊢ (M ↾ X).IsBase I

Tactic:
rw [← isBase_restrict_iff'] at hI hJ

Premises used: Matroid.isBase_restrict_iff'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
⊢ (M ↾ X).IsBase J

Tactic:
rw [← isBase_restrict_iff'] at hI hJ

Premises used: Matroid.isBase_restrict_iff'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
⊢ I.encard = J.encard

Tactic:
hI.encard_eq_encard_of_isBase hJ

Premises used: Matroid.IsBase.encard_eq_encard_of_isBase
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
⊢ I.encard = J.encard

Tactic:
exact hI.encard_eq_encard_of_isBase hJ

Premises used: Matroid.IsBase.encard_eq_encard_of_isBase
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J X
⊢ I.encard = J.encard

Tactic:
hI.isBasis'.encard_eq_encard hJ.isBasis'

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.encard_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
by_contra! : ∀ (he : ∀ (e : α) (_ : e ∈ J \ I), ¬M.Indep (insert e I)), False
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
by_contra! he
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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)
simp_rw : ∀ e ∈ J, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
⊢ M.IsBasis I (I ∪ J)

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]

Premises used: Set.union_diff_left, and_imp, and_iff_left, Set.subset_union_left, Set.insert_subset_iff, Matroid.Indep.subset_ground, Set.mem_diff, Matroid.Indep.isBasis_iff_forall_insert_dep, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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)
⊢ ∀ e ∈ J, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E

Tactic:
fun e heJ heI ↦ ⟨he e ⟨heJ, heI⟩, hJ.subset_ground heJ⟩

Premises used: Matroid.Indep.subset_ground, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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)
⊢ ∀ e ∈ J, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E

Tactic:
exact fun e heJ heI ↦ ⟨he e ⟨heJ, heI⟩, hJ.subset_ground heJ⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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)

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⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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)
obtain : ∀ (J' : Set α) (hJ' : M.IsBasis J' (I ∪ J)) (hJJ' : J ⊆ J'), False
⊢ False

Tactic:
obtain ⟨J', hJ', hJJ'⟩ := hJ.subset_isBasis_of_subset I.subset_union_right

Premises used: Set.subset_union_right, Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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'
⊢ J'.encard < J.encard

Tactic:
rw [← hJ'.encard_eq_encard hb] at hIJ

Premises used: Matroid.IsBasis.encard_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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'
hIJ₁ : J'.encard < J.encard
⊢ M.IsBasis J' (I ∪ J)

Tactic:
rw [← hJ'.encard_eq_encard hb] at hIJ

Premises used: Matroid.IsBasis.encard_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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'
hIJ₁ : J'.encard < J.encard
hJ'₁ : M.IsBasis J' (I ∪ J)
⊢ J ⊆ J'

Tactic:
rw [← hJ'.encard_eq_encard hb] at hIJ

Premises used: Matroid.IsBasis.encard_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
he : ∀ (e : α) (_ : e ∈ J \ I), ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
J' : Set α
hIJ : J'.encard < J.encard
hJ' : M.IsBasis J' (I ∪ J)
hJJ' : J ⊆ J'
⊢ False

Tactic:
hIJ.not_ge (encard_mono hJJ')

Premises used: Set.encard_mono, LT.lt.not_ge
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
he : ∀ (e : α) (_ : e ∈ J \ I), ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
J' : Set α
hIJ : J'.encard < J.encard
hJ' : M.IsBasis J' (I ∪ J)
hJJ' : J ⊆ J'
⊢ False

Tactic:
exact hIJ.not_ge (encard_mono hJJ')

Premises used: Set.encard_mono, LT.lt.not_ge
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep (↑I : Set α)
hJ : M.Indep (↑J : Set α)
hIJ : I.card < J.card
⊢ (↑I : Set α).encard < (↑J : Set α).encard

Tactic:
simpa [encard_eq_coe_toFinset_card]

Premises used: Set.encard_eq_coe_toFinset_card
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep (↑I : Set α)
hJ : M.Indep (↑J : Set α)
hIJ : I.card < J.card
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 α))
⊢ ∃ 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])

Premises used: Matroid.Indep.augment
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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 α))
⊢ x ∈ J ∧ x ∉ I

Tactic:
simp only [mem_diff, Finset.mem_coe] at hx

Premises used: Set.mem_diff, Finset.mem_coe
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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 : α
hxI : M.Indep (insert x (↑I : Set α))
hx : x ∈ J ∧ x ∉ I
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e (↑I : Set α))

Tactic:
⟨x, hx.1, hx.2, hxI⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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 : α
hxI : M.Indep (insert x (↑I : Set α))
hx : x ∈ J ∧ x ∉ I
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e (↑I : Set α))

Tactic:
exact ⟨x, hx.1, hx.2, hxI⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ #(↑B : Type u) ≤ M.cRank

Tactic:
le_ciSup (f := fun B : {B // M.IsBase B} ↦ #B.1) bddAbove_of_small ⟨B, hB⟩

Premises used: Matroid.cRank, Subtype.mk, le_ciSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I : Set α
ind : M.Indep I
⊢ #(↑I : Type u) ≤ M.cRank

Tactic:
have ⟨B, isBase, hIB⟩ := ind.exists_isBase_superset
  le_ciSup_of_le bddAbove_of_small ⟨B, isBase⟩ (mk_le_mk_of_subset hIB)

Premises used: le_ciSup_of_le, Cardinal.mk, Set.Elem, LE.le, Matroid.cRank, Subtype.mk, Matroid.Indep.exists_isBase_superset, _private.0.Matroid.Indep.cardinalMk_le_cRank.match_1, Cardinal.mk_le_mk_of_subset, Cardinal.bddAbove_of_small
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
B : { B : Set α // M.IsBase B }
⊢ #(↑(↑B : Set α) : Type u) ≤ #(↑(↑B : Set α) : Type u)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
⊢ #(↑I : Type u) ≤ M.cRk X

Tactic:
(isBase_restrict_iff'.2 hIX).cardinalMk_le_cRank

Premises used: Iff.mpr, Matroid.isBase_restrict_iff', Matroid.IsBase.cardinalMk_le_cRank, Matroid.cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ #(↑I : Type u) ≤ M.cRk X

Tactic:
hIX.isBasis'.cardinalMk_le_cRk

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.cardinalMk_le_cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
κ : Cardinal.{u}
⊢ M.cRank ≤ κ ↔ ∀ ⦃B : Set α⦄, M.IsBase B → #(↑B : Type u) ≤ κ

Tactic:
⟨fun h _ hB ↦ (hB.cardinalMk_le_cRank.trans h), fun h ↦ ciSup_le fun ⟨_, hB⟩ ↦ h hB⟩

Premises used: Matroid.IsBase.cardinalMk_le_cRank, Cardinal.mk, Set.Elem, LE.le, Iff.intro, LE.le.trans, Subtype.val, _private.0.Matroid.cRank_le_iff.match_1, ciSup_le
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
simp_rw : (M ↾ X).cRank ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #(↑I : Type u) ≤ κ
simp_rw₁ : (∀ ⦃B : Set α⦄, (M ↾ X).IsBase B → #(↑B : Type u) ≤ κ) ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #(↑I : Type u) ≤ κ
⊢ M.cRk X ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #(↑I : Type u) ≤ κ

Tactic:
simp_rw [cRk, cRank_le_iff, isBase_restrict_iff']

Premises used: Matroid.isBase_restrict_iff', Matroid.cRank_le_iff, Matroid.cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ #(↑I : Type u) ≤ M.cRk X

Tactic:
let ⟨_, hJ, hIJ⟩ := hI.subset_isBasis'_of_subset hIX
  (mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cRk

Premises used: Cardinal.mk, Set.Elem, LE.le, Matroid.Indep.subset_isBasis'_of_subset, Cardinal.mk_le_mk_of_subset, Matroid.cRk, _private.0.Matroid.Indep.cardinalMk_le_cRk_of_subset.match_1, LE.le.trans, Matroid.IsBasis'.cardinalMk_le_cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X : Set α
⊢ M.cRk X ≤ #(↑X : Type u)

Tactic:
ciSup_le fun ⟨_, hI⟩ ↦ mk_le_mk_of_subset hI.subset_ground

Premises used: Cardinal.mk, Set.Elem, Matroid.IsBase.subset_ground, LE.le, Matroid.cRank, Cardinal.mk_le_mk_of_subset, Matroid.cRk, _private.0.Matroid.cRk_le_cardinalMk.match_1, Subtype.val, ciSup_le
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
rw : (M ↾ M.E).cRank = M.cRank
rw₁ rw₂ : M.cRank = M.cRank
⊢ M.cRk M.E = M.cRank

Tactic:
rw [cRk, restrict_ground_eq_self]

Premises used: Matroid.restrict_ground_eq_self, Matroid.cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X : Set α
⊢ (M ↾ X).cRank = M.cRk X

Tactic:
rfl

Premises used: Matroid.cRk, rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
simp : ∀ ⦃a b : Set α⦄, a ⊆ b → ∀ ⦃I : Set α⦄, M.IsBasis' I a → #(↑I : Type u) ≤ M.cRk b
⊢ Monotone M.cRk

Tactic:
simp only [Monotone, le_eq_subset, cRk_le_iff]

Premises used: Set.le_eq_subset, Monotone, Matroid.cRk_le_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
obtain : ∀ (J : Set α) (hJ : M.IsBasis' J Y) (hIJ : I ⊆ J), #(↑I : Type u) ≤ M.cRk Y
⊢ #(↑I : Type u) ≤ M.cRk Y

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hIX.indep.subset_isBasis'_of_subset (hIX.subset.trans hXY)

Premises used: HasSubset.Subset.trans, Matroid.IsBasis'.indep, Matroid.Indep.subset_isBasis'_of_subset, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ #(↑I : Type u) ≤ M.cRk Y

Tactic:
(mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cRk

Premises used: Cardinal.mk_le_mk_of_subset, LE.le.trans, Matroid.IsBasis'.cardinalMk_le_cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ #(↑I : Type u) ≤ M.cRk Y

Tactic:
exact (mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cRk

Premises used: Cardinal.mk_le_mk_of_subset, LE.le.trans, Matroid.IsBasis'.cardinalMk_le_cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
⊢ M.cRk X ≤ M.cRk Y

Tactic:
M.cRk_mono hXY

Premises used: Matroid.cRk_mono
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X : Set α
⊢ M.cRk (X ∩ M.E) = M.cRk X

Tactic:
(M.cRk_le_of_subset inter_subset_left).antisymm <| cRk_le_iff.2
    fun _ h ↦ h.isBasis_inter_ground.cardinalMk_le_cRk

Premises used: Iff.mpr, LE.le.antisymm, Matroid.IsBasis.cardinalMk_le_cRk, Set.inter_subset_left, Matroid.IsBasis'.isBasis_inter_ground, Matroid.cRk_le_iff, Matroid.cRk_le_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
simp_rw : ∀ ⦃I : Set α⦄, M.IsBasis' I Y → I ⊆ X
⊢ ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y

Tactic:
simp_rw [isBasis'_restrict_iff, inter_eq_self_of_subset_left hYX, iff_self_and]

Premises used: Matroid.isBasis'_restrict_iff, iff_self_and, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ ∀ ⦃I : Set α⦄, M.IsBasis' I Y → I ⊆ X

Tactic:
fun I h ↦ h.subset.trans hYX

Premises used: HasSubset.Subset.trans, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ ∀ ⦃I : Set α⦄, M.IsBasis' I Y → I ⊆ X

Tactic:
exact fun I h ↦ h.subset.trans hYX
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ ∀ ⦃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
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
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
⊢ (M ↾ X).cRk Y = M.cRk Y

Tactic:
simp_rw [le_antisymm_iff, cRk_le_iff]

Premises used: Matroid.cRk_le_iff, le_antisymm_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (∀ ⦃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:
⟨fun I hI ↦ (aux.2 hI).cardinalMk_le_cRk, fun I hI ↦ (aux.1 hI).cardinalMk_le_cRk⟩

Premises used: Iff.mpr, And.intro, Iff.mp, Matroid.IsBasis'.cardinalMk_le_cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (∀ ⦃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:
exact ⟨fun I hI ↦ (aux.2 hI).cardinalMk_le_cRk, fun I hI ↦ (aux.1 hI).cardinalMk_le_cRk⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
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)
rw₃ rw₄ : M.cRk (X ∩ Y) = M.cRk (X ∩ Y)
⊢ (M ↾ X).cRk Y = M.cRk (X ∩ Y)

Tactic:
rw [← cRk_inter_ground, restrict_ground_eq, cRk_restrict_subset _ inter_subset_right,
    inter_comm]

Premises used: Matroid.cRk_restrict_subset, Matroid.cRk_inter_ground, Matroid.restrict_ground_eq, Set.inter_comm, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I : Set α
hI : M.Indep I
⊢ #(↑I : Type u) = M.cRk I

Tactic:
(M.cRk_le_cardinalMk I).antisymm' (hI.isBasis_self.cardinalMk_le_cRk)

Premises used: LE.le.antisymm', Matroid.cRk_le_cardinalMk, Matroid.IsBasis.cardinalMk_le_cRk, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
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))
⊢ lift.{u, v} ((M.map f hf).cRk (f '' X)) = lift.{v, u} (M.cRk X)

Tactic:
nth_rw 1 [cRk, cRank, le_antisymm_iff, lift_iSup bddAbove_of_small, cRk, cRank, cRk, cRank]

Premises used: Cardinal.lift_iSup, Matroid.cRank, le_antisymm_iff, Matroid.cRk, Cardinal.bddAbove_of_small
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
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))
⊢ ⨆ (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 2 [lift_iSup bddAbove_of_small]

Premises used: Cardinal.lift_iSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
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))
⊢ ⨆ (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:
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)]

Premises used: Matroid.isBase_restrict_iff', ciSup_le_iff, Set.image_mono, Subtype.forall, Matroid.isBasis'_iff_isBasis, Cardinal.bddAbove_of_small
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
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))

Tactic:
⟨fun I hI ↦ ?_, fun I hI ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
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))
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))
⊢ (∀ (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:
refine ⟨fun I hI ↦ ?_, fun I hI ↦ ?_⟩