awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
⊢ #(↑(⋃ (j : Ordinal.{u}), ⋃ (_ : j < o), A j) : Type v) ≤ c
have 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
Tactic: simp_rw [← mem_Iio, biUnion_eq_iUnion, iUnion, iSup, ← ToType.mk.symm.surjective.range_comp]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
⊢ #(↑(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
have 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
Tactic: rw [← lift_le.{u}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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.{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
have 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
Tactic: apply ((mk_iUnion_le_lift _).trans _).trans_eq (mul_eq_self (aleph0_le_lift.2 hc))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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.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
have 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
Tactic: rw [mk_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
have 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
Tactic: refine mul_le_mul' ho (ciSup_le' ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
⊢ #(↑(⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < o), A j) : Type u_1) ≤ c
have apply : lift.{u_1, u_1} o.card ≤ lift.{u_1, u_1} c
Tactic: apply mk_biUnion_le_of_le_lift _ hc A hA
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{v}
⊢ Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ (f i).card
have pos : ∀ (hf : ¬BddAbove (range f)), Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ (f i).card
Tactic: by_cases! hf : ¬ BddAbove (range f)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
⊢ Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ (f i).card
have neg : ∀ (hf : BddAbove (range f)), Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ (f i).card
Tactic: by_cases! hf : ¬ BddAbove (range f)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
have neg : Cardinal.lift.{u, v} #(ToType (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ #(f i).ToType
Tactic: simp_rw [← mk_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Cardinal.lift.{u, v} #(ToType (⨆ (i : ι), f i)) ≤ sum.{u, v} fun (i : ι) ↦ #(f i).ToType
have neg : Cardinal.lift.{max v u, v} #(ToType (⨆ (i : ι), f i)) ≤ Cardinal.lift.{v, max v u} #((x : ι) × (f x).ToType)
Tactic: rw [← mk_sigma, ← Cardinal.lift_id'.{v} #(Σ _, _), ← Cardinal.lift_umax.{v, u}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Cardinal.lift.{max v u, v} #(ToType (⨆ (i : ι), f i)) ≤ Cardinal.lift.{v, max v u} #((x : ι) × (f x).ToType)
have 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}) sorry)
Tactic: apply lift_mk_le_lift_mk_of_surjective (f := .mk ∘ (⟨·.2.toOrd,
    (mem_Iio.mp (ToType.toOrd _).2).trans_le (le_ciSup hf _)⟩))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ 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}) ⋯)
have 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}) sorry
Tactic: rw [EquivLike.comp_surjective]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
x : Ordinal.{v}
hx : Membership.mem (γ := Set Ordinal.{v}) (Iio (⨆ (i : ι), f i)) x
⊢ ∃ (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
have 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}) sorry :
            { 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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (hypothesis)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ card (⨆ (i : ι), f i) ≤ sum fun (i : ι) ↦ (f i).card
have this : 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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
⊢ card (⨆ (i : ι), f i) ≤ sum fun (i : ι) ↦ (f i).card
have rwa : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
⊢ card (⨆ (a : (↑(Iio o) : Type (u + 1))), f a) ≤ sum fun (i : o.ToType) ↦ (f i.toOrd).card
have apply : Eq (α := Ordinal.{max u v}) (⨆ (i : o.ToType), f i.toOrd) (⨆ (a : (↑(Iio o) : Type (u + 1))), f a)
Tactic: apply le_of_eq_of_le (congr_arg _ _).symm (card_iSup_le_sum_card _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
⊢ card (⨆ (a : (↑(Iio o) : Type (u + 1))), f a) ≤
    Cardinal.lift.{v, u} o.card * ⨆ (a : (↑(Iio o) : Type (u + 1))), (f a).card
have 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
Tactic: apply (card_iSup_Iio_le_sum_card f).trans
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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.card * ⨆ (a : (↑(Iio o) : Type (u + 1))), (f a).card
have h : #o.ToType = o.card
Tactic: convert! ← sum_le_lift_mk_mul_iSup _
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{max u v}
h : #o.ToType = o.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
have h₁ : Eq (α := Cardinal.{max u v}) (⨆ (i : o.ToType), (f i.toOrd).card) (⨆ (a : (↑(Iio o) : Type (u + 1))), (f a).card)
Tactic: convert! ← sum_le_lift_mk_mul_iSup _
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
⊢ card (⨆ (i : ι), f i) ≤ c
have pos : ∀ (hc : c < ℵ₀), card (⨆ (i : ι), f i) ≤ c
Tactic: by_cases! hc : c < ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
⊢ card (⨆ (i : ι), f i) ≤ c
have neg : ∀ (hc : ℵ₀ ≤ c), card (⨆ (i : ι), f i) ≤ c
Tactic: by_cases! hc : c < ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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 < ℵ₀
⊢ card (⨆ (i : ι), f i) ≤ c
have 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})
Tactic: obtain ⟨n, rfl⟩ := lt_aleph0.1 hc
Cleared hypotheses: c, hι, hf, hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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}) < ℵ₀
⊢ card (⨆ (i : ι), f i) ≤ (↑n : Cardinal.{v})
have pos : LE.le.{v + 1} (α := Ordinal.{v}) (⨆ (i : ι), f i) (↑n : Ordinal.{v})
Tactic: rw [card_le_nat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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})
have pos : ∀ (i : ι), f i ≤ (↑n : Ordinal.{v})
Tactic: refine ciSup_le' fun i ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
⊢ card (⨆ (i : ι), f i) ≤ c
have neg : Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ Cardinal.lift.{u, v} c
Tactic: rw [← Cardinal.lift_le.{u}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
⊢ Cardinal.lift.{u, v} (card (⨆ (i : ι), f i)) ≤ Cardinal.lift.{u, v} c
have apply : Cardinal.lift.{v, u} #ι * ⨆ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c
Tactic: apply (lift_card_iSup_le_sum_card ..).trans ((sum_le_lift_mk_mul_iSup_lift _).trans _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
⊢ Cardinal.lift.{v, u} #ι * ⨆ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c
have rw : Cardinal.lift.{v, u} #ι * ⨆ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c * Cardinal.lift.{u, v} c
Tactic: rw [← mul_eq_self hc, Cardinal.lift_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
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
⊢ Cardinal.lift.{v, u} #ι * ⨆ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c * Cardinal.lift.{u, v} c
have apply : ∀ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c
Tactic: apply mul_le_mul' hι (ciSup_le' _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (hypothesis)
Goal:
ι : Type u_1
c : Cardinal.{u_1}
f : ι → Ordinal.{u_1}
hι : #ι ≤ c
hf : ∀ (i : ι), (f i).card ≤ c
⊢ card (⨆ (i : ι), f i) ≤ c
have hι₁ : Cardinal.lift.{u_1, u_1} #ι ≤ Cardinal.lift.{u_1, u_1} c
Tactic: rw [← Cardinal.lift_le] at hι
Cleared hypotheses: hι, hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u}
c : Cardinal.{v}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : (↑(Iio o) : Type (u + 1))), (f i).card ≤ c
⊢ card (⨆ (i : (↑(Iio o) : Type (u + 1))), f i) ≤ c
have apply : Cardinal.lift.{v, u + 1} #(↑(Iio o) : Type (u + 1)) ≤ Cardinal.lift.{u + 1, v} c
Tactic: apply card_iSup_le_lift _ hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u}
c : Cardinal.{v}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : (↑(Iio o) : Type (u + 1))), (f i).card ≤ c
| Cardinal.lift.{u + 1, v} c
have rw : Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
Tactic: rw [← Cardinal.lift_lift.{u, u + 1}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u}
c : Cardinal.{v}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : (↑(Iio o) : Type (u + 1))), (f i).card ≤ c
⊢ Cardinal.lift.{v, u + 1} #(↑(Iio o) : Type (u + 1)) ≤ Cardinal.lift.{u + 1, v} c
have conv_rhs : Cardinal.lift.{v, u + 1} #(↑(Iio o) : Type (u + 1)) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
Tactic: conv_rhs => rw [← Cardinal.lift_lift.{u, u + 1}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u}
c : Cardinal.{v}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : (↑(Iio o) : Type (u + 1))), (f i).card ≤ c
⊢ Cardinal.lift.{v, u + 1} #(↑(Iio o) : Type (u + 1)) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
have rwa : Cardinal.lift.{v, u + 1} (Cardinal.lift.{u + 1, u} o.card) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
Tactic: rwa [Cardinal.mk_Iio_ordinal, Cardinal.lift_lift, ← Cardinal.lift_lift.{v, u + 1},
    Cardinal.lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u}
c : Cardinal.{v}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : (↑(Iio o) : Type (u + 1))), (f i).card ≤ c
rwa :
  Cardinal.lift.{v, u + 1} (Cardinal.lift.{u + 1, u} o.card) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
⊢ Cardinal.lift.{v, u + 1} #(↑(Iio o) : Type (u + 1)) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
have rwa₁ : Cardinal.lift.{max (u + 1) v, u} o.card ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
Tactic: rwa [Cardinal.mk_Iio_ordinal, Cardinal.lift_lift, ← Cardinal.lift_lift.{v, u + 1},
    Cardinal.lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u}
c : Cardinal.{v}
f : (↑(Iio o) : Type (u + 1)) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : (↑(Iio o) : Type (u + 1))), (f i).card ≤ c
rwa :
  Cardinal.lift.{v, u + 1} (Cardinal.lift.{u + 1, u} o.card) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
rwa₁ : Cardinal.lift.{max (u + 1) v, u} o.card ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
⊢ Cardinal.lift.{v, u + 1} #(↑(Iio o) : Type (u + 1)) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
have rwa₂ : Cardinal.lift.{u + 1, max v u} (Cardinal.lift.{v, u} o.card) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
Tactic: rwa [Cardinal.mk_Iio_ordinal, Cardinal.lift_lift, ← Cardinal.lift_lift.{v, u + 1},
    Cardinal.lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (hypothesis)
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
f : (↑(Iio o) : Type (u_1 + 1)) → Ordinal.{u_1}
hι : o.card ≤ c
hf : ∀ (i : (↑(Iio o) : Type (u_1 + 1))), (f i).card ≤ c
⊢ card (⨆ (i : (↑(Iio o) : Type (u_1 + 1))), f i) ≤ c
have hι₁ : Cardinal.lift.{u_1, u_1} o.card ≤ Cardinal.lift.{u_1, u_1} c
Tactic: rw [← Cardinal.lift_le] at hι
Cleared hypotheses: hι, hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ (sSup s).card ≤ c
have rw : card (⨆ (a : (↑s : Type (u + 1))), (↑a : Ordinal.{u})) ≤ c
Tactic: rw [sSup_eq_iSup']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ card (⨆ (a : (↑s : Type (u + 1))), (↑a : Ordinal.{u})) ≤ c
have hι : Cardinal.lift.{u, u + 1} #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c
Tactic: apply card_iSup_le_lift
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
hι : Cardinal.lift.{u, u + 1} #(↑s : Type (u + 1)) ≤ Cardinal.lift.{u + 1, u} c
⊢ card (⨆ (a : (↑s : Type (u + 1))), (↑a : Ordinal.{u})) ≤ c
have hf : ∀ (i : (↑s : Type (u + 1))), (↑i : Ordinal.{u}).card ≤ c
Tactic: apply card_iSup_le_lift
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ (b + 1)).card ≤ max a.card (b + 1).card
have add_one : max a.card (a ^ b).card ≤ max a.card (b.card + 1)
Tactic: rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
add_one : max a.card (a ^ b).card ≤ max a.card (b.card + 1)
⊢ (a ^ (b + 1)).card ≤ max a.card (b + 1).card
have add_one₁ : (a ^ b).card ≠ 0
Tactic: rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
add_one : max a.card (a ^ b).card ≤ max a.card (b.card + 1)
add_one₁ : (a ^ b).card ≠ 0
⊢ (a ^ (b + 1)).card ≤ max a.card (b + 1).card
have add_one₂ : ℵ₀ ≤ a.card
Tactic: rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ max a.card (a ^ b).card ≤ max a.card (b.card + 1)
have add_one : max a.card (max a.card b.card) ≤ max a.card (b.card + 1)
Tactic: grw [IH]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ max a.card (max a.card b.card) ≤ max a.card (b.card + 1)
have add_one : max a.card b.card ≤ max a.card (b.card + 1)
Tactic: rw [← max_assoc, max_self]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ max a.card b.card ≤ max a.card (b.card + 1)
have add_one : max a.card b.card ≤ max a.card b.card
Tactic: grw [← le_self_add]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card ≠ 0
have add_one : ¬(a = 0 ∧ b ≠ 0)
Tactic: rw [ne_eq, card_eq_zero, opow_eq_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
hb : Order.IsSuccLimit b
IH : ∀ o' < b, (a ^ o').card ≤ max a.card o'.card
⊢ (a ^ b).card ≤ max a.card b.card
have limit : card (⨆ (b_1 : (↑(Iio b) : Type (u_1 + 1))), a ^ (↑b_1 : Ordinal.{u_1})) ≤ max a.card b.card
Tactic: rw [(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isSuccLimit hb]