awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
refine_2 : prod f = lift.{u, v} (∏ i ∈ ∅, f i)
refine_2₁ : prod f = lift.{u, v} 1
refine_2₂ : prod f = 1
refine_2₃ : #((i : PEmpty.{u + 1}) → Quotient.out (f i)) = 1
refine_2₄ refine_2₅ : Eq (α := Cardinal.{max u v}) 1 1
⊢ prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)

Tactic:
rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]

Premises used: Finset.prod_empty, Fintype.univ_pempty, Cardinal.prod, Cardinal.lift_one, Cardinal.mk_eq_one
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α_1 : Type u
h_1 : Fintype α_1
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : Option α → Cardinal.{v}
refine_3 :
  (lift.{u, v} (f none) * prod.{u, v} fun (i : α) ↦ lift.{v, v} (f (some i))) =
    lift.{u, v} (f none) * prod.{u, v} fun (a : α) ↦ f (some a)
⊢ prod f = lift.{u, v} (∏ i : Option α, f i)

Tactic:
rw [Cardinal.prod, mk_congr Equiv.piOptionEquivProd, mk_prod, lift_umax.{v, u}, mk_out, ←
        Cardinal.prod, lift_prod, Fintype.prod_option, lift_mul, ← h fun a => f (some a)]

Premises used: Fintype.prod_option, Cardinal.mk_out, Cardinal.lift_prod, Equiv.piOptionEquivProd, Option.some, Cardinal.lift_mul, Cardinal.prod, Cardinal.mk_congr, Cardinal.mk_prod
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α_1 : Type u
h_1 : Fintype α_1
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : Option α → Cardinal.{v}
⊢ (lift.{u, v} (f none) * prod.{u, v} fun (i : α) ↦ lift.{v, v} (f (some i))) =
    lift.{u, v} (f none) * prod.{u, v} fun (a : α) ↦ f (some a)

Tactic:
simp only [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ #α ≤ 1 ↔ Subsingleton α

Tactic:
⟨fun ⟨f⟩ => ⟨fun _ _ => f.injective (Subsingleton.elim _ _)⟩, fun ⟨h⟩ =>
    ⟨fun _ => ULift.up 0, fun _ _ _ => h _ _⟩⟩

Premises used: _private.0.Cardinal.le_one_iff_subsingleton.match_2, Cardinal.mk, Function.Embedding.mk, LE.le, Nonempty.intro, Subsingleton.intro, Iff.intro, Function.Embedding.injective, Subsingleton, Subsingleton.elim, OfNat.ofNat, ULift.up, DFunLike.coe, _private.0.Cardinal.le_one_iff_subsingleton.match_1
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
⊢ #(↑s : Type u) ≤ 1 ↔ s.Subsingleton

Tactic:
le_one_iff_subsingleton.trans s.subsingleton_coe

Premises used: Cardinal.le_one_iff_subsingleton, Iff.trans, Set.subsingleton_coe
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
rw : ¬#α ≤ 1 ↔ Nontrivial α
rw₁ : ¬Subsingleton α ↔ Nontrivial α
rw₂ : ¬¬Nontrivial α ↔ Nontrivial α
rw₃ rw₄ : Nontrivial α ↔ Nontrivial α
⊢ 1 < #α ↔ Nontrivial α

Tactic:
rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, Classical.not_not]

Premises used: not_le, Classical.not_not, Cardinal.le_one_iff_subsingleton, not_nontrivial_iff_subsingleton
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
⊢ sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
refine_1 : ∀ (h : sInf s = 0), s = ∅ ∨ ∃ a ∈ s, a = 0
refine_2 : ∀ (h : s = ∅ ∨ ∃ a ∈ s, a = 0), sInf s = 0
⊢ sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
h : sInf s = 0
refine_1 :
  ∀ (h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (sInf ∅) 0),
    Eq.{u_1 + 2} (α := Set Cardinal.{u_1}) ∅ ∅ ∨
      ∃ (a : Cardinal.{u_1}), Membership.mem (γ := Set Cardinal.{u_1}) ∅ a ∧ a = 0
refine_1₁ : ∀ (hne : s.Nonempty), s = ∅ ∨ ∃ a ∈ s, a = 0
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (sInf ∅) 0
⊢ Eq.{u_1 + 2} (α := Set Cardinal.{u_1}) ∅ ∅ ∨
    ∃ (a : Cardinal.{u_1}), Membership.mem (γ := Set Cardinal.{u_1}) ∅ a ∧ a = 0

Tactic:
Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (sInf ∅) 0
⊢ Eq.{u_1 + 2} (α := Set Cardinal.{u_1}) ∅ ∅ ∨
    ∃ (a : Cardinal.{u_1}), Membership.mem (γ := Set Cardinal.{u_1}) ∅ a ∧ a = 0

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
h : sInf s = 0
hne : s.Nonempty
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
Or.inr ⟨sInf s, csInf_mem hne, h⟩

Premises used: csInf_mem, And.intro, Exists.intro, InfSet.sInf, Or.inr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
h : sInf s = 0
hne : s.Nonempty
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
exact Or.inr ⟨sInf s, csInf_mem hne, h⟩

Premises used: Or.inr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
h : s = ∅ ∨ ∃ a ∈ s, a = 0
refine_2 : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (sInf ∅) 0
refine_2₁ : ∀ (ha : 0 ∈ s), sInf s = 0
⊢ sInf s = 0

Tactic:
rcases h with rfl | ⟨a, ha, rfl⟩

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (sInf ∅) 0

Tactic:
Cardinal.sInf_empty

Premises used: Cardinal.sInf_empty
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (sInf ∅) 0

Tactic:
exact Cardinal.sInf_empty

Premises used: Cardinal.sInf_empty
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
ha : 0 ∈ s
⊢ sInf s = 0

Tactic:
eq_bot_iff.2 (csInf_le' ha)

Premises used: Iff.mpr, csInf_le', eq_bot_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
ha : 0 ∈ s
⊢ sInf s = 0

Tactic:
exact eq_bot_iff.2 (csInf_le' ha)

Premises used: Iff.mpr, csInf_le', eq_bot_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Sort u_1
f : ι → Cardinal.{u_2}
⊢ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (⨅ (i : ι), f i) 0 ↔ IsEmpty ι ∨ ∃ (i : ι), f i = 0

Tactic:
simp [iInf, sInf_eq_zero_iff]

Premises used: iInf, Cardinal.sInf_eq_zero_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Sort u_1
f : ι → Cardinal.{u_2}
inst : IsEmpty ι
⊢ iSup f = 0

Tactic:
ciSup_of_empty f

Premises used: ciSup_of_empty
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{v}
inl : lift.{u, v} (sInf ∅) = sInf (lift.{u, v} '' ∅)
inr : ∀ (hs : s.Nonempty), lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ lift.{u, v} (sInf ∅) = sInf (lift.{u, v} '' ∅)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{v}
hs : s.Nonempty
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Tactic:
lift_monotone.map_csInf hs

Premises used: Cardinal.lift_monotone, Monotone.map_csInf
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{v}
hs : s.Nonempty
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Tactic:
exact lift_monotone.map_csInf hs

Premises used: Cardinal.lift_monotone, Monotone.map_csInf
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ lift.{u, v} (sInf (range f)) = sInf (lift.{u, v} '' range f)

Tactic:
lift_sInf (range f)

Premises used: Cardinal.lift_sInf, Set.range
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Sort u_1
f : ι → Cardinal.{v}
h : (range fun (i : ι) ↦ lift.{u, v} (f i)) = lift.{u, v} '' range f
⊢ lift.{u, v} (sInf (range f)) = sInf (range fun (i : ι) ↦ lift.{u, v} (f i))

Tactic:
convert! lift_sInf (range f)

Premises used: Cardinal.lift_sInf, Set.range
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Sort u_1
f : ι → Cardinal.{v}
h : (range fun (i : ι) ↦ (lift.{u, v} ∘ f) i) = lift.{u, v} '' range f
⊢ (range fun (i : ι) ↦ lift.{u, v} (f i)) = lift.{u, v} '' range f

Tactic:
simp_rw [← comp_apply (f := lift), range_comp]

Premises used: Set.range_comp, Function.comp_apply
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
a : Cardinal.{u}
rw : Small.{u, u + 1} (↑(Iic #(Quotient.out a)) : Type (u + 1))
⊢ Small.{u, u + 1} (↑(Iic a) : Type (u + 1))

Tactic:
rw [← mk_out a]

Premises used: Cardinal.mk_out
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
a : Cardinal.{u}
apply :
  Surjective (β := (↑(Iic #(Quotient.out a)) : Type (u + 1))) fun (x : Set (Quotient.out a)) ↦
    Subtype.mk (p := fun (x : Cardinal.{u}) ↦ x ∈ Iic #(Quotient.out a)) #(↑x : Type u) ⋯
⊢ Small.{u, u + 1} (↑(Iic #(Quotient.out a)) : Type (u + 1))

Tactic:
apply @small_of_surjective (Set a.out) (Iic #a.out) _ fun x => ⟨#x, mk_set_le x⟩

Premises used: small_of_surjective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
a x : Cardinal.{u}
hx : x ∈ Iic #(Quotient.out a)
⊢ ∃ (a_1 : Set (Quotient.out a)),
    (fun (x : Set (Quotient.out a)) ↦
          (Subtype.mk (p := fun (x : Cardinal.{u}) ↦ x ∈ Iic #(Quotient.out a)) #(↑x : Type u) ⋯ :
            { x : Cardinal.{u} // x ∈ Iic #(Quotient.out a) }))
        a_1 =
      Subtype.mk (p := fun (x : Cardinal.{u}) ↦ x ∈ Iic #(Quotient.out a)) x hx

Tactic:
simpa using le_mk_iff_exists_set.1 hx

Premises used: Cardinal.le_mk_iff_exists_set, Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
a : Cardinal.{u}
⊢ Small.{u, u + 1} (↑(Iio a) : Type (u + 1))

Tactic:
small_subset Iio_subset_Iic_self

Premises used: small_subset, Set.Iio_subset_Iic_self
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
a b : Cardinal.{u}
⊢ Small.{u, u + 1} (↑(Icc a b) : Type (u + 1))

Tactic:
small_subset Icc_subset_Iic_self

Premises used: Set.Icc_subset_Iic_self, small_subset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
a b : Cardinal.{u}
⊢ Small.{u, u + 1} (↑(Ico a b) : Type (u + 1))

Tactic:
small_subset Ico_subset_Iio_self

Premises used: Set.Ico_subset_Iio_self, small_subset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
a b : Cardinal.{u}
⊢ Small.{u, u + 1} (↑(Ioc a b) : Type (u + 1))

Tactic:
small_subset Ioc_subset_Iic_self

Premises used: Set.Ioc_subset_Iic_self, small_subset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
a b : Cardinal.{u}
⊢ Small.{u, u + 1} (↑(Ioo a b) : Type (u + 1))

Tactic:
small_subset Ioo_subset_Iio_self

Premises used: Set.Ioo_subset_Iio_self, small_subset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u}
ι : Type u
e : (↑s : Type (u + 1)) ≃ ι
h : (sum fun (x : ι) ↦ (↑((e.symm : (a : ι) → (↑s : Type (u + 1))) x) : Cardinal.{u})) ∈ upperBounds s
⊢ BddAbove s

Tactic:
use sum.{u, u} fun x ↦ e.symm x
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u}
ι : Type u
e : (↑s : Type (u + 1)) ≃ ι
a : Cardinal.{u}
ha : a ∈ s
⊢ a ≤ sum fun (x : ι) ↦ (↑((e.symm : (a : ι) → (↑s : Type (u + 1))) x) : Cardinal.{u})

Tactic:
simpa using le_sum (fun x ↦ e.symm x) (e ⟨a, ha⟩)

Premises used: Cardinal.le_sum, Subtype.mk, Equiv.symm, Subtype.val, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u}
h : Small.{u, u + 1} (↑s : Type (u + 1))
⊢ BddAbove s

Tactic:
bddAbove_iff_small.2 h

Premises used: Iff.mpr, Cardinal.bddAbove_iff_small
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Cardinal.{u}
⊢ BddAbove (range f)

Tactic:
bddAbove_of_small

Premises used: Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : BddAbove s
rw : ∀ (hs : Small.{u, u + 1} (↑s : Type (u + 1))), Small.{max u v, (max u v) + 1} (↑(f '' s) : Type ((max u v) + 1))
⊢ BddAbove (f '' s)

Tactic:
rw [bddAbove_iff_small] at hs ⊢

Premises used: Cardinal.bddAbove_iff_small
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
⊢ Small.{max u v, (max u v) + 1} (↑(f '' s) : Type ((max u v) + 1))

Tactic:
small_lift _

Premises used: small_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
⊢ Small.{max u v, (max u v) + 1} (↑(f '' s) : Type ((max u v) + 1))

Tactic:
exact small_lift _

Premises used: small_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
rw : BddAbove (g '' range f)
⊢ BddAbove (range (g ∘ f))

Tactic:
rw [range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (g '' range f)

Tactic:
bddAbove_image g hf

Premises used: Cardinal.bddAbove_image
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (g '' range f)

Tactic:
exact bddAbove_image g hf

Premises used: Cardinal.bddAbove_image
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ Small.{max u v, max (u + 1) (v + 1)} Cardinal.{max u v}

Tactic:
have := small_lift.{_, v} Cardinal.{max u v}
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : Small.{max u v, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ BddAbove (α := Cardinal.{max u v}) univ

Tactic:
rw [← small_univ_iff, ← bddAbove_iff_small] at this

Premises used: Cardinal.bddAbove_iff_small, small_univ_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : BddAbove (α := Cardinal.{max u v}) univ
⊢ False

Tactic:
not_bddAbove_univ this

Premises used: not_bddAbove_univ
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : BddAbove (α := Cardinal.{max u v}) univ
⊢ False

Tactic:
exact not_bddAbove_univ this

Premises used: not_bddAbove_univ
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
⊢ Uncountable Cardinal.{u}

Tactic:
Uncountable.of_not_small not_small_cardinal.{u}

Premises used: not_small_cardinal, Uncountable.of_not_small
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
f : ι → Cardinal.{v}
rw : (sum fun (i : ι) ↦ lift.{max u v, v} (f i)) ≤ sum fun (x : ι) ↦ ⨆ (i : ι), lift.{u, v} (f i)
⊢ sum f ≤ lift.{v, u} #ι * ⨆ (i : ι), lift.{u, v} (f i)

Tactic:
rw [← (sum f).lift_id, lift_sum, ← lift_umax.{u, v}, ← (⨆ i, lift (f i)).lift_id,
    lift_umax.{max v u, u}, ← sum_const]

Premises used: iSup, Cardinal.lift, Cardinal.lift_sum, Cardinal.sum_const, Cardinal.lift_id, Cardinal.sum
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
f : ι → Cardinal.{v}
⊢ (sum fun (i : ι) ↦ lift.{max u v, v} (f i)) ≤ sum fun (x : ι) ↦ ⨆ (i : ι), lift.{u, v} (f i)

Tactic:
sum_le_sum _ _ fun i => ?_

Premises used: Cardinal.sum_le_sum
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
f : ι → Cardinal.{v}
refine : ∀ (i : ι), lift.{max u v, v} (f i) ≤ ⨆ (i : ι), lift.{u, v} (f i)
⊢ (sum fun (i : ι) ↦ lift.{max u v, v} (f i)) ≤ sum fun (x : ι) ↦ ⨆ (i : ι), lift.{u, v} (f i)

Tactic:
refine sum_le_sum _ _ fun i => ?_

Premises used: Cardinal.sum_le_sum
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
f : ι → Cardinal.{v}
i : ι
rw : lift.{u, v} (f i) ≤ ⨆ (i : ι), lift.{u, v} (f i)
⊢ lift.{max u v, v} (f i) ≤ ⨆ (i : ι), lift.{u, v} (f i)

Tactic:
rw [lift_umax.{v, u}]
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} (f i) ≤ ⨆ (i : ι), lift.{u, v} (f i)

Tactic:
le_ciSup bddAbove_of_small i

Premises used: le_ciSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} (f i) ≤ ⨆ (i : ι), lift.{u, v} (f i)

Tactic:
exact le_ciSup bddAbove_of_small i

Premises used: le_ciSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
⊢ sum f ≤ lift.{v, u} #ι * ⨆ (i : ι), f i

Tactic:
simpa [← lift_umax] using sum_le_lift_mk_mul_iSup_lift f

Premises used: Cardinal.lift_umax, Cardinal.sum_le_lift_mk_mul_iSup_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
f : ι → Cardinal.{u}
⊢ sum f ≤ #ι * ⨆ (i : ι), f i

Tactic:
simpa using sum_le_lift_mk_mul_iSup_lift f

Premises used: Cardinal.sum_le_lift_mk_mul_iSup_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
apply : ∀ (c : Cardinal.{max u_1 u}) (hc : c ∈ upperBounds (lift.{u, u_1} '' s)), lift.{u, u_1} (sSup s) ≤ c
apply₁ : lift.{u, u_1} (sSup s) ∈ upperBounds (lift.{u, u_1} '' s)
⊢ lift.{u, u_1} (sSup s) = sSup (lift.{u, u_1} '' s)

Tactic:
apply ((le_csSup_iff' (bddAbove_image.{_, u} _ hs)).2 fun c hc => _).antisymm (csSup_le' _)
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
hc : c ∈ upperBounds (lift.{u, u_1} '' s)
by_contra : ∀ (h : ¬lift.{u, u_1} (sSup s) ≤ c), False
⊢ lift.{u, u_1} (sSup s) ≤ c

Tactic:
by_contra h
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
hc : c ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬lift.{u, u_1} (sSup s) ≤ c
obtain :
  ∀ (d : Cardinal.{u_1}) (hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s))
    (h : ¬lift.{u, u_1} (sSup s) ≤ lift.{u, u_1} d), False
⊢ False

Tactic:
obtain ⟨d, rfl⟩ := Cardinal.mem_range_lift_of_le (not_le.1 h).le

Premises used: not_le, Cardinal.mem_range_lift_of_le, LT.lt.le, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬lift.{u, u_1} (sSup s) ≤ lift.{u, u_1} d
⊢ ¬sSup s ≤ d

Tactic:
simp_rw [lift_le] at h hc

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬sSup s ≤ d
⊢ ¬∀ x ∈ s, x ≤ d

Tactic:
rw [csSup_le_iff' hs] at h

Premises used: csSup_le_iff'
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬∀ x ∈ s, x ≤ d
⊢ False

Tactic:
h fun a ha => lift_le.1 <| hc (mem_image_of_mem _ ha)

Premises used: Cardinal.lift, Set.mem_image_of_mem, Iff.mp, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬∀ x ∈ s, x ≤ d
⊢ False

Tactic:
exact h fun a ha => lift_le.1 <| hc (mem_image_of_mem _ ha)

Premises used: Cardinal.lift, Set.mem_image_of_mem, Iff.mp, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
j : Cardinal.{u_1}
hj : j ∈ s
⊢ lift.{u, u_1} j ≤ lift.{u, u_1} (sSup s)

Tactic:
lift_le.2 (le_csSup hs hj)

Premises used: Iff.mpr, le_csSup, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
s : Set Cardinal.{u_1}
hs : BddAbove s
j : Cardinal.{u_1}
hj : j ∈ s
⊢ lift.{u, u_1} j ≤ lift.{u, u_1} (sSup s)

Tactic:
exact lift_le.2 (le_csSup hs hj)

Premises used: Iff.mpr, le_csSup, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
rw : sSup (range (lift.{u, w} ∘ f)) = sSup (range fun (i : ι) ↦ lift.{u, w} (f i))
⊢ lift.{u, w} (iSup f) = ⨆ (i : ι), lift.{u, w} (f i)

Tactic:
rw [iSup, iSup, lift_sSup hf, ← range_comp]

Premises used: Set.range_comp, iSup, Cardinal.lift_sSup
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ sSup (range (lift.{u, w} ∘ f)) = sSup (range fun (i : ι) ↦ lift.{u, w} (f i))

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
rw : ⨆ (i : ι), lift.{u, w} (f i) ≤ t
⊢ lift.{u, w} (iSup f) ≤ t

Tactic:
rw [lift_iSup hf]

Premises used: Cardinal.lift_iSup
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ ⨆ (i : ι), lift.{u, w} (f i) ≤ t

Tactic:
ciSup_le' w

Premises used: ciSup_le'
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ ⨆ (i : ι), lift.{u, w} (f i) ≤ t

Tactic:
exact ciSup_le' w

Premises used: ciSup_le'
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
rw : ⨆ (i : ι), lift.{u, w} (f i) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ lift.{u, w} (iSup f) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t

Tactic:
rw [lift_iSup hf]

Premises used: Cardinal.lift_iSup
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ ⨆ (i : ι), lift.{u, w} (f i) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t

Tactic:
ciSup_le_iff' (bddAbove_range_comp.{_, _, u} hf _)

Premises used: Quotient.map, Cardinal.lift, ciSup_le_iff', Cardinal.bddAbove_range_comp, Cardinal.map, Quot.map
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ ⨆ (i : ι), lift.{u, w} (f i) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t

Tactic:
exact ciSup_le_iff' (bddAbove_range_comp.{_, _, u} hf _)
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
rw : LE.le (α := Cardinal.{max w w'}) (⨆ (i : ι), lift.{w', w} (f i)) (⨆ (i : ι'), lift.{w, w'} (f' i))
⊢ lift.{w', w} (iSup f) ≤ lift.{w, w'} (iSup f')

Tactic:
rw [lift_iSup hf, lift_iSup hf']

Premises used: Cardinal.lift_iSup
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ LE.le (α := Cardinal.{max w w'}) (⨆ (i : ι), lift.{w', w} (f i)) (⨆ (i : ι'), lift.{w, w'} (f' i))

Tactic:
ciSup_mono_of_forall_exists' (bddAbove_range_comp.{_, _, w} hf' _) fun i => ⟨_, h i⟩

Premises used: Cardinal.bddAbove_range_comp, Exists.intro, ciSup_mono_of_forall_exists'
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ LE.le (α := Cardinal.{max w w'}) (⨆ (i : ι), lift.{w', w} (f i)) (⨆ (i : ι'), lift.{w, w'} (f' i))

Tactic:
exact ciSup_mono_of_forall_exists' (bddAbove_range_comp.{_, _, w} hf' _) fun i => ⟨_, h i⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type v
ι' : Type v'
f : ι → Cardinal.{v}
f' : ι' → Cardinal.{v'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{v', v} (f i) ≤ lift.{v, v'} (f' (g i))
⊢ lift.{v', v} (iSup f) ≤ lift.{v, v'} (iSup f')

Tactic:
lift_iSup_le_lift_iSup hf hf' h

Premises used: Cardinal.lift_iSup_le_lift_iSup
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
rw : ⨆ (i : ι), lift.{u, v} (f i) ≤ sum f
⊢ lift.{u, v} (⨆ (i : ι), f i) ≤ sum f

Tactic:
rw [lift_iSup bddAbove_of_small]

Premises used: Cardinal.lift_iSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
⊢ ⨆ (i : ι), lift.{u, v} (f i) ≤ sum f

Tactic:
ciSup_le' fun i => lift_le_sum f i

Premises used: ciSup_le', Cardinal.lift_le_sum
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
⊢ ⨆ (i : ι), lift.{u, v} (f i) ≤ sum f

Tactic:
exact ciSup_le' fun i => lift_le_sum f i

Premises used: ciSup_le', Cardinal.lift_le_sum