awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X I : Set α
hI : M.IsBasis' I X
rw : #(↑I : Type u) = M.cRk X
rw₁ rw₂ : #(↑I : Type u) = #(↑I : Type u)
⊢ M.cRk (M.closure X) = M.cRk X

Tactic:
rw [← hI.isBasis_closure_right.cardinalMk_eq_cRk, ← hI.cardinalMk_eq_cRk]

Premises used: Matroid.IsBasis'.cardinalMk_eq_cRk, Matroid.IsBasis.cardinalMk_eq_cRk, Matroid.IsBasis'.isBasis_closure_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X Y : Set α
inst : M.InvariantCardinalRank
hXY : M.closure X = M.closure Y
rw : M.cRk (M.closure X) = M.cRk Y
rw₁ : M.cRk (M.closure Y) = M.cRk Y
rw₂ rw₃ : M.cRk Y = M.cRk Y
⊢ M.cRk X = M.cRk Y

Tactic:
rw [← cRk_closure, hXY, cRk_closure]

Premises used: Matroid.cRk_closure
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X : Set α
inst : M.InvariantCardinalRank
h : M.Spanning X
⊢ M.cRank ≤ #(↑X : Type u)

Tactic:
have ⟨_B, hB, hBX⟩ := h.exists_isBase_subset
  (hB.cardinalMk_eq_cRank).symm.trans_le (mk_le_mk_of_subset hBX)

Premises used: Cardinal.mk, Matroid.IsBase.cardinalMk_eq_cRank, Set.Elem, Eq.trans_le, LE.le, Matroid.Spanning.exists_isBase_subset, Matroid.cRank, Cardinal.mk_le_mk_of_subset, _private.0.Matroid.Spanning.cRank_le_cardinalMk.match_1, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X Y : Set α
⊢ M.cRk (X ∪ M.closure Y) = M.cRk (X ∪ Y)

Tactic:
M.cRk_closure_congr (M.closure_union_closure_right_eq _ _)

Premises used: Matroid.closure_union_closure_right_eq, Matroid.cRk_closure_congr
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X Y : Set α
⊢ M.cRk (M.closure X ∪ Y) = M.cRk (X ∪ Y)

Tactic:
M.cRk_closure_congr (M.closure_union_closure_left_eq _ _)

Premises used: Matroid.closure_union_closure_left_eq, Matroid.cRk_closure_congr
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
e : α
X : Set α
rw : M.cRk (M.closure X ∪ {e}) = M.cRk (insert e X)
rw₁ : M.cRk (X ∪ {e}) = M.cRk (insert e X)
rw₂ rw₃ : M.cRk (insert e X) = M.cRk (insert e X)
⊢ M.cRk (insert e (M.closure X)) = M.cRk (insert e X)

Tactic:
rw [← union_singleton, cRk_union_closure_left_eq, union_singleton]

