awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
I1 : s.card ≤ u.card
h : (↑u.card : Cardinal.{u}) = #(↑(f i) : Type u)
⊢ LE.le.{u + 1} (α := Cardinal.{u}) (↑u.card : Cardinal.{u}) (↑n : Cardinal.{u})

Tactic:
convert! h'f i
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
I1 : s.card ≤ u.card
⊢ (↑u.card : Cardinal.{u}) = #(↑(f i) : Type u)

Tactic:
simp only [u, Set.toFinset_card, mk_fintype]

Premises used: Set.toFinset_card, Cardinal.mk_fintype
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
I1 : s.card ≤ u.card
⊢ LE.le.{u + 1} (α := Cardinal.{u}) (↑u.card : Cardinal.{u}) (↑n : Cardinal.{u})

Tactic:
have I2 : (u.card : Cardinal) ≤ n := by
      convert! h'f i; simp only [u, Set.toFinset_card, mk_fintype]
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
I1 : s.card ≤ u.card
I2 : LE.le.{u + 1} (α := Cardinal.{u}) (↑u.card : Cardinal.{u}) (↑n : Cardinal.{u})
⊢ s.card ≤ n

Tactic:
I1.trans (Nat.cast_le.1 I2)

Premises used: Iff.mp, Nat.cast_le, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
I1 : s.card ≤ u.card
I2 : LE.le.{u + 1} (α := Cardinal.{u}) (↑u.card : Cardinal.{u}) (↑n : Cardinal.{u})
⊢ s.card ≤ n

Tactic:
exact I1.trans (Nat.cast_le.1 I2)

Premises used: Iff.mp, Nat.cast_le, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
x : α
hx : x ∈ t
⊢ ∃ (i : ι), x ∈ f i

Tactic:
(ht x hx).exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
x : α
hx : x ∈ t
obtain : ∀ (i : ι) (hi : x ∈ f i), Membership.mem (γ := Set α) (⋃ (i : ι), f i) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), f i) x

Tactic:
obtain ⟨i, hi⟩ : ∃ i, x ∈ f i := (ht x hx).exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
x : α
hx : x ∈ t
i : ι
hi : x ∈ f i
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), f i) x

Tactic:
mem_iUnion_of_mem i hi

Premises used: Set.mem_iUnion_of_mem
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
x : α
hx : x ∈ t
i : ι
hi : x ∈ f i
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), f i) x

Tactic:
exact mem_iUnion_of_mem i hi

Premises used: Set.mem_iUnion_of_mem
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
⊢ t ⊆ ⋃ (i : ι), f i

Tactic:
have : t ⊆ ⋃ i, f i := by
      intro x hx
      obtain ⟨i, hi⟩ : ∃ i, x ∈ f i := (ht x hx).exists
      exact mem_iUnion_of_mem i hi
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
⊢ #(↑t : Type u) ≤ #(↑(⋃ (i : ι), f i) : Type u)

Tactic:
mk_le_mk_of_subset this

Premises used: Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
⊢ #(↑(⋃ (i : ι), f i) : Type u) ≤ sum fun (i : ι) ↦ #(↑(f i) : Type u)

Tactic:
mk_iUnion_le_sum_mk

