awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift.{u, v} #(↑(range f) : Type v) = lift.{v, u} #α

Tactic:
lift_mk_eq'.mpr ⟨(Equiv.ofInjective f hf).symm⟩

Premises used: Iff.mpr, Cardinal.lift_mk_eq', Nonempty.intro, Equiv.ofInjective, Equiv.symm
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift.{max u w, v} #(↑(range f) : Type v) = lift.{max v w, u} #α

Tactic:
lift_mk_eq.{v, u, w}.mpr ⟨(Equiv.ofInjective f hf).symm⟩

Premises used: Iff.mpr, Cardinal.lift_mk_eq, Nonempty.intro, Equiv.ofInjective, Equiv.symm
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Injective f
rw : lift.{u, v} #(↑(range f) : Type v) ≤ lift.{u, v} #β
⊢ lift.{v, u} #α ≤ lift.{u, v} #β

Tactic:
rw [← Cardinal.mk_range_eq_of_injective hf]

Premises used: Cardinal.mk_range_eq_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift.{u, v} #(↑(range f) : Type v) ≤ lift.{u, v} #β

Tactic:
Cardinal.lift_le.2 (Cardinal.mk_set_le _)

Premises used: Iff.mpr, Cardinal.mk_set_le, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift.{u, v} #(↑(range f) : Type v) ≤ lift.{u, v} #β

Tactic:
exact Cardinal.lift_le.2 (Cardinal.mk_set_le _)

Premises used: Iff.mpr, Cardinal.mk_set_le, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Surjective f
⊢ lift.{u, v} #β ≤ lift.{v, u} #α

Tactic:
lift_mk_le_lift_mk_of_injective (injective_surjInv hf)

Premises used: Cardinal.lift_mk_le_lift_mk_of_injective, Function.injective_surjInv
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set α
h : InjOn f s
⊢ #(↑(f '' s) : Type u) = #(↑s : Type u)

Tactic:
mk_congr (Equiv.Set.imageOfInjOn f s h).symm

Premises used: Equiv.Set.imageOfInjOn, Equiv.symm, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h : InjOn f s
⊢ lift.{u, v} #(↑(f '' s) : Type v) = lift.{v, u} #(↑s : Type u)

Tactic:
lift_mk_eq.{v, u, 0}.mpr ⟨(Equiv.Set.imageOfInjOn f s h).symm⟩

Premises used: Iff.mpr, Cardinal.lift_mk_eq, Nonempty.intro, Equiv.Set.imageOfInjOn, Equiv.symm
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set α
hf : Injective f
⊢ #(↑(f '' s) : Type u) = #(↑s : Type u)

Tactic:
mk_image_eq_of_injOn _ _ hf.injOn

Premises used: Function.Injective.injOn, Cardinal.mk_image_eq_of_injOn
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
h : Injective f
⊢ lift.{u, v} #(↑(f '' s) : Type v) = lift.{v, u} #(↑s : Type u)

Tactic:
mk_image_eq_of_injOn_lift _ _ h.injOn

Premises used: Function.Injective.injOn, Cardinal.mk_image_eq_of_injOn_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α ↪ β
s : Set α
⊢ lift.{u, v} #(↑((⇑f : (a : α) → β) '' s) : Type v) = lift.{v, u} #(↑s : Type u)

Tactic:
mk_image_eq_lift _ _ f.injective

Premises used: Cardinal.mk_image_eq_lift, Function.Embedding.injective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α ↪ β
s : Set α
⊢ #(↑((⇑f : (a : α) → β) '' s) : Type u) = #(↑s : Type u)

Tactic:
simpa using mk_image_embedding_lift f s

Premises used: Cardinal.mk_image_embedding_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
ι : Type v
f : ι → Set α
⊢ ⨆ (i : ι), #(↑(f i) : Type u) ≤ #(↑(⋃ (i : ι), f i) : Type u)

Tactic:
ciSup_le' fun _ => mk_le_mk_of_subset (subset_iUnion _ _)

Premises used: ciSup_le', Set.subset_iUnion, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α ι : Type u
f : ι → Set α
⊢ #(↑(⋃ (i : ι), f i) : Type u) ≤ sum fun (i : ι) ↦ #(↑(f i) : Type u)