Premises used: Matroid.cRk_union_closure_left_eq, Set.union_singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X Y : Set α
⊢ M.cRk (M.closure X ∪ M.closure Y) = M.cRk (X ∪ Y)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X Y : Set α
obtain : ∀ (Ii : Set α) (hIi : M.IsBasis' Ii (X ∩ Y)), M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Tactic:
obtain ⟨Ii, hIi⟩ := M.exists_isBasis' (X ∩ Y)

Premises used: Inter.inter, Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
obtain : ∀ (IX : Set α) (hIX : M.IsBasis' IX X) (hIX' : Ii ⊆ IX), M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Tactic:
obtain ⟨IX, hIX, hIX'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_left)

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Matroid.IsBasis'.indep, Matroid.Indep.subset_isBasis'_of_subset, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
obtain : ∀ (IY : Set α) (hIY : M.IsBasis' IY Y) (hIY' : Ii ⊆ IY), M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Tactic:
obtain ⟨IY, hIY, hIY'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_right)

Premises used: HasSubset.Subset.trans, Matroid.IsBasis'.indep, Matroid.Indep.subset_isBasis'_of_subset, Matroid.IsBasis'.subset, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
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
rw : M.cRk (IX ∪ IY) + #(↑Ii : Type u) ≤ #(↑(IX ∪ IY) : Type u) + #(↑(IX ∩ IY) : Type u)
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Tactic:
rw [← cRk_union_closure_eq, ← hIX.closure_eq_closure, ← hIY.closure_eq_closure,
    cRk_union_closure_eq, ← hIi.cardinalMk_eq_cRk, ← hIX.cardinalMk_eq_cRk,
    ← hIY.cardinalMk_eq_cRk, ← mk_union_add_mk_inter, add_comm]

Premises used: Matroid.IsBasis'.closure_eq_closure, Cardinal.mk_union_add_mk_inter, Matroid.IsBasis'.cardinalMk_eq_cRk, Matroid.cRk_union_closure_eq, add_comm
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
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.cRk (IX ∪ IY) + #(↑Ii : Type u) ≤ #(↑(IX ∪ IY) : Type u) + #(↑(IX ∩ IY) : Type u)

Tactic:
add_le_add (M.cRk_le_cardinalMk _) (mk_le_mk_of_subset (subset_inter hIX' hIY'))

Premises used: add_le_add, Matroid.cRk_le_cardinalMk, Set.subset_inter, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
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.cRk (IX ∪ IY) + #(↑Ii : Type u) ≤ #(↑(IX ∪ IY) : Type u) + #(↑(IX ∩ IY) : Type u)

Tactic:
exact add_le_add (M.cRk_le_cardinalMk _) (mk_le_mk_of_subset (subset_inter hIX' hIY'))

Premises used: add_le_add, Matroid.cRk_le_cardinalMk, Set.subset_inter, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B B' X Y : Set α
inst : M.Finitary
suffices :
  ∀ ⦃B B' : Set α⦄ ⦃N : Matroid α⦄,
    N.Finitary → N.IsBase B → N.IsBase B' → #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
⊢ M.InvariantCardinalRank

Tactic:
suffices aux : ∀ ⦃B B'⦄ ⦃N : Matroid α⦄, Finitary N → N.IsBase B → N.IsBase B' →
      #(B \ B' : Set α) ≤ #(B' \ B : Set α) from
    ⟨fun I J X hI hJ ↦ (aux (restrict_finitary X) hI.isBase_restrict hJ.isBase_restrict).antisymm
      (aux (restrict_finitary X) hJ.isBase_restrict hI.isBase_restrict)⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
pos : ∀ (h : (B' \ B).Finite), #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
neg : ∀ (h : ¬(B' \ B).Finite), #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)

Tactic:
by_cases h : (B' \ B).Finite

Premises used: Set.Finite, SDiff.sdiff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : (B' \ B).Finite
pos : (B \ B').Finite
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)

Tactic:
rw [← cast_ncard h, ← cast_ncard, hB.ncard_diff_comm hB']

Premises used: Matroid.IsBase.ncard_diff_comm, Set.cast_ncard
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : (B' \ B).Finite
⊢ (B \ B').Finite

Tactic:
(hB'.diff_finite_comm hB).mp h

Premises used: Matroid.IsBase.diff_finite_comm, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : (B' \ B).Finite
⊢ (B \ B').Finite

Tactic:
exact (hB'.diff_finite_comm hB).mp h

Premises used: Matroid.IsBase.diff_finite_comm, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : ¬(B' \ B).Finite
⊢ Infinite.{u + 1} (↑(B' \ B) : Type u)

Tactic:
rw [← Set.Infinite, ← infinite_coe_iff] at h

Premises used: Set.infinite_coe_iff, Set.Infinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
a : α
ha : a ∈ B' \ B
⊢ ¬N.Indep (insert a B)

Tactic:
have := (hB.insert_dep ⟨hB'.subset_ground ha.1, ha.2⟩).1
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
a : α
ha : a ∈ B' \ B
this : ¬N.Indep (insert a B)
contrapose! :
  ∀ (this : ∀ (S : Set α) (_ : Finite.{u + 1} (↑S : Type u)) (_ : S ⊆ B), N.Indep (insert a S)), N.Indep (insert a B)
⊢ ∃ (S : Set α), Finite.{u + 1} (↑S : Type u) ∧ S ⊆ B ∧ ¬N.Indep (insert a S)

Tactic:
contrapose! this
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
a : α
ha : a ∈ B' \ B
this : ∀ (S : Set α) (_ : Finite.{u + 1} (↑S : Type u)) (_ : S ⊆ B), N.Indep (insert a S)
⊢ N.Indep (insert a B)

Tactic:
Finitary.indep_of_forall_finite _ fun J hJ fin ↦ (this (J \ {a}) fin.diff.to_subtype <|
      diff_singleton_subset_iff.mpr hJ).subset (subset_insert_diff_singleton ..)

Premises used: Iff.mpr, Matroid.Finitary.indep_of_forall_finite, Set.diff_singleton_subset_iff, Matroid.Indep.subset, Set.Finite.diff, Set.Finite.to_subtype, SDiff.sdiff, Set.subset_insert_diff_singleton, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
a : α
ha : a ∈ B' \ B
this : ∀ (S : Set α) (_ : Finite.{u + 1} (↑S : Type u)) (_ : S ⊆ B), N.Indep (insert a S)
⊢ N.Indep (insert a B)

Tactic:
exact Finitary.indep_of_forall_finite _ fun J hJ fin ↦ (this (J \ {a}) fin.diff.to_subtype <|
      diff_singleton_subset_iff.mpr hJ).subset (subset_insert_diff_singleton ..)

Premises used: Iff.mpr, Matroid.Finitary.indep_of_forall_finite, Set.diff_singleton_subset_iff, Matroid.Indep.subset, Set.Finite.diff, Set.Finite.to_subtype, SDiff.sdiff, Set.subset_insert_diff_singleton, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
⊢ ∀ (a : α) (ha : a ∈ B' \ B), ∃ (S : Set α), Finite.{u + 1} (↑S : Type u) ∧ S ⊆ B ∧ ¬N.Indep (insert a S)

Tactic:
have (a : α) (ha : a ∈ B' \ B) : ∃ S : Set α, Finite S ∧ S ⊆ B ∧ ¬ N.Indep (insert a S) := by
    have := (hB.insert_dep ⟨hB'.subset_ground ha.1, ha.2⟩).1
    contrapose! this
    exact Finitary.indep_of_forall_finite _ fun J hJ fin ↦ (this (J \ {a}) fin.diff.to_subtype <|
      diff_singleton_subset_iff.mpr hJ).subset (subset_insert_diff_singleton ..)
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
this : ∀ (a : α) (ha : a ∈ B' \ B), ∃ (S : Set α), Finite.{u + 1} (↑S : Type u) ∧ S ⊆ B ∧ ¬N.Indep (insert a S)
neg :
  ∀ (S : (a : α) → (ha : a ∈ B' \ B) → Set α) (S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u))
    (hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B) (dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))),
    #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)

Tactic:
choose S S_fin hSB dep using this
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
this : B \ B' ⊆ U
⊢ ℵ₀ ≤ #(↑(B' \ B) : Type u)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
this : B \ B' ⊆ U
refine : max (#(↑(B' \ B) : Type u)) (⨆ (i : (↑(B' \ B) : Type u)), #(↑(S (↑i : α) ⋯) : Type u)) ≤ #(↑(B' \ B) : Type u)
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)

Tactic:
refine (mk_le_mk_of_subset this).trans <| (mk_iUnion_le ..).trans
      <| (mul_le_max_of_aleph0_le_left (by simp)).trans ?_

Premises used: Cardinal.mul_le_max_of_aleph0_le_left, Cardinal.mk_le_mk_of_subset, LE.le.trans, Cardinal.mk_iUnion_le
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
this : B \ B' ⊆ U
simp : ⨆ (i : (↑(B' \ B) : Type u)), #(↑(S (↑i : α) ⋯) : Type u) ≤ #(↑(B' \ B) : Type u)
⊢ max (#(↑(B' \ B) : Type u)) (⨆ (i : (↑(B' \ B) : Type u)), #(↑(S (↑i : α) ⋯) : Type u)) ≤ #(↑(B' \ B) : Type u)

Tactic:
simp only [sup_le_iff, le_refl, true_and]

Premises used: le_refl, sup_le_iff, true_and
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
this : B \ B' ⊆ U
e : (↑(B' \ B) : Type u)
⊢ ℵ₀ ≤ #(↑(B' \ B) : Type u)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
this : B \ B' ⊆ U
⊢ ⨆ (i : (↑(B' \ B) : Type u)), #(↑(S (↑i : α) ⋯) : Type u) ≤ #(↑(B' \ B) : Type u)

Tactic:
exact ciSup_le' fun e ↦ (lt_aleph0_of_finite _).le.trans <| by simp

Premises used: LT.lt.le, ciSup_le', Cardinal.lt_aleph0_of_finite, LE.le.trans
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
neg : B \ B' ⊆ U
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)

Tactic:
suffices B \ B' ⊆ U by
    refine (mk_le_mk_of_subset this).trans <| (mk_iUnion_le ..).trans
      <| (mul_le_max_of_aleph0_le_left (by simp)).trans ?_
    simp only [sup_le_iff, le_refl, true_and]
    exact ciSup_le' fun e ↦ (lt_aleph0_of_finite _).le.trans <| by simp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
neg : B ⊆ B ∩ B' ∪ U
⊢ B \ B' ⊆ U

Tactic:
rw [← diff_inter_self_eq_diff, diff_subset_iff, inter_comm]

Premises used: Set.diff_subset_iff, Set.inter_comm, Set.diff_inter_self_eq_diff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
⊢ B ∩ B' ∪ U ⊆ B

Tactic:
have hUB : (B ∩ B') ∪ U ⊆ B :=
    union_subset inter_subset_left (iUnion_subset fun e ↦ (hSB e.1 e.2))
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
hUB : B ∩ B' ∪ U ⊆ B
neg : ∀ (hBU : ¬B ⊆ B ∩ B' ∪ U), False
⊢ B ⊆ B ∩ B' ∪ U

Tactic:
by_contra hBU
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
hUB : B ∩ B' ∪ U ⊆ B
hBU : ¬B ⊆ B ∩ B' ∪ U
neg : ∀ (a : α) (ha : a ∈ B' \ (B ∩ B' ∪ U)) (ind : N.Indep (insert a (B ∩ B' ∪ U))), False
⊢ False

Tactic:
have ⟨a, ha, ind⟩ := hB.exists_insert_of_ssubset ⟨hUB, hBU⟩ hB'
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
hUB : B ∩ B' ∪ U ⊆ B
hBU : ¬B ⊆ B ∩ B' ∪ U
a : α
ha : a ∈ B' \ (B ∩ B' ∪ U)
ind : N.Indep (insert a (B ∩ B' ∪ U))
⊢ a ∈ B' \ B

Tactic:
have : a ∈ B' \ B := ⟨ha.1, fun haB ↦ ha.2 (.inl ⟨haB, ha.1⟩)⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
hUB : B ∩ B' ∪ U ⊆ B
hBU : ¬B ⊆ B ∩ B' ∪ U
a : α
ha : a ∈ B' \ (B ∩ B' ∪ U)
ind : N.Indep (insert a (B ∩ B' ∪ U))
this : a ∈ B' \ B
⊢ False

Tactic:
dep a this (ind.subset <| insert_subset_insert <| .trans ?_ subset_union_right)

Premises used: Set.subset_union_right, HasSubset.Subset.trans, Matroid.Indep.subset, Set.insert_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
hUB : B ∩ B' ∪ U ⊆ B
hBU : ¬B ⊆ B ∩ B' ∪ U
a : α
ha : a ∈ B' \ (B ∩ B' ∪ U)
ind : N.Indep (insert a (B ∩ B' ∪ U))
this : a ∈ B' \ B
neg : S a this ⊆ U
⊢ False

Tactic:
refine dep a this (ind.subset <| insert_subset_insert <| .trans ?_ subset_union_right)

Premises used: Set.subset_union_right, HasSubset.Subset.trans, Matroid.Indep.subset, Set.insert_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
hUB : B ∩ B' ∪ U ⊆ B
hBU : ¬B ⊆ B ∩ B' ∪ U
a : α
ha : a ∈ B' \ (B ∩ B' ∪ U)
ind : N.Indep (insert a (B ∩ B' ∪ U))
this : a ∈ B' \ B
⊢ S a this ⊆ U

Tactic:
subset_iUnion_of_subset ⟨a, this⟩ subset_rfl

Premises used: Set.subset_iUnion_of_subset, Subtype.mk, subset_rfl