awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
n : ℕ
a : Cardinal.{u}
rw : lift.{v, u} (↑n : Cardinal.{u}) < lift.{v, u} a ↔ (↑n : Cardinal.{u}) < a
rw₁ rw₂ : (↑n : Cardinal.{u}) < a ↔ (↑n : Cardinal.{u}) < a
⊢ (↑n : Cardinal.{max u v}) < lift.{v, u} a ↔ (↑n : Cardinal.{u}) < a

Tactic:
rw [← lift_natCast.{v, u}, lift_lt]

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
⊢ 0 < lift.{v, u} a ↔ 0 < a

Tactic:
simpa using nat_lt_lift_iff (n := 0)

Premises used: Cardinal.nat_lt_lift_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
⊢ 1 < lift.{v, u} a ↔ 1 < a

Tactic:
simpa using nat_lt_lift_iff (n := 1)

Premises used: Cardinal.nat_lt_lift_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n < lift.{v, u} a ↔ OfNat.ofNat n < a

Tactic:
nat_lt_lift_iff

Premises used: Cardinal.nat_lt_lift_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
s : Finset α
⊢ #↥s = (↑s.card : Cardinal.{u})

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u_1
s : Finset α
⊢ (↑s.card : Cardinal.{u_1}) ≤ #α

Tactic:
@mk_coe_finset _ s ▸ mk_set_le _

Premises used: Eq.rec, Cardinal.mk_coe_finset, Cardinal.mk_set_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
⊢ CharZero Cardinal.{u_1}

Tactic:
⟨fun a b h ↦ ?_⟩

Premises used: CharZero.mk
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
refine : ∀ (a b : ℕ) (h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑b : Cardinal.{u_1})), a = b
⊢ CharZero Cardinal.{u_1}

Tactic:
refine ⟨fun a b h ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
a b : ℕ
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑b : Cardinal.{u_1})
rwa : ∀ (h : lift.{u_1, 0} #(Fin a) = (↑b : Cardinal.{u_1})), a = b
rwa₁ : ∀ (h : lift.{u_1, 0} #(Fin a) = lift.{u_1, 0} #(Fin b)), a = b
rwa₂ : ∀ (h : #(Fin a) = #(Fin b)), a = b
rwa₃ : ∀ (h : Nonempty (Fin a ≃ Fin b)), a = b
rwa₄ : ∀ (h : Fintype.card (Fin a) = Fintype.card (Fin b)), a = b
rwa₅ : ∀ (h : a = Fintype.card (Fin b)), a = b
rwa₆ rwa₇ rwa₈ rwa₉ : ∀ (h : a = b), a = b
⊢ a = b

Tactic:
rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq,
    Fintype.card_fin, Fintype.card_fin] at h

Premises used: Fintype.card_fin, Fintype.card_eq, Cardinal.lift_mk_fin, Cardinal.lift_inj, Cardinal.eq
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #(↑(A j) : Type v) ≤ c
simp_rw :
  #(↑(sSup
            (range.{v, u + 1} (ι := o.ToType)
              ((fun (x : (↑(Iio o) : Type (u + 1))) ↦ A (↑x : Ordinal.{u})) ∘
                (⇑(OrderIso.symm ToType.mk) : (a : o.ToType) → (↑(Iio o) : Type (u + 1)))))) :
        Type v) ≤
    c
⊢ #(↑(⋃ (j : Ordinal.{u}), ⋃ (_ : j < o), A j) : Type v) ≤ c

Tactic:
simp_rw [← mem_Iio, biUnion_eq_iUnion, iUnion, iSup, ← ToType.mk.symm.surjective.range_comp]

Premises used: Set.mem_Iio, iSup, Function.Surjective.range_comp, OrderIso.surjective, OrderIso.symm, Ordinal.ToType.mk, Set.biUnion_eq_iUnion, Set.iUnion
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #(↑(A j) : Type v) ≤ c
rw :
  lift.{u, v}
      #(↑(sSup
              (range.{v, u + 1} (ι := o.ToType)
                ((fun (x : (↑(Iio o) : Type (u + 1))) ↦ A (↑x : Ordinal.{u})) ∘
                  (⇑(OrderIso.symm ToType.mk) : (a : o.ToType) → (↑(Iio o) : Type (u + 1)))))) :
          Type v) ≤
    lift.{u, v} c
⊢ #(↑(sSup
            (range.{v, u + 1} (ι := o.ToType)
              ((fun (x : (↑(Iio o) : Type (u + 1))) ↦ A (↑x : Ordinal.{u})) ∘
                (⇑(OrderIso.symm ToType.mk) : (a : o.ToType) → (↑(Iio o) : Type (u + 1)))))) :
        Type v) ≤
    c

Tactic:
rw [← lift_le.{u}]
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #(↑(A j) : Type v) ≤ c
apply :
  lift.{v, u} #o.ToType *
      ⨆ (i : o.ToType),
        lift.{u, v}
          #(↑(((fun (x : (↑(Iio o) : Type (u + 1))) ↦ A (↑x : Ordinal.{u})) ∘
                    (⇑(OrderIso.symm ToType.mk) : (a : o.ToType) → (↑(Iio o) : Type (u + 1))))
                  i) :
              Type v) ≤
    lift.{u, v} c * lift.{u, v} c
⊢ lift.{u, v}
      #(↑(sSup
              (range.{v, u + 1} (ι := o.ToType)
                ((fun (x : (↑(Iio o) : Type (u + 1))) ↦ A (↑x : Ordinal.{u})) ∘
                  (⇑(OrderIso.symm ToType.mk) : (a : o.ToType) → (↑(Iio o) : Type (u + 1)))))) :
          Type v) ≤
    lift.{u, v} c

Tactic:
apply ((mk_iUnion_le_lift _).trans _).trans_eq (mul_eq_self (aleph0_le_lift.2 hc))

Premises used: Iff.mpr, LE.le.trans_eq, Cardinal.mul_eq_self, Cardinal.aleph0_le_lift, Cardinal.mk_iUnion_le_lift, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #(↑(A j) : Type v) ≤ c
rw :
  lift.{v, u} o.card *
      ⨆ (i : o.ToType),
        lift.{u, v}
          #(↑(((fun (x : (↑(Iio o) : Type (u + 1))) ↦ A (↑x : Ordinal.{u})) ∘
                    (⇑(OrderIso.symm ToType.mk) : (a : o.ToType) → (↑(Iio o) : Type (u + 1))))
                  i) :
              Type v) ≤
    lift.{u, v} c * lift.{u, v} c
⊢ lift.{v, u} #o.ToType *
      ⨆ (i : o.ToType),
        lift.{u, v}
          #(↑(((fun (x : (↑(Iio o) : Type (u + 1))) ↦ A (↑x : Ordinal.{u})) ∘
                    (⇑(OrderIso.symm ToType.mk) : (a : o.ToType) → (↑(Iio o) : Type (u + 1))))
                  i) :
              Type v) ≤
    lift.{u, v} c * lift.{u, v} c

Tactic:
rw [mk_toType]

Premises used: Cardinal.mk_toType
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #(↑(A j) : Type v) ≤ c
⊢ lift.{v, u} o.card *
      ⨆ (i : o.ToType),
        lift.{u, v}
          #(↑(((fun (x : (↑(Iio o) : Type (u + 1))) ↦ A (↑x : Ordinal.{u})) ∘
                    (⇑(OrderIso.symm ToType.mk) : (a : o.ToType) → (↑(Iio o) : Type (u + 1))))
                  i) :
              Type v) ≤
    lift.{u, v} c * lift.{u, v} c

Tactic:
mul_le_mul' ho (ciSup_le' ?_)

Premises used: ciSup_le', mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #(↑(A j) : Type v) ≤ c
refine :
  ∀ (i : o.ToType),
    lift.{u, v}
        #(↑(((fun (x : (↑(Iio o) : Type (u + 1))) ↦ A (↑x : Ordinal.{u})) ∘
                  (⇑(OrderIso.symm ToType.mk) : (a : o.ToType) → (↑(Iio o) : Type (u + 1))))
                i) :
            Type v) ≤
      lift.{u, v} c
⊢ lift.{v, u} o.card *
      ⨆ (i : o.ToType),
        lift.{u, v}
          #(↑(((fun (x : (↑(Iio o) : Type (u + 1))) ↦ A (↑x : Ordinal.{u})) ∘
                    (⇑(OrderIso.symm ToType.mk) : (a : o.ToType) → (↑(Iio o) : Type (u + 1))))
                  i) :
              Type v) ≤
    lift.{u, v} c * lift.{u, v} c

Tactic:
refine mul_le_mul' ho (ciSup_le' ?_)

Premises used: ciSup_le', mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #(↑(A j) : Type v) ≤ c
i : o.ToType
⊢ lift.{u, v}
      #(↑(((fun (x : (↑(Iio o) : Type (u + 1))) ↦ A (↑x : Ordinal.{u})) ∘
                (⇑(OrderIso.symm ToType.mk) : (a : o.ToType) → (↑(Iio o) : Type (u + 1))))
              i) :
          Type v) ≤
    lift.{u, v} c

Tactic:
simpa using hA _ i.toOrd.prop
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
β : Type u_1
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o.card ≤ c
hc : ℵ₀ ≤ c
A : Ordinal.{u_1} → Set β
hA : ∀ j < o, #(↑(A j) : Type u_1) ≤ c
apply : lift.{u_1, u_1} o.card ≤ lift.{u_1, u_1} c
⊢ #(↑(⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < o), A j) : Type u_1) ≤ c

Tactic:
apply mk_biUnion_le_of_le_lift _ hc A hA

Premises used: Cardinal.mk_biUnion_le_of_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
β : Type u_1
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o.card ≤ c
hc : ℵ₀ ≤ c
A : Ordinal.{u_1} → Set β
hA : ∀ j < o, #(↑(A j) : Type u_1) ≤ c
rwa rwa₁ rwa₂ rwa₃ : o.card ≤ c
⊢ lift.{u_1, u_1} o.card ≤ lift.{u_1, u_1} c

Tactic:
rwa [Cardinal.lift_le]

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
pos : ∀ (hf : ¬BddAbove (range f)), Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ (f i).card
neg : ∀ (hf : BddAbove (range f)), Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ (f i).card
⊢ Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ (f i).card

Tactic:
by_cases! hf : ¬ BddAbove (range f)

Premises used: BddAbove, Set.range
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : ¬BddAbove (range f)
⊢ Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ (f i).card

Tactic:
simp [ciSup_of_not_bddAbove hf]

Premises used: ciSup_of_not_bddAbove
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
neg : Cardinal.lift.{u, v} #(ToType (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ #(f i).ToType
⊢ Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ (f i).card

Tactic:
simp_rw [← mk_toType]

Premises used: Cardinal.mk_toType
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
neg : Cardinal.lift.{max v u, v} #(ToType (⨆ (i : ι), f i)) ≤ Cardinal.lift.{v, max v u} #((x : ι) × (f x).ToType)
⊢ Cardinal.lift.{u, v} #(ToType (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ #(f i).ToType

Tactic:
rw [← mk_sigma, ← Cardinal.lift_id'.{v} #(Σ _, _), ← Cardinal.lift_umax.{v, u}]

Premises used: Cardinal.mk_sigma
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
neg :
  Function.Surjective (α := (x : ι) × (f x).ToType) (β := ToType (⨆ (i : ι), f i))
    (Function.comp (β := (↑(Iio (⨆ (i : ι), f i)) : Type (v + 1)))
      (⇑ToType.mk : (a : (↑(Iio (⨆ (i : ι), f i)) : Type (v + 1))) → (⨆ (i : ι), f i).ToType)
      fun (x : (x : ι) × (f x).ToType) ↦
      Subtype.mk (p := fun (x : Ordinal.{v}) ↦ Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x)
        (↑x.snd (β := fun (x : ι) ↦ (f x).ToType).toOrd : Ordinal.{v}) ⋯)
⊢ Cardinal.lift.{max v u, v} #(ToType (⨆ (i : ι), f i)) ≤ Cardinal.lift.{v, max v u} #((x : ι) × (f x).ToType)

Tactic:
apply lift_mk_le_lift_mk_of_surjective (f := .mk ∘ (⟨·.2.toOrd,
    (mem_Iio.mp (ToType.toOrd _).2).trans_le (le_ciSup hf _)⟩))

Premises used: Cardinal.lift_mk_le_lift_mk_of_surjective
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
neg :
  Function.Surjective (β := (↑(Iio (⨆ (i : ι), f i)) : Type (v + 1))) fun (x : (x : ι) × (f x).ToType) ↦
    Subtype.mk (p := fun (x : Ordinal.{v}) ↦ Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x)
      (↑x.snd (β := fun (x : ι) ↦ (f x).ToType).toOrd : Ordinal.{v}) ⋯
⊢ Function.Surjective (α := (x : ι) × (f x).ToType) (β := ToType (⨆ (i : ι), f i))
    (Function.comp (β := (↑(Iio (⨆ (i : ι), f i)) : Type (v + 1)))
      (⇑ToType.mk : (a : (↑(Iio (⨆ (i : ι), f i)) : Type (v + 1))) → (⨆ (i : ι), f i).ToType)
      fun (x : (x : ι) × (f x).ToType) ↦
      Subtype.mk (p := fun (x : Ordinal.{v}) ↦ Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x)
        (↑x.snd (β := fun (x : ι) ↦ (f x).ToType).toOrd : Ordinal.{v}) ⋯)

Tactic:
rw [EquivLike.comp_surjective]

Premises used: EquivLike.comp_surjective
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
x : Ordinal.{v}
hx : Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x
neg :
  ∀ (i : ι) (hi : x < f i),
    ∃ (a : (x : ι) × (f x).ToType),
      (fun (x : (x : ι) × (f x).ToType) ↦
            (Subtype.mk (p := fun (x : Ordinal.{v}) ↦ Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x)
                (↑x.snd (β := fun (x : ι) ↦ (f x).ToType).toOrd : Ordinal.{v}) ⋯ :
              { x : Ordinal.{v} // Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x }))
          a =
        Subtype.mk (p := fun (x : Ordinal.{v}) ↦ Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x) x hx
⊢ ∃ (a : (x : ι) × (f x).ToType),
    (fun (x : (x : ι) × (f x).ToType) ↦
          (Subtype.mk (p := fun (x : Ordinal.{v}) ↦ Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x)
              (↑x.snd (β := fun (x : ι) ↦ (f x).ToType).toOrd : Ordinal.{v}) ⋯ :
            { x : Ordinal.{v} // Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x }))
        a =
      Subtype.mk (p := fun (x : Ordinal.{v}) ↦ Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x) x hx

Tactic:
obtain ⟨i, hi⟩ := (lt_ciSup_iff' hf).mp hx

Premises used: Iff.mp, lt_ciSup_iff'
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
x : Ordinal.{v}
hx : Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x
i : ι
hi : x < f i
⊢ (fun (x : (x : ι) × (f x).ToType) ↦
        (Subtype.mk (p := fun (x : Ordinal.{v}) ↦ Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x)
            (↑x.snd (β := fun (x : ι) ↦ (f x).ToType).toOrd : Ordinal.{v}) ⋯ :
          { x : Ordinal.{v} // Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x }))
      (Sigma.mk (β := fun (x : ι) ↦ (f x).ToType) i
        ((ToType.mk : (a : (↑(Iio (f i)) : Type (v + 1))) → (f i).ToType)
          (Subtype.mk (p := fun (x : Ordinal.{v}) ↦ x ∈ Iio (f i)) x hi))) =
    Subtype.mk (p := fun (x : Ordinal.{v}) ↦ Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x) x hx

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
x : Ordinal.{v}
hx : Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x
i : ι
hi : x < f i
⊢ ∃ (a : (x : ι) × (f x).ToType),
    (fun (x : (x : ι) × (f x).ToType) ↦
          (Subtype.mk (p := fun (x : Ordinal.{v}) ↦ Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x)
              (↑x.snd (β := fun (x : ι) ↦ (f x).ToType).toOrd : Ordinal.{v}) ⋯ :
            { x : Ordinal.{v} // Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x }))
        a =
      Subtype.mk (p := fun (x : Ordinal.{v}) ↦ Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x) x hx

Tactic:
exact ⟨⟨i, .mk ⟨x, hi⟩⟩, by simp⟩
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ Cardinal.lift.{u, max u v} (card (⨆ (i : ι), f i)) ≤ sum fun (i : ι) ↦ (f i).card

Tactic:
have := lift_card_iSup_le_sum_card f
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
this : Cardinal.lift.{u, max u v} (card (⨆ (i : ι), f i)) ≤ sum fun (i : ι) ↦ (f i).card
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : card (⨆ (i : ι), f i) ≤ sum fun (i : ι) ↦ (f i).card), card (⨆ (i : ι), f i) ≤ sum fun (i : ι) ↦ (f i).card
⊢ card (⨆ (i : ι), f i) ≤ sum fun (i : ι) ↦ (f i).card

Tactic:
rwa [Cardinal.lift_id'] at this

Premises used: Cardinal.lift_id'
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
apply : Eq (α := Ordinal.{max u v}) (⨆ (i : o.ToType), f i.toOrd) (⨆ (a : (↑(Iio o) : Type (u + 1))), f a)
⊢ card (⨆ (a : (↑(Iio o) : Type (u + 1))), f a) ≤ sum fun (i : o.ToType) ↦ (f i.toOrd).card

Tactic:
apply le_of_eq_of_le (congr_arg _ _).symm (card_iSup_le_sum_card _)

Premises used: congr_arg, le_of_eq_of_le, Eq.symm, Ordinal.card_iSup_le_sum_card
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
⊢ Eq (α := Ordinal.{max u v}) (⨆ (i : o.ToType), f i.toOrd) (⨆ (a : (↑(Iio o) : Type (u + 1))), f a)

Tactic:
simpa using ToType.mk.symm.iSup_comp (g := fun x ↦ f x)

Premises used: Equiv.iSup_comp, OrderIso.symm, Ordinal.ToType.mk, RelIso.toEquiv
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
apply :
  (sum fun (i : o.ToType) ↦ (f i.toOrd).card) ≤
    Cardinal.lift.{v, u} o.card * ⨆ (a : (↑(Iio o) : Type (u + 1))), (f a).card
⊢ card (⨆ (a : (↑(Iio o) : Type (u + 1))), f a) ≤
    Cardinal.lift.{v, u} o.card * ⨆ (a : (↑(Iio o) : Type (u + 1))), (f a).card

Tactic:
apply (card_iSup_Iio_le_sum_card f).trans

Premises used: Ordinal.card_iSup_Iio_le_sum_card, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
⊢ (sum fun (i : o.ToType) ↦ (f i.toOrd).card) ≤ Cardinal.lift.{v, u} #o.ToType * ⨆ (i : o.ToType), (f i.toOrd).card

Tactic:
sum_le_lift_mk_mul_iSup _

Premises used: Cardinal.sum_le_lift_mk_mul_iSup
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
h : #o.ToType = o.card
h₁ : Eq (α := Cardinal.{max u v}) (⨆ (i : o.ToType), (f i.toOrd).card) (⨆ (a : (↑(Iio o) : Type (u + 1))), (f a).card)
⊢ (sum fun (i : o.ToType) ↦ (f i.toOrd).card) ≤
    Cardinal.lift.{v, u} o.card * ⨆ (a : (↑(Iio o) : Type (u + 1))), (f a).card

Tactic:
convert! ← sum_le_lift_mk_mul_iSup _

Premises used: Cardinal.sum_le_lift_mk_mul_iSup
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
⊢ #o.ToType = o.card

Tactic:
mk_toType o

Premises used: Cardinal.mk_toType
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
⊢ #o.ToType = o.card

Tactic:
exact mk_toType o

Premises used: Cardinal.mk_toType
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
⊢ Eq (α := Cardinal.{max u v}) (⨆ (i : o.ToType), (f i.toOrd).card) (⨆ (a : (↑(Iio o) : Type (u + 1))), (f a).card)

Tactic:
ToType.mk.symm.iSup_comp (g := fun x ↦ (f x).card)

Premises used: Equiv.iSup_comp, OrderIso.symm, Ordinal.ToType.mk, RelIso.toEquiv
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
⊢ Eq (α := Cardinal.{max u v}) (⨆ (i : o.ToType), (f i.toOrd).card) (⨆ (a : (↑(Iio o) : Type (u + 1))), (f a).card)

Tactic:
exact ToType.mk.symm.iSup_comp (g := fun x ↦ (f x).card)

Premises used: Equiv.iSup_comp, OrderIso.symm, Ordinal.ToType.mk, RelIso.toEquiv
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
pos : ∀ (hc : c < ℵ₀), card (⨆ (i : ι), f i) ≤ c
neg : ∀ (hc : ℵ₀ ≤ c), card (⨆ (i : ι), f i) ≤ c
⊢ card (⨆ (i : ι), f i) ≤ c

Tactic:
by_cases! hc : c < ℵ₀
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : c < ℵ₀
pos :
  ∀ (n : ℕ) (hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} (↑n : Cardinal.{v}))
    (hf : ∀ (i : ι), (f i).card ≤ (↑n : Cardinal.{v})) (hc : (↑n : Cardinal.{v}) < ℵ₀),
    card (⨆ (i : ι), f i) ≤ (↑n : Cardinal.{v})
⊢ card (⨆ (i : ι), f i) ≤ c

Tactic:
obtain ⟨n, rfl⟩ := lt_aleph0.1 hc

Premises used: Iff.mp, Cardinal.lt_aleph0, rfl
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
n : ℕ
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} (↑n : Cardinal.{v})
hf : ∀ (i : ι), (f i).card ≤ (↑n : Cardinal.{v})
hc : (↑n : Cardinal.{v}) < ℵ₀
pos : LE.le.{v + 1} (α := Ordinal.{v}) (⨆ (i : ι), f i) (↑n : Ordinal.{v})
⊢ card (⨆ (i : ι), f i) ≤ (↑n : Cardinal.{v})

Tactic:
rw [card_le_nat]

Premises used: Ordinal.card_le_nat
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
n : ℕ
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} (↑n : Cardinal.{v})
hf : ∀ (i : ι), (f i).card ≤ (↑n : Cardinal.{v})
hc : (↑n : Cardinal.{v}) < ℵ₀
⊢ LE.le.{v + 1} (α := Ordinal.{v}) (⨆ (i : ι), f i) (↑n : Ordinal.{v})

Tactic:
ciSup_le' fun i ↦ ?_

Premises used: ciSup_le'
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
n : ℕ
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} (↑n : Cardinal.{v})
hf : ∀ (i : ι), (f i).card ≤ (↑n : Cardinal.{v})
hc : (↑n : Cardinal.{v}) < ℵ₀
pos : ∀ (i : ι), f i ≤ (↑n : Ordinal.{v})
⊢ LE.le.{v + 1} (α := Ordinal.{v}) (⨆ (i : ι), f i) (↑n : Ordinal.{v})

Tactic:
refine ciSup_le' fun i ↦ ?_

Premises used: ciSup_le'
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{v}
n : ℕ
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} (↑n : Cardinal.{v})
hf : ∀ (i : ι), (f i).card ≤ (↑n : Cardinal.{v})
hc : (↑n : Cardinal.{v}) < ℵ₀
i : ι
⊢ f i ≤ (↑n : Ordinal.{v})

Tactic:
simpa using hf i
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
neg : Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ Cardinal.lift.{u, v} c
⊢ card (⨆ (i : ι), f i) ≤ c

Tactic:
rw [← Cardinal.lift_le.{u}]
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
apply : Cardinal.lift.{v, u} #ι * ⨆ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c
⊢ Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ Cardinal.lift.{u, v} c

Tactic:
apply (lift_card_iSup_le_sum_card ..).trans ((sum_le_lift_mk_mul_iSup_lift _).trans _)

Premises used: Ordinal.lift_card_iSup_le_sum_card, Cardinal.sum_le_lift_mk_mul_iSup_lift, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
rw :
  Cardinal.lift.{v, u} #ι * ⨆ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c * Cardinal.lift.{u, v} c
⊢ Cardinal.lift.{v, u} #ι * ⨆ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c

Tactic:
rw [← mul_eq_self hc, Cardinal.lift_mul]

Premises used: Cardinal.mul_eq_self, Cardinal.lift_mul
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
apply : ∀ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c
⊢ Cardinal.lift.{v, u} #ι * ⨆ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c * Cardinal.lift.{u, v} c

Tactic:
apply mul_le_mul' hι (ciSup_le' _)

Premises used: ciSup_le', mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ ∀ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c

Tactic:
simpa [← lift_card]

Premises used: Ordinal.lift_card
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u_1
c : Cardinal.{u_1}
f : ι → Ordinal.{u_1}
hι : #ι ≤ c
hf : ∀ (i : ι), (f i).card ≤ c
⊢ Cardinal.lift.{u_1, u_1} #ι ≤ Cardinal.lift.{u_1, u_1} c

Tactic:
rw [← Cardinal.lift_le] at hι

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Ordinal
Goal:
ι : Type u_1
c : Cardinal.{u_1}
f : ι → Ordinal.{u_1}
hι : #ι ≤ c
hf : ∀ (i : ι), (f i).card ≤ c
hι₁ : Cardinal.lift.{u_1, u_1} #ι ≤ Cardinal.lift.{u_1, u_1} c
⊢ ∀ (i : ι), (f i).card ≤ c

Tactic:
rw [← Cardinal.lift_le] at hι

Premises used: Cardinal.lift_le