Tactic:
calc
    #(⋃ i, f i) ≤ #(Σ i, f i) := mk_le_of_surjective (Set.sigmaToiUnion_surjective f)
    _ = sum fun i => #(f i) := mk_sigma _

Premises used: Cardinal.mk_le_of_surjective, Trans.trans, Cardinal.mk_sigma, Set.sigmaToiUnion_surjective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
ι : Type v
f : ι → Set α
⊢ lift.{v, u} #(↑(⋃ (i : ι), f i) : Type u) ≤ sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)

Tactic:
calc
    lift.{v} #(⋃ i, f i) ≤ #(Σ i, f i) :=
      mk_le_of_surjective <| ULift.up_surjective.comp (Set.sigmaToiUnion_surjective f)
    _ = sum fun i => #(f i) := mk_sigma _

Premises used: Cardinal.mk_le_of_surjective, Trans.trans, ULift.up_surjective, Cardinal.mk_sigma, Function.Surjective.comp, Set.sigmaToiUnion_surjective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α ι : Type u
f : ι → Set α
h : Pairwise (Disjoint on f)
⊢ #(↑(⋃ (i : ι), f i) : Type u) = sum fun (i : ι) ↦ #(↑(f i) : Type u)

Tactic:
calc
    #(⋃ i, f i) = #(Σ i, f i) := mk_congr (Set.unionEqSigmaOfDisjoint h)
    _ = sum fun i => #(f i) := mk_sigma _

Premises used: Trans.trans, Set.unionEqSigmaOfDisjoint, Cardinal.mk_sigma, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
ι : Type v
f : ι → Set α
h : Pairwise (Disjoint on f)
⊢ lift.{v, u} #(↑(⋃ (i : ι), f i) : Type u) = sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)

Tactic:
calc
    lift.{v} #(⋃ i, f i) = #(Σ i, f i) :=
      mk_congr <| .trans Equiv.ulift (Set.unionEqSigmaOfDisjoint h)
    _ = sum fun i => #(f i) := mk_sigma _

Premises used: Trans.trans, Equiv.trans, Equiv.ulift, Set.unionEqSigmaOfDisjoint, Cardinal.mk_sigma, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α ι : Type u
f : ι → Set α
⊢ #(↑(⋃ (i : ι), f i) : Type u) ≤ #ι * ⨆ (i : ι), #(↑(f i) : Type u)

Tactic:
mk_iUnion_le_sum_mk.trans (sum_le_mk_mul_iSup _)

Premises used: Cardinal.sum_le_mk_mul_iSup, Cardinal.mk_iUnion_le_sum_mk, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
ι : Type v
f : ι → Set α
⊢ lift.{v, u} #(↑(⋃ (i : ι), f i) : Type u) ≤ lift.{u, v} #ι * ⨆ (i : ι), lift.{v, u} #(↑(f i) : Type u)

Tactic:
mk_iUnion_le_sum_mk_lift.trans <| Eq.trans_le ?_ (sum_le_lift_mk_mul_iSup _)

Premises used: Cardinal.mk_iUnion_le_sum_mk_lift, Eq.trans_le, Cardinal.sum_le_lift_mk_mul_iSup, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
ι : Type v
f : ι → Set α
refine : (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)) = sum fun (i : ι) ↦ lift.{v, u} #(↑(f i) : Type u)
⊢ lift.{v, u} #(↑(⋃ (i : ι), f i) : Type u) ≤ lift.{u, v} #ι * ⨆ (i : ι), lift.{v, u} #(↑(f i) : Type u)

Tactic:
refine mk_iUnion_le_sum_mk_lift.trans <| Eq.trans_le ?_ (sum_le_lift_mk_mul_iSup _)

Premises used: Cardinal.mk_iUnion_le_sum_mk_lift, Eq.trans_le, Cardinal.sum_le_lift_mk_mul_iSup, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
ι : Type v
f : ι → Set α
rw : (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)) = lift.{v, max u v} (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u))
rw₁ rw₂ : (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)) = sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)
⊢ (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)) = sum fun (i : ι) ↦ lift.{v, u} #(↑(f i) : Type u)