Premises used: Cardinal.mk_iUnion_le_sum_mk
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
⊢ (sum fun (i : ι) ↦ #(↑(f i) : Type u)) ≤ sum fun (x : ι) ↦ a

Tactic:
sum_le_sum _ _ h'f

Premises used: Cardinal.sum_le_sum
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
⊢ (sum fun (x : ι) ↦ a) = #ι * a

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
grw grw₁ : ℵ₀ * a ≤ ℵ₀ * a
⊢ #ι * a ≤ ℵ₀ * a

Tactic:
grw [mk_le_aleph0]

Premises used: Cardinal.mk_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
⊢ ℵ₀ * a = a

Tactic:
aleph0_mul_eq ha

Premises used: Cardinal.aleph0_mul_eq
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ (i : ι), f i
calc : (sum fun (x : ι) ↦ a) = #ι * a
calc₁ : #ι * a ≤ ℵ₀ * a
⊢ #(↑t : Type u) ≤ a

Tactic:
calc #t ≤ #(⋃ i, f i) := mk_le_mk_of_subset this
      _ ≤ sum (fun i ↦ #(f i)) := mk_iUnion_le_sum_mk
      _ ≤ sum (fun _ ↦ a) := sum_le_sum _ _ h'f
      _ = #ι * a := by simp
      _ ≤ ℵ₀ * a := by grw [mk_le_aleph0]
      _ = a := aleph0_mul_eq ha

Premises used: Cardinal.mk, Cardinal.mk_iUnion_le_sum_mk, Set.Elem, Cardinal.sum_le_sum, Cardinal.aleph0_mul_eq, Cardinal.mk_le_mk_of_subset, Set.iUnion, Cardinal.sum
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun (x : Set α) ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
this : #(↑(ULift.down ⁻¹' t) : Type (max u v)) ≤ lift.{v, u} a
⊢ #(↑t : Type u) ≤ a

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun (x : Set α) ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
suffices : #(↑(ULift.down ⁻¹' t) : Type (max u v)) ≤ lift.{v, u} a
⊢ #(↑t : Type u) ≤ a

Tactic:
suffices #(ULift.down.{v} ⁻¹' t) ≤ Cardinal.lift.{v, u} a by simpa
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun (x : Set α) ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift.{u, v} ι) := Filter.map ULift.up l
ht₁ : ∀ x ∈ ULift.down ⁻¹' t, ∀ᶠ (i : ULift.{u, v} ι) in l', x ∈ g i
h'f₁ : ∀ (i : ULift.{u, v} ι), #(↑(g i) : Type (max u v)) ≤ lift.{v, u} a
⊢ #(↑(ULift.down ⁻¹' t) : Type (max u v)) ≤ lift.{v, u} a

Tactic:
apply mk_subtype_le_of_countable_eventually_mem_aux (ι := ULift.{u} ι) (l := l') (f := g)
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun (x : Set α) ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift.{u, v} ι) := Filter.map ULift.up l
x : ULift.{v, u} α
hx : x ∈ ULift.down ⁻¹' t
⊢ ∀ᶠ (i : ULift.{u, v} ι) in l', x ∈ g i

Tactic:
simpa only [Function.comp_apply, mem_preimage, eventually_map] using ht _ hx

Premises used: Filter.eventually_map, Function.comp_apply, Set.mem_preimage
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun (x : Set α) ↦ ULift.down ⁻¹' x) ∘ f ∘ ULift.down
l' : Filter (ULift.{u, v} ι) := Filter.map ULift.up l
i : ULift.{u, v} ι
⊢ #(↑(g i) : Type (max u v)) ≤ lift.{v, u} a

Tactic:
simpa [g] using h'f i.down

Premises used: ULift.down
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
rw : #(↑Set.univ : Type u) ≤ a
⊢ #α ≤ a

Tactic:
rw [← mk_univ]

Premises used: Cardinal.mk_univ
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
⊢ #(↑Set.univ : Type u) ≤ a

Tactic:
mk_subtype_le_of_countable_eventually_mem (l := l) (fun x _ ↦ ht x) h'f

Premises used: Cardinal.mk_subtype_le_of_countable_eventually_mem
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
⊢ #(↑Set.univ : Type u) ≤ a

Tactic:
exact mk_subtype_le_of_countable_eventually_mem (l := l) (fun x _ ↦ ht x) h'f

Premises used: Cardinal.mk_subtype_le_of_countable_eventually_mem
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) = a
a₁ : #α ≤ a
a₂ : a ≤ #α
⊢ #α = a

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) = a
⊢ #α ≤ a

Tactic:
apply mk_le_of_countable_eventually_mem ht (fun i ↦ (h'f i).le)

Premises used: Eq.le, Cardinal.mk_le_of_countable_eventually_mem
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) = a
⊢ Nonempty ι

Tactic:
nonempty_of_neBot l

Premises used: Filter.nonempty_of_neBot
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) = a
a₁ : ∀ (i : ι), a ≤ #α
⊢ a ≤ #α

Tactic:
obtain ⟨i⟩ : Nonempty ι := nonempty_of_neBot l

Premises used: Filter.nonempty_of_neBot, Nonempty
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) = a
i : ι
a₁ : #(↑(f i) : Type u) ≤ #α
⊢ a ≤ #α

Tactic:
rw [← (h'f i)]
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) = a
i : ι
⊢ #(↑(f i) : Type u) ≤ #α

Tactic:
mk_set_le (f i)

Premises used: Cardinal.mk_set_le
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α : Type u
ι : Type v
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) = a
i : ι
⊢ #(↑(f i) : Type u) ≤ #α

Tactic:
exact mk_set_le (f i)

Premises used: Cardinal.mk_set_le
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α β : Type u
⊢ CanLift Cardinal.{u} (Type u) mk fun (x : Cardinal.{u}) ↦ True

Tactic:
⟨fun c _ => Quot.inductionOn c fun α => ⟨α, rfl⟩⟩

Premises used: Quot.inductionOn, CanLift.mk
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
motive : Cardinal.{u_1} → Prop
c : Cardinal.{u_1}
mk : ∀ (α : Type u_1), motive #α
⊢ motive c

Tactic:
Quotient.inductionOn c mk

Premises used: Quotient.inductionOn
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
motive : Cardinal.{u_1} → Cardinal.{u_2} → Prop
c₁ : Cardinal.{u_1}
c₂ : Cardinal.{u_2}
mk : ∀ (α : Type u_1) (β : Type u_2), motive #α #β
⊢ motive c₁ c₂

Tactic:
Quotient.inductionOn₂ c₁ c₂ mk

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
motive : Cardinal.{u_1} → Cardinal.{u_2} → Cardinal.{u_3} → Prop
c₁ : Cardinal.{u_1}
c₂ : Cardinal.{u_2}
c₃ : Cardinal.{u_3}
mk : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), motive #α #β #γ
⊢ motive c₁ c₂ c₃

Tactic:
Quotient.inductionOn₃ c₁ c₂ c₃ mk

Premises used: Quotient.inductionOn₃
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u_1
motive : (ι → Cardinal.{v}) → Prop
f : ι → Cardinal.{v}
mk : ∀ (f : ι → Type v), motive fun (i : ι) ↦ #(f i)
⊢ motive f

Tactic:
Quotient.induction_on_pi f mk

Premises used: Quotient.induction_on_pi
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α β : Type u
⊢ #α = #β ↔ Nonempty.{max 1 (u + 1)} (α ≃ β)

Tactic:
Quotient.eq'

Premises used: Cardinal, Cardinal.mk, Quotient.eq'
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
c : Cardinal.{u_1}
⊢ #(Quotient.out c) = c

Tactic:
Quotient.out_eq _

Premises used: Cardinal, Cardinal.mk, Quotient.mk', Quotient.out_eq
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α_1 β : Type u
α : Type v
⊢ #(Quotient.out #α) = #α

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α β : Type u
e : α ≃ β
⊢ #α = #β

Tactic:
Quot.sound ⟨e⟩

Premises used: Quot.sound, Cardinal, Cardinal.mk, Nonempty.intro, Quotient, Quotient.mk'
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
f : Type u → Type v
hf : (α β : Type u) → α ≃ β → f α ≃ f β
α : Type u
⊢ map f hf #α = #(f α)

Tactic:
rfl

Premises used: Cardinal.mk, Quotient.mk', rfl
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
⊢ #(ULift.{v, u} α) = lift.{v, u} #α

Tactic:
rfl

Premises used: Quotient.map, Cardinal.lift, Cardinal.map, Quot.map, rfl
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ lift.{max u v, u} = lift.{v, u}

Tactic:
funext fun a => inductionOn a fun _ => (Equiv.ulift.trans Equiv.ulift.symm).cardinal_eq

Premises used: funext, Cardinal.inductionOn
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a : Cardinal.{max u v}
⊢ lift.{u, max u v} a = a

Tactic:
inductionOn a fun _ => mk_congr Equiv.ulift

Premises used: Cardinal.inductionOn
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a : Cardinal.{u}
⊢ lift.{u, u} a = a

Tactic:
lift_id'.{u, u} a

Premises used: Cardinal.lift_id'
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a : Cardinal.{u}
⊢ lift.{0, u} a = a

Tactic:
lift_id'.{0, u} a

Premises used: Cardinal.lift_id'
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a : Cardinal.{u_1}
⊢ lift.{w, max v u_1} (lift.{v, u_1} a) = lift.{max v w, u_1} a

Tactic:
inductionOn a fun _ => (Equiv.ulift.trans <| Equiv.ulift.trans Equiv.ulift.symm).cardinal_eq

Premises used: Cardinal.inductionOn
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a : Cardinal.{u}
rw : Nonempty (Quotient.out #(ULift.{v, u} (Quotient.out a)) ≃ Quotient.out a)
⊢ Nonempty (Quotient.out (lift.{v, u} a) ≃ Quotient.out a)

Tactic:
rw [← mk_out a, ← mk_uLift, mk_out]

Premises used: Cardinal.mk_out, Cardinal.mk_uLift
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a : Cardinal.{u}
⊢ Nonempty (Quotient.out #(ULift.{v, u} (Quotient.out a)) ≃ Quotient.out a)

Tactic:
⟨outMkEquiv.trans Equiv.ulift⟩

Premises used: Equiv.trans, Equiv.ulift, Cardinal.outMkEquiv, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a : Cardinal.{u}
⊢ Nonempty (Quotient.out #(ULift.{v, u} (Quotient.out a)) ≃ Quotient.out a)

Tactic:
exact ⟨outMkEquiv.trans Equiv.ulift⟩
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
β : Type v
⊢ lift.{max v w, u} #α = lift.{max u w, v} #β ↔ Nonempty (α ≃ β)

Tactic:
Quotient.eq'.trans
    ⟨fun ⟨f⟩ => ⟨Equiv.ulift.symm.trans <| f.trans Equiv.ulift⟩, fun ⟨f⟩ =>
      ⟨Equiv.ulift.trans <| f.trans Equiv.ulift.symm⟩⟩

Premises used: _private.0.Cardinal.lift_mk_eq.match_2, Cardinal, Equiv.trans, ULift, Quotient.map, Cardinal.lift, Equiv.ulift, Equiv, Quotient.eq', Nonempty.intro, Cardinal.map, _private.0.Cardinal.lift_mk_eq.match_1, Iff.intro, Quot.map, Iff.trans, Nonempty, Equiv.symm, Setoid.r
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
β : Type v
⊢ lift.{v, u} #α = lift.{u, v} #β ↔ Nonempty (α ≃ β)

Tactic:
lift_mk_eq.{u, v, 0}

Premises used: Cardinal.lift_mk_eq
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
β : Type v
e : α ≃ β
⊢ lift.{v, u} #α = lift.{u, v} #β

Tactic:
lift_mk_eq'.2 ⟨e⟩

Premises used: Iff.mpr, Cardinal.lift_mk_eq', Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
inst : IsEmpty α
⊢ #α = 0

Tactic:
(Equiv.equivOfIsEmpty α (ULift (Fin 0))).cardinal_eq

Premises used: Equiv.equivOfIsEmpty, ULift, Quotient.map, Cardinal.lift, Cardinal.mk, Cardinal.map, Quotient.mk', Quot.map, OfNat.ofNat, Fin, Equiv.cardinal_eq
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ lift.{u_2, u_1} 0 = 0

Tactic:
mk_eq_zero _

Premises used: Cardinal.mk_eq_zero, Quotient.map, Cardinal.lift, Cardinal.map, Quot.map
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
⊢ #α = 0 ↔ IsEmpty α

Tactic:
⟨fun e =>
    let ⟨h⟩ := Quotient.exact e
    h.isEmpty,
    @mk_eq_zero α⟩

Premises used: Cardinal.mk_eq_zero, IsEmpty, Equiv.isEmpty, _private.0.Cardinal.mk_eq_zero_iff.match_1, Iff.intro, Quotient.exact
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
⊢ #α ≠ 0 ↔ Nonempty α

Tactic:
(not_iff_not.2 mk_eq_zero_iff).trans not_isEmpty_iff

Premises used: not_iff_not, Iff.mpr, Cardinal.mk_eq_zero_iff, not_isEmpty_iff, Iff.trans
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
inst : Nonempty α
⊢ #α ≠ 0

Tactic:
mk_ne_zero_iff.2 ‹_›

Premises used: Iff.mpr, Cardinal.mk_ne_zero_iff
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
x : Cardinal.{u_1}
h : x ≠ 0
rwa : #(Quotient.out x) ≠ 0
rwa₁ rwa₂ rwa₃ rwa₄ : x ≠ 0
⊢ Nonempty.{u_1 + 1} (Quotient.out x)

Tactic:
rwa [← mk_ne_zero_iff, mk_out]

Premises used: Cardinal.mk_ne_zero_iff, Cardinal.mk_out
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α β : Type u
⊢ Nontrivial Cardinal.{u}

Tactic:
⟨⟨1, 0, mk_ne_zero _⟩⟩

Premises used: Nontrivial.mk, Exists.intro, Cardinal.mk_ne_zero, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
inst : Subsingleton α
inst_1 : Nonempty α
⊢ #α = 1

Tactic:
let ⟨_⟩ := nonempty_unique α; (Equiv.ofUnique α (ULift (Fin 1))).cardinal_eq

Premises used: ULift, Cardinal.mk, nonempty_unique, Equiv.ofUnique, _private.0.Cardinal.mk_eq_one.match_1, OfNat.ofNat, Fin, Eq, Equiv.cardinal_eq
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α β : Type u
⊢ #α + #β = #(α ⊕ β)

Tactic:
rfl

Premises used: Cardinal.mk, Quotient.map₂, Quotient.mk', Cardinal.map₂, rfl
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
β : Type v
⊢ #(α ⊕ β) = lift.{v, u} #α + lift.{u, v} #β

Tactic:
mk_congr (Equiv.ulift.symm.sumCongr Equiv.ulift.symm)

Premises used: Cardinal.mk, Equiv.ulift, Quotient.map₂, Equiv.sumCongr, Quotient.mk', Cardinal.map₂, Equiv.symm, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
rw : #(α ⊕ PUnit) = #α + 1
rw₁ : lift.{u, u} #α + lift.{u, u} #PUnit = #α + 1
rw₂ : lift.{u, u} #α + lift.{u, u} 1 = #α + 1
rw₃ : #α + lift.{u, u} 1 = #α + 1
rw₄ rw₅ : #α + 1 = #α + 1
⊢ #(Option α) = #α + 1

Tactic:
rw [(Equiv.optionEquivSumPUnit.{u, u} α).cardinal_eq, mk_sum, mk_eq_one PUnit, lift_id, lift_id]

Premises used: PUnit, Cardinal.mk_sum, Cardinal.mk_eq_one, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
β : Type v
⊢ #(α ⊕' β) = lift.{v, u} #α + lift.{u, v} #β

Tactic:
(mk_congr (Equiv.psumEquivSum α β)).trans (mk_sum α β)

Premises used: Equiv.psumEquivSum, Cardinal.mk_sum, Cardinal.mk_congr, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α β : Type u
⊢ #α * #β = #(α × β)

Tactic:
rfl

Premises used: Cardinal.mk, Quotient.map₂, Quotient.mk', Cardinal.map₂, rfl
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
β : Type v
⊢ #(α × β) = lift.{v, u} #α * lift.{u, v} #β

Tactic:
mk_congr (Equiv.ulift.symm.prodCongr Equiv.ulift.symm)

Premises used: Cardinal.mk, Equiv.ulift, Quotient.map₂, Quotient.mk', Cardinal.map₂, Equiv.symm, Equiv.prodCongr, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α β : Type u
⊢ #α ^ #β = #(β → α)

Tactic:
rfl

Premises used: Cardinal.mk, Quotient.map₂, Quotient.mk', Cardinal.map₂, rfl
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α : Type u
β : Type v
⊢ #(α → β) = lift.{u, v} #β ^ lift.{v, u} #α

Tactic:
mk_congr (Equiv.ulift.symm.arrowCongr Equiv.ulift.symm)

Premises used: Equiv.arrowCongr, Cardinal.mk, Equiv.ulift, Quotient.map₂, Quotient.mk', Cardinal.map₂, Equiv.symm, Cardinal.mk_congr