mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < typeLT o.ToType
b : o.ToType
hb : b ∈ S
hb' : (typein LT.lt).toRelEmbedding ((enum fun x1 x2 ↦ x1 < x2) ⟨a, ha⟩) ≤ (typein LT.lt).toRelEmbedding b
⊢ a < lsub f

Tactic:
typein_enum

Goal state after:
case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < typeLT o.ToType
b : o.ToType
hb : b ∈ S
hb' : a ≤ (typein LT.lt).toRelEmbedding b
⊢ a < lsub f
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < typeLT o.ToType
b : o.ToType
hb : b ∈ S
hb' : a ≤ (typein LT.lt).toRelEmbedding b
⊢ a < lsub f

Tactic:
]

Goal state after:
case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < typeLT o.ToType
b : o.ToType
hb : b ∈ S
hb' : a ≤ (typein LT.lt).toRelEmbedding b
⊢ a < lsub f
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_1
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
⊢ type r ≤ type r

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
⊢ ∃ ι f, lsub f = o ∧ #ι = sInf {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
]

Goal state after:
o : Ordinal.{u}
⊢ ∃ ι f, lsub f = o ∧ #ι = sInf {a | ∃ ι f, lsub f = o ∧ #ι = a}
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lift.{u, max u v} (lsub f)).cof ≤ Cardinal.lift.{max u v, u} #ι

Tactic:
]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lift.{u, max u v} (lsub f)).cof ≤ Cardinal.lift.{max u v, u} #ι
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
a : Cardinal.{u}
⊢ a ≤ sInf {a | ∃ ι f, lsub f = o ∧ #ι = a} ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι

Tactic:
]

Goal state after:
o : Ordinal.{u}
a : Cardinal.{u}
⊢ a ≤ sInf {a | ∃ ι f, lsub f = o ∧ #ι = a} ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ #ι

Tactic:
]

Goal state after:
o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ #ι
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl.inl
n m : ℕ
⊢ ↑(n ^ m) ≤ max ℵ₀ (max (↑n).card (↑m).card)

Tactic:
]

Goal state after:
case inl.inl
n m : ℕ
⊢ ↑(n ^ m) ≤ max ℵ₀ (max (↑n).card (↑m).card)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{v, u} #ι < c.cof

Tactic:
]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{v, u} #ι < c.cof
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_2
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i j : Ordinal.{u}
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ ⟨i, x✝¹⟩ < ⟨j, h⟩

Tactic:
]

Goal state after:
case refine_2
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i j : Ordinal.{u}
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ ⟨i, x✝¹⟩ < ⟨j, h⟩
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
hf : Cardinal.lift.{v, u} #ι < (iSup f).cof
⊢ Cardinal.lift.{v, u} #ι < (iSup f).cof

Tactic:
]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
hf : Cardinal.lift.{v, u} #ι < (iSup f).cof
⊢ Cardinal.lift.{v, u} #ι < (iSup f).cof
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_3
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
⊢ ∀ (i : ι), f i < (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)

Tactic:
]

Goal state after:
case refine_3
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
⊢ ∀ (i : ι), f i < (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{v, u} #ι < c.ord.cof

Tactic:
]

Goal state after:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{v, u} #ι < c.ord.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_1
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{v, u} #(List ι) < c.cof

Tactic:
]

Goal state after:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{v, u} #(List ι) < c.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_1
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ max (Cardinal.lift.{v, u} ℵ₀) (Cardinal.lift.{v, u} #ι) < c.cof

Tactic:
]

Goal state after:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ max (Cardinal.lift.{v, u} ℵ₀) (Cardinal.lift.{v, u} #ι) < c.cof
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case pos
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∀ (j : ι), r j i → f j < f i
⊢ f i ≤ f ↑⟨i, h⟩

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a : Ordinal.{u_1}
h : a ≠ 0
⊢ max ℵ₀ a.card = max ℵ₀ a.card

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a : Ordinal.{u_1}
h : 1 < a
⊢ max ℵ₀ a.card = max ℵ₀ a.card

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Ordinal.{u}
hc : ℵ₀ < c.cof
hc' : #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{u}
⊢ #ι < c.cof

Tactic:
]

Goal state after:
ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Ordinal.{u}
hc : ℵ₀ < c.cof
hc' : #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{u}
⊢ #ι < c.cof
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) ω

Tactic:
]

Goal state after:
case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) ω
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ f, o.cof.ord.blsub f = o

Tactic:
]

Goal state after:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ f, o.cof.ord.blsub f = o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ f, (type r).blsub f = o

Tactic:
]

Goal state after:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ f, (type r).blsub f = o
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ((fun x1 x2 ↦ x1 ^ x2) a b).card < ℵ_ o

Tactic:
]

Goal state after:
case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ((fun x1 x2 ↦ x1 ^ x2) a b).card < ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = ↑n
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
⊢ ⟦α⟧ ≤ ⟦α⟧

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ 0 < o

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ 0 < o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = b
hι' : (#ι).ord = type r
⊢ a ≤ #ι

Tactic:
]

Goal state after:
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = b
hι' : (#ι).ord = type r
⊢ a ≤ #ι
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case neg.refine_2
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ j, r j i ∧ f i ≤ f j
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ f i ≤ f ↑⟨⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h, ⋯⟩

Tactic:
]

Goal state after:
case neg.refine_2
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ j, r j i ∧ f i ≤ f j
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ f i ≤ f ↑⟨⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} #o.ToType

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} #o.ToType
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{u, u} o.card

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{u, u} o.card
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ℵ₀ ≤ c

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ℵ₀ ≤ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
n : ℕ
ih : ⟦α⟧ ^ ↑n ≤ ⟦α⟧
⊢ ⟦α⟧ ≤ ⟦α⟧

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
⊢ o.card < c.cof

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
⊢ o.card < c.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card + b.card < c

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card + b.card < c
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_2
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (a.blsub fun b x ↦ f b) = f a

Tactic:
]

Goal state after:
case refine_2
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (a.blsub fun b x ↦ f b) = f a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ Cardinal.lift.{u, u} o.card

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ Cardinal.lift.{u, u} o.card
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 2 ^ c ≤ 2 ^ c

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o.card.ord

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o.card.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
⊢ o.card < c.cof

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
⊢ o.card < c.cof
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ ω ≤ o

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ ω ≤ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{u, v} (c i)) = lift.{v, u} (2 ^ #ι)

Tactic:
]

Goal state after:
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{u, v} (c i)) = lift.{v, u} (2 ^ #ι)
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
H : (ℵ_ o).IsRegular
⊢ ℵ_ o = ℵ_ o

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
h : IsSuccLimit o
⊢ IsSuccLimit o

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
h : IsSuccLimit o
⊢ IsSuccLimit o
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
⊢ (⨆ i, ↑(f i) + 1).card ≤ c

Tactic:
]

Goal state after:
case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
⊢ (⨆ i, ↑(f i) + 1).card ≤ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case le_cof_ord.refine_2
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
i : ↑(Iio (succ c).ord.cof.ord)
⊢ ↑(f i) + 1 < (succ c).ord

Tactic:
]

Goal state after:
case le_cof_ord.refine_2
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
i : ↑(Iio (succ c).ord.cof.ord)
⊢ ↑(f i) + 1 < (succ c).ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.inl
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ (succ ℵ₀).IsRegular

Tactic:
]

Goal state after:
⊢ (succ ℵ₀).IsRegular
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
h : ω ≤ o
⊢ (succ (preAleph o)).IsRegular

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ (succ (preAleph o)).IsRegular
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ lift.{v, u} (2 ^ #ι) = lift.{v, u} (2 ^ #ι)

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card * b.card < c

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card * b.card < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
h : ω ≤ o
⊢ preAleph (o + 1) = preAleph (o + 1)

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (succ (ℵ_ o)).IsRegular

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
⊢ (succ (ℵ_ o)).IsRegular
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o.card.ord

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o.card.ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{v, u} 2) ≤ prod fun i ↦ lift.{u, v} (c i)

Tactic:
]

Goal state after:
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{v, u} 2) ≤ prod fun i ↦ lift.{u, v} (c i)
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case le_cof_ord
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
⊢ κ ≤ κ.ord.cof

Tactic:
]

Goal state after:
case le_cof_ord
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
⊢ κ ≤ κ.ord.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x < y
hs' : #↑s = Order.cof α
⊢ ∀ (a : α), ∃ b ∈ s, r a b

Tactic:
]

Goal state after:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x < y
hs' : #↑s = Order.cof α
⊢ ∀ (a : α), ∃ b ∈ s, r a b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ⊢ Cardinal.univ.{u, v} = Cardinal.univ.{u, v}

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inl
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
⊢ #{ s // Bounded r s } = 0

Tactic:
]

Goal state after:
case inl
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
⊢ #{ s // Bounded r s } = 0