Tactic:
rw [← lift_sum, lift_id'.{_, u}]

Premises used: Cardinal.lift_sum
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
A : Set (Set α)
rw :
  #(↑(⋃ (i : (↑A : Type u)), (↑i : Set α)) : Type u) ≤ #(↑A : Type u) * ⨆ (s : (↑A : Type u)), #(↑(↑s : Set α) : Type u)
⊢ #(↑(⋃₀ A) : Type u) ≤ #(↑A : Type u) * ⨆ (s : (↑A : Type u)), #(↑(↑s : Set α) : Type u)

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
A : Set (Set α)
⊢ #(↑(⋃ (i : (↑A : Type u)), (↑i : Set α)) : Type u) ≤ #(↑A : Type u) * ⨆ (s : (↑A : Type u)), #(↑(↑s : Set α) : Type u)

Tactic:
apply mk_iUnion_le

Premises used: Cardinal.mk_iUnion_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι α : Type u
A : ι → Set α
s : Set ι
rw :
  #(↑(⋃ (x : (↑s : Type u)), A (↑x : ι)) : Type u) ≤ #(↑s : Type u) * ⨆ (x : (↑s : Type u)), #(↑(A (↑x : ι)) : Type u)
⊢ #(↑(⋃ x ∈ s, A x) : Type u) ≤ #(↑s : Type u) * ⨆ (x : (↑s : Type u)), #(↑(A (↑x : ι)) : Type u)

Tactic:
rw [biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι α : Type u
A : ι → Set α
s : Set ι
⊢ #(↑(⋃ (x : (↑s : Type u)), A (↑x : ι)) : Type u) ≤ #(↑s : Type u) * ⨆ (x : (↑s : Type u)), #(↑(A (↑x : ι)) : Type u)

Tactic:
apply mk_iUnion_le

Premises used: Cardinal.mk_iUnion_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
ι : Type v
A : ι → Set α
s : Set ι
rw :
  lift.{v, u} #(↑(⋃ (x : (↑s : Type v)), A (↑x : ι)) : Type u) ≤
    lift.{u, v} #(↑s : Type v) * ⨆ (x : (↑s : Type v)), lift.{v, u} #(↑(A (↑x : ι)) : Type u)
⊢ lift.{v, u} #(↑(⋃ x ∈ s, A x) : Type u) ≤
    lift.{u, v} #(↑s : Type v) * ⨆ (x : (↑s : Type v)), lift.{v, u} #(↑(A (↑x : ι)) : Type u)

Tactic:
rw [biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
ι : Type v
A : ι → Set α
s : Set ι
⊢ lift.{v, u} #(↑(⋃ (x : (↑s : Type v)), A (↑x : ι)) : Type u) ≤
    lift.{u, v} #(↑s : Type v) * ⨆ (x : (↑s : Type v)), lift.{v, u} #(↑(A (↑x : ι)) : Type u)

Tactic:
apply mk_iUnion_le_lift

Premises used: Cardinal.mk_iUnion_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Finset α
⊢ #(↑(↑s : Set α) : Type u) < ℵ₀

Tactic:
lt_aleph0_of_finite _

Premises used: Cardinal.lt_aleph0_of_finite
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
s : Set α
n : ℕ
mp : #(↑s : Type u_1) = (↑n : Cardinal.{u_1}) → ∃ (t : Finset α), (↑t : Set α) = s ∧ t.card = n
mpr : (∃ (t : Finset α), (↑t : Set α) = s ∧ t.card = n) → #(↑s : Type u_1) = (↑n : Cardinal.{u_1})
⊢ #(↑s : Type u_1) = (↑n : Cardinal.{u_1}) ↔ ∃ (t : Finset α), (↑t : Set α) = s ∧ t.card = n

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
s : Set α
n : ℕ
h : #(↑s : Type u_1) = (↑n : Cardinal.{u_1})
⊢ s.Finite

Tactic:
lt_aleph0_iff_set_finite.1 (h.symm ▸ natCast_lt_aleph0)

Premises used: Eq.rec, Cardinal.natCast_lt_aleph0, Iff.mp, Eq.symm, Cardinal.lt_aleph0_iff_set_finite
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
s : Set α
n : ℕ
h : #(↑s : Type u_1) = (↑n : Cardinal.{u_1})
mp :
  ∀ (s : Finset α) (h : #(↑(↑s : Set α) : Type u_1) = (↑n : Cardinal.{u_1})),
    ∃ (t : Finset α), (↑t : Set α) = (↑s : Set α) ∧ t.card = n
⊢ ∃ (t : Finset α), (↑t : Set α) = s ∧ t.card = n

Tactic:
lift s to Finset α using lt_aleph0_iff_set_finite.1 (h.symm ▸ natCast_lt_aleph0)

Premises used: Finset, Iff.mp, Cardinal.lt_aleph0_iff_set_finite
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
n : ℕ
s : Finset α
h : #(↑(↑s : Set α) : Type u_1) = (↑n : Cardinal.{u_1})
⊢ ∃ (t : Finset α), (↑t : Set α) = (↑s : Set α) ∧ t.card = n

Tactic:
simpa using h
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
t : Finset α
⊢ #(↑(↑t : Set α) : Type u_1) = (↑t.card : Cardinal.{u_1})

Tactic:
mk_coe_finset

Premises used: Cardinal.mk_coe_finset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
t : Finset α
⊢ #(↑(↑t : Set α) : Type u_1) = (↑t.card : Cardinal.{u_1})

Tactic:
exact mk_coe_finset

Premises used: Cardinal.mk_coe_finset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
rw : #(↑univ : Type u) = (↑n : Cardinal.{u}) ↔ ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n
rw₁ rw₂ : (∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n) ↔ ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n
⊢ #α = (↑n : Cardinal.{u}) ↔ ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n

Tactic:
rw [← mk_univ, mk_set_eq_nat_iff_finset]

Premises used: Cardinal.mk_univ, Cardinal.mk_set_eq_nat_iff_finset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
rw : (∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n) ↔ ∃ (h : Fintype α), Fintype.card α = n
⊢ #α = (↑n : Cardinal.{u}) ↔ ∃ (h : Fintype α), Fintype.card α = n

Tactic:
rw [mk_eq_nat_iff_finset]

Premises used: Cardinal.mk_eq_nat_iff_finset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
mp : (∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n) → ∃ (h : Fintype α), Fintype.card α = n
mpr : (∃ (h : Fintype α), Fintype.card α = n) → ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n
⊢ (∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n) ↔ ∃ (h : Fintype α), Fintype.card α = n

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
t : Finset α
ht : (↑t : Set α) = univ
hn : t.card = n
⊢ ∃ (h : Fintype α), Fintype.card α = n

Tactic:
⟨⟨t, eq_univ_iff_forall.1 ht⟩, hn⟩

Premises used: Set.eq_univ_iff_forall, Fintype.mk, Exists.intro, Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
t : Finset α
ht : (↑t : Set α) = univ
hn : t.card = n
⊢ ∃ (h : Fintype α), Fintype.card α = n

Tactic:
exact ⟨⟨t, eq_univ_iff_forall.1 ht⟩, hn⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
t : Finset α
ht : ∀ (x : α), x ∈ t
hn : Fintype.card α = n
⊢ ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n

Tactic:
⟨t, eq_univ_iff_forall.2 ht, hn⟩

Premises used: Iff.mpr, Set.eq_univ_iff_forall, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
t : Finset α
ht : ∀ (x : α), x ∈ t
hn : Fintype.card α = n
⊢ ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n

Tactic:
exact ⟨t, eq_univ_iff_forall.2 ht, hn⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
rw : Subsingleton.{u + 1} (↑s : Type u) ∧ Nonempty.{u + 1} (↑s : Type u) ↔ ∃ (x : α), s = {x}
rw₁ : Subsingleton.{u + 1} (↑s : Type u) ∧ Nonempty.{u + 1} (↑s : Type u) ↔ s.Nonempty ∧ s.Subsingleton
rw₂ : Subsingleton.{u + 1} (↑s : Type u) ∧ s.Nonempty ↔ s.Nonempty ∧ s.Subsingleton
rw₃ : s.Subsingleton ∧ s.Nonempty ↔ s.Nonempty ∧ s.Subsingleton
rw₄ rw₅ : s.Nonempty ∧ s.Subsingleton ↔ s.Nonempty ∧ s.Subsingleton
⊢ #(↑s : Type u) = 1 ↔ ∃ (x : α), s = {x}

Tactic:
rw [eq_one_iff_unique, Set.exists_eq_singleton_iff_nonempty_subsingleton,
    Set.nonempty_coe_sort, Set.subsingleton_coe, and_comm]

Premises used: Set.nonempty_coe_sort, and_comm, Cardinal.eq_one_iff_unique, Set.exists_eq_singleton_iff_nonempty_subsingleton, Set.subsingleton_coe
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
⊢ #(↑(S ∪ T) : Type u) + #(↑(S ∩ T) : Type u) = #(↑S : Type u) + #(↑T : Type u)

Tactic:
Quot.sound ⟨Equiv.Set.unionSumInter S T⟩

Premises used: Quot.sound, Cardinal, Quotient.map₂, Nonempty.intro, Quotient, Cardinal.map₂, Equiv.Set.unionSumInter
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
⊢ #(↑(S ∪ T) : Type u) + #(↑(S ∩ T) : Type u) = #(↑S : Type u) + #(↑T : Type u)

Tactic:
exact Quot.sound ⟨Equiv.Set.unionSumInter S T⟩

Premises used: Quot.sound
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
⊢ #(↑(S ∪ T) : Type u) + #(↑(S ∩ T) : Type u) = #(↑S : Type u) + #(↑T : Type u)

Tactic:
classical
  exact Quot.sound ⟨Equiv.Set.unionSumInter S T⟩

Premises used: Quot.sound
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
⊢ #(↑(S ∪ T) : Type u) ≤ #(↑S : Type u) + #(↑T : Type u)

Tactic:
@mk_union_add_mk_inter α S T ▸ self_le_add_right #(S ∪ T : Set α) #(S ∩ T : Set α)

Premises used: self_le_add_right, Cardinal.mk_union_add_mk_inter, Cardinal.mk, Eq.rec, Set.Elem, Inter.inter, Union.union
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
H : Disjoint S T
⊢ #(↑(S ∪ T) : Type u) = #(↑S : Type u) + #(↑T : Type u)

Tactic:
Quot.sound ⟨Equiv.Set.union H⟩

Premises used: Equiv.Set.union, Quot.sound, Cardinal, Cardinal.mk, Quotient.map₂, Nonempty.intro, Quotient, Quotient.mk', Cardinal.map₂
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
H : Disjoint S T
⊢ #(↑(S ∪ T) : Type u) = #(↑S : Type u) + #(↑T : Type u)

Tactic:
exact Quot.sound ⟨Equiv.Set.union H⟩

Premises used: Quot.sound
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
H : Disjoint S T
⊢ #(↑(S ∪ T) : Type u) = #(↑S : Type u) + #(↑T : Type u)

Tactic:
classical
  exact Quot.sound ⟨Equiv.Set.union H⟩

Premises used: Quot.sound
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
a : α
h : a ∉ s
rw : Disjoint s {a}
⊢ #(↑(insert a s) : Type u) = #(↑s : Type u) + 1

Tactic:
rw [← union_singleton, mk_union_of_disjoint, mk_singleton]

Premises used: Cardinal.mk_union_of_disjoint, Cardinal.mk_singleton, Set.union_singleton
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ Disjoint s {a}

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
a : α
pos : ∀ (h : a ∈ s), #(↑(insert a s) : Type u) ≤ #(↑s : Type u) + 1
neg : ∀ (h : a ∉ s), #(↑(insert a s) : Type u) ≤ #(↑s : Type u) + 1
⊢ #(↑(insert a s) : Type u) ≤ #(↑s : Type u) + 1

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
a : α
h : a ∈ s
⊢ #(↑(insert a s) : Type u) ≤ #(↑s : Type u) + 1

Tactic:
simp only [insert_eq_of_mem h, self_le_add_right]

Premises used: self_le_add_right, Set.insert_eq_of_mem
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
a : α
h : a ∉ s
neg neg₁ : #(↑s : Type u) + 1 ≤ #(↑s : Type u) + 1
⊢ #(↑(insert a s) : Type u) ≤ #(↑s : Type u) + 1

Tactic:
rw [mk_insert h]

Premises used: Cardinal.mk_insert
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
s : Set α
⊢ #(↑s : Type u_1) + #(↑sᶜ : Type u_1) = #α

Tactic:
mk_congr (Equiv.Set.sumCompl s)

Premises used: Cardinal.mk, Equiv.Set.sumCompl, Quotient.map₂, Quotient.mk', Cardinal.map₂, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
s : Set α
⊢ #(↑s : Type u_1) + #(↑sᶜ : Type u_1) = #α

Tactic:
exact mk_congr (Equiv.Set.sumCompl s)

Premises used: Equiv.Set.sumCompl, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
s : Set α
⊢ #(↑s : Type u_1) + #(↑sᶜ : Type u_1) = #α

Tactic:
classical
  exact mk_congr (Equiv.Set.sumCompl s)
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
t : Set α
H : #(↑t : Type u) ≤ (↑n : Cardinal.{u})
s : Finset α
hs : (↑s : Set α) ⊆ t
⊢ s.card ≤ n

Tactic:
simpa using (mk_le_mk_of_subset hs).trans H

Premises used: Cardinal.mk_le_mk_of_subset, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
t : Set α
refine : ∀ (H : ∀ (s : Finset α), (↑s : Set α) ⊆ t → s.card ≤ n), #(↑t : Type u) ≤ (↑n : Cardinal.{u})
⊢ #(↑t : Type u) ≤ (↑n : Cardinal.{u}) ↔ ∀ (s : Finset α), (↑s : Set α) ⊆ t → s.card ≤ n

Tactic:
refine ⟨fun H s hs ↦ by simpa using (mk_le_mk_of_subset hs).trans H, fun H ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), (↑s : Set α) ⊆ t → s.card ≤ n
apply : ∀ (s : Finset (↑t : Type u)), s.card ≤ n
⊢ #(↑t : Type u) ≤ (↑n : Cardinal.{u})

Tactic:
apply card_le_of (fun s ↦ ?_)

Premises used: Cardinal.card_le_of
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), (↑s : Set α) ⊆ t → s.card ≤ n
s : Finset (↑t : Type u)
u : Finset α := Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ t)) s
⊢ u.card = s.card

Tactic:
have : u.card = s.card := Finset.card_image_of_injOn Subtype.coe_injective.injOn
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), (↑s : Set α) ⊆ t → s.card ≤ n
s : Finset (↑t : Type u)
u : Finset α := Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ t)) s
this : u.card = s.card
⊢ s.card ≤ n

Tactic:
grind
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), (↑s : Set α) ⊆ t → s.card ≤ n
s : Finset (↑t : Type u)
let let₁ let₂ : s.card ≤ n
let₃ :
  let u := Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ t)) s;
  ∀ (this : u.card = s.card), s.card ≤ n
⊢ s.card ≤ n

Tactic:
classical
  let u : Finset α := s.image Subtype.val
  have : u.card = s.card := Finset.card_image_of_injOn Subtype.coe_injective.injOn
  grind
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
⊢ #{ x : α // p x } ≤ #{ x : α // q x }

Tactic:
⟨embeddingOfSubset _ _ h⟩

Premises used: Nonempty.intro, Set.embeddingOfSubset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
have : ∀ (this : Fintype (↑A : Type u)), #(↑A : Type u) < #(↑B : Type u)
⊢ #(↑A : Type u) < #(↑B : Type u)

Tactic:
have : Fintype A := (hfin.subset hlt.subset).fintype
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
this : Fintype (↑A : Type u)
have : ∀ (this : Fintype (↑B : Type u)), #(↑A : Type u) < #(↑B : Type u)
⊢ #(↑A : Type u) < #(↑B : Type u)

Tactic:
have : Fintype B := hfin.fintype
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
this_1 : Fintype (↑A : Type u)
this : Fintype (↑B : Type u)
⊢ #(↑A : Type u) < #(↑B : Type u)

Tactic:
simpa using Finset.card_lt_card <| Set.toFinset_ssubset_toFinset.mpr hlt

Premises used: Iff.mpr, Set.toFinset_ssubset_toFinset, Finset.card_lt_card
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
inl : ∀ (hfin : Finite.{u + 1} (↑B : Type u)), #(↑A : Type u) < #(↑B : Type u)
inr : ∀ (hinf : Infinite.{u + 1} (↑B : Type u)), #(↑A : Type u) < #(↑B : Type u)
⊢ #(↑A : Type u) < #(↑B : Type u)

Tactic:
rcases finite_or_infinite B with hfin | hinf

Premises used: finite_or_infinite, Set.Elem
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
A B : Set α
hfin_1 : A.Finite
hlt : A ⊂ B
hfin : Finite.{u + 1} (↑B : Type u)
⊢ #(↑A : Type u) < #(↑B : Type u)

Tactic:
card_lt_card_of_right_finite hfin hlt

Premises used: Cardinal.card_lt_card_of_right_finite
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
A B : Set α
hfin_1 : A.Finite
hlt : A ⊂ B
hfin : Finite.{u + 1} (↑B : Type u)
⊢ #(↑A : Type u) < #(↑B : Type u)

Tactic:
exact card_lt_card_of_right_finite hfin hlt

Premises used: Cardinal.card_lt_card_of_right_finite
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
hinf : Infinite.{u + 1} (↑B : Type u)
⊢ #(↑A : Type u) < #(↑B : Type u)

Tactic:
(lt_aleph0_iff_subtype_finite.mpr hfin).trans_le <| Cardinal.aleph0_le_mk_iff.mpr hinf

Premises used: Iff.mpr, Set.Mem, Cardinal.aleph0_le_mk_iff, Cardinal.lt_aleph0_iff_subtype_finite, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
hinf : Infinite.{u + 1} (↑B : Type u)
⊢ #(↑A : Type u) < #(↑B : Type u)

Tactic:
exact (lt_aleph0_iff_subtype_finite.mpr hfin).trans_le <| Cardinal.aleph0_le_mk_iff.mpr hinf

Premises used: Iff.mpr, Cardinal.aleph0_le_mk_iff, Cardinal.lt_aleph0_iff_subtype_finite, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
inst : Finite α
⊢ StrictMono (α := Set α) (mk ∘ Elem)

Tactic:
fun _ s ↦ card_lt_card_of_right_finite s.toFinite

Premises used: StrictMono, Set.toFinite, Cardinal.card_lt_card_of_right_finite
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ StrictMonoOn (α := Set α) (mk ∘ Elem) {s : Set α | s.Finite}

Tactic:
fun _ _ _ ↦ card_lt_card_of_right_finite

Premises used: Set.Mem, setOf, Set.Finite, StrictMonoOn, Cardinal.card_lt_card_of_right_finite
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
⊢ #(↑S : Type u) ≤ #(↑(S \ T) : Type u) + #(↑T : Type u)

Tactic:
(mk_le_mk_of_subset <| subset_diff_union _ _).trans <| mk_union_le _ _

Premises used: Cardinal.mk_le_mk_of_subset, Set.subset_diff_union, LE.le.trans, Cardinal.mk_union_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
h : T ⊆ S
rw rw₁ : #(↑S : Type u) = #(↑S : Type u)
⊢ #(↑(S \ T ∪ T) : Type u) = #(↑S : Type u)

Tactic:
rw [diff_union_of_subset h]

Premises used: Set.diff_union_of_subset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
h : T ⊆ S
refine : Disjoint (S \ T) T
⊢ #(↑(S \ T) : Type u) + #(↑T : Type u) = #(↑S : Type u)

Tactic:
refine (mk_union_of_disjoint <| ?_).symm.trans <| by rw [diff_union_of_subset h]

Premises used: Cardinal.mk_union_of_disjoint, Eq.symm, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
h : T ⊆ S
⊢ Disjoint (S \ T) T

Tactic:
disjoint_sdiff_self_left

Premises used: disjoint_sdiff_self_left