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

Goal state before:
pp: a : Ordinal.{u_1}
f : ↑(Iio a) → Ordinal.{u_1}
hf : StrictMono f
ha : IsSuccPrelimit a
⊢ (⨆ i, f i).cof = a.cof

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c < ℵ_ ↑n ↔ c < ℵ_ ↑n

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℵ_ ↑n = lift.{v, u} c ↔ ℵ_ ↑n = c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c = ℵ_ ↑n ↔ c = ℵ_ ↑n

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : IsSuccLimit a
⊢ (f a).cof = a.cof

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n ≤ lift.{v, u} c ↔ ℶ_ ↑n ≤ c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c ≤ ℶ_ ↑n ↔ c ≤ ℶ_ ↑n

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n < lift.{v, u} c ↔ ℶ_ ↑n < c

Tactic:
by

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

Goal state before:
pp: case add_one
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
a✝ : a + 1 = a → (a + 1).cof ≤ (f (a + 1)).cof
⊢ (a + 1).cof ≤ (f (a + 1)).cof

Tactic:
rw [cof_add_one, Cardinal.one_le_iff_ne_zero, cof_eq_zero.ne]
    exact (hf.strictMono (lt_succ a)).ne_zero

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c < ℶ_ ↑n ↔ c < ℶ_ ↑n

Tactic:
by

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

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n = lift.{v, u} c ↔ ℶ_ ↑n = c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c = ℶ_ ↑n ↔ c = ℶ_ ↑n

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
⊢ ω_ 1 ≤ lift.{v, u} o ↔ ω_ 1 ≤ o

Tactic:
by

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

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a + b = b ↔ max ℵ₀ a ≤ b ∨ a = 0

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
⊢ a.cof ≤ (f a).cof

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
⊢ lift.{v, u} o ≤ ω_ 1 ↔ o ≤ ω_ 1

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u_1}
n : ℕ
ha : ℵ₀ ≤ a
⊢ ↑n + a = a

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
⊢ ω_ 1 < lift.{v, u} o ↔ ω_ 1 < o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
⊢ lift.{v, u} o < ω_ 1 ↔ o < ω_ 1

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
⊢ a * b = b ^ succ (log b a)

Tactic:
by

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

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
⊢ Small.{u, u + 2} ↑(Iio (typeLT ↑s))

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
⊢ ω_ 1 = lift.{v, u} o ↔ ω_ 1 = o

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ (fun x1 x2 ↦ x1 ^ x2) ↑m ↑n < ω

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
i : α
h : (#α).ord = typeLT α
hα : ℵ₀ ≤ #α
⊢ #↑(Iic i) < #α

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
⊢ lift.{v, u} o = ω_ 1 ↔ o = ω_ 1

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n ≤ lift.{v, u} o ↔ ω_ ↑n ≤ o

Tactic:
by

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

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
⊢ (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o ≤ ω_ ↑n ↔ o ≤ ω_ ↑n

Tactic:
by

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

Goal state before:
pp: β : 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) ≤ c
⊢ #↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c

Tactic:
by

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

Goal state before:
pp: β : 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) ≤ c
⊢ #↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c

Tactic:
by

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

Goal state before:
pp: a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ c < ℵ₀

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n < lift.{v, u} o ↔ ω_ ↑n < o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o < ω_ ↑n ↔ o < ω_ ↑n

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n = lift.{v, u} o ↔ ω_ ↑n = o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o = ω_ ↑n ↔ o = ω_ ↑n

Tactic:
by

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

Goal state before:
pp: a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
⊢ b = c

Tactic:
by

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

Goal state before:
pp: a b c : Cardinal.{u_1}
h : a + b = c + b
hb : b < ℵ₀
⊢ a = c

Tactic:
by

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ ⨆ i, ↑(f i) + 1 = o

Tactic:
by

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ o.cof.ord = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
⊢ ∃ r, (∀ (x : α), #{ y // ¬r x y } < #α) ∧ ∀ (y : α), #{ x // r x y } < #α

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
x : Ordinal.{v}
hx : x ∈ Iio (⨆ i, f i)
i : ι
hi : x < f i
⊢ (fun x ↦ ⟨↑x.snd.toOrd, ⋯⟩) ⟨i, ToType.mk ⟨x, hi⟩⟩ = ⟨x, hx⟩

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
i : ι
⊢ f i + c ≤ (⨆ i, f i) + c

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{v}
⊢ Cardinal.lift.{u, v} (⨆ i, f i).card ≤ sum fun i ↦ (f i).card

Tactic:
by

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ ⨆ i, ↑(f i) = o

Tactic:
by

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

Goal state before:
pp: s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : Cardinal.lift.{u + 2, u + 1} #↑s < Cardinal.lift.{u + 2, u} (⨆ i, ↑(f i) + 1).cof
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
x✝ : ↑(Iio (typeLT ↑s))
⊢ ∀ ⦃b : ↑(Iio (typeLT ↑s))⦄, x✝ < b → ↑(f x✝) < ↑(f b)

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : o ≤ o.cof.ord
⊢ IsCofinal (range id)

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ (⨆ i, f i).card ≤ sum fun i ↦ (f i).card

Tactic:
by

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

Goal state before:
pp: f : ↑(Iio 0) → ↑(Iio 0)
⊢ 0 ≤ (cof 0).ord

Tactic:
by

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

Goal state before:
pp: f : ↑(Iio 0) → ↑(Iio 0)
x✝ : ↑(Iio 0)
⊢ ∀ ⦃b : ↑(Iio 0)⦄, x✝ < b → f x✝ < f b

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ (⨆ a, f a).card ≤ sum fun i ↦ (f i.toOrd).card

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 1 ≤ (o + 1).cof.ord

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
x✝ : ↑(Iio 1)
⊢ ∀ ⦃b : ↑(Iio 1)⦄, x✝ < b → (fun x ↦ ⟨o, ⋯⟩) x✝ < (fun x ↦ ⟨o, ⋯⟩) b

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ IsCofinal (range fun x ↦ ⟨o, ⋯⟩)

Tactic:
by

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

Goal state before:
pp: a b o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : ↑(Iio b) → ↑(Iio a)
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ b ≤ o.cof.ord

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ (⨆ a, f a).card ≤ Cardinal.lift.{v, u} o.card * ⨆ a, (f a).card

Tactic:
by

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

Goal state before:
pp: a b o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : ↑(Iio b) → ↑(Iio a)
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ IsCofinal (range (f ∘ g))

Tactic:
by

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
⊢ a ≤ (g o).cof.ord

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ (⨆ i, f i) + c = ⨆ i, f i + c

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ c + ⨆ i, f i = ⨆ i, c + f i

Tactic:
by

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

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
⊢ sSup ((fun x ↦ x + 1) '' s) < a

Tactic:
by

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

Goal state before:
pp: ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
hf : BddAbove (range f)
g : ι' → Cardinal.{v}
hg : BddAbove (range g)
⊢ (⨆ i, f i) + ⨆ j, g j = ⨆ i, ⨆ j, f i + g j

Tactic:
by

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

Goal state before:
pp: β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ ∀ i ∈ range f, i < a

Tactic:
by

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
⊢ IsCofinal (range fun i ↦ ⟨g ↑(f i), ⋯⟩)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
x✝ : ↑(Iio o.cof.ord)
⊢ ∀ ⦃b : ↑(Iio o.cof.ord)⦄, x✝ < b → (↑(g x✝)).toOrd < (↑(g b)).toOrd

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
c : Cardinal.{u_1}
f : ι → Ordinal.{u_1}
hι : #ι ≤ c
hf : ∀ (i : ι), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
by

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

Goal state before:
pp: β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ ⨆ i, f i + 1 < a

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
i : ι
⊢ f i * c ≤ (⨆ i, f i) * c

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : #α < a.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i + 1 < a

Tactic:
by

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

Goal state before:
pp: a o : Ordinal.{u_1}
ha : o.cof.ord = a
⊢ ∃ f, IsFundamentalSeq f

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
by

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

Goal state before:
pp: a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ a.cof.ord ≤ o

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : #α < a.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i < a

Tactic:
by

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

Goal state before:
pp: β : Type v
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
⊢ (lift.{v, u} (⨆ i, f i + 1)).cof ≤ Cardinal.lift.{u, v} #β

Tactic:
by

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

Goal state before:
pp: a✝ : Ordinal.{?u.2}
b : Ordinal.{?u.4}
o✝ : Ordinal.{?u.6}
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi : i < a.cof.ord
⊢ a.cof.ord ≤ o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
f : ↑(Iio o) → Ordinal.{u_1}
hι : o.card ≤ c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
⊢ (⨆ i, f i + 1).cof ≤ #α

Tactic:
by

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

Goal state before:
pp: a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ a.IsFundamentalSequence a.cof.ord fun i hi ↦ f i ⋯

Tactic:
by

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

Goal state before:
pp: f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}
⊢ 0 ≤ (cof 0).ord

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #↑s ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ (sSup s).card ≤ c

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u}
⊢ (succ o).IsFundamentalSequence 1 fun x x_1 ↦ o

Tactic:
by

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

Goal state before:
pp: s : Set Cardinal.{u}
a : Cardinal.{u}
ha : #↑s < (Cardinal.lift.{u + 1, u} a).ord.cof
hs : ∀ i ∈ s, i < a
⊢ sSup s < a

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ (⨆ i, f i) * c = ⨆ i, c * f i

Tactic:
Cardinal.ciSup_mul f

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ ⨆ i, f i * c = ⨆ i, c * f i
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ c * ⨆ i, f i = ⨆ i, c * f i

Tactic:
by

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

Goal state before:
pp: ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
g : ι' → Cardinal.{v}
⊢ (⨆ i, f i) * ⨆ j, g j = ⨆ i, ⨆ j, f i * g j

Tactic:
by

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

Goal state before:
pp: a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i j : Ordinal.{u}
hi : i < o
hj : j < o
hij : i ≤ j
⊢ f i hi ≤ f j hj

Tactic:
by

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

Goal state before:
pp: β : Type v
f : β → Cardinal.{u}
a : Cardinal.{u}
ha : Cardinal.lift.{u, v} #β < (Cardinal.lift.{v, u} a).ord.cof
hf : ∀ (i : β), f i < a
⊢ ⨆ i, f i < a

Tactic:
by

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

Goal state before:
pp: a✝¹ : Ordinal.{?u.2}
b : Ordinal.{?u.4}
o✝¹ : Ordinal.{?u.6}
a✝ o✝ : Ordinal.{u}
f✝ : (b : Ordinal.{u}) → b < o✝ → Ordinal.{u}
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
i : Ordinal.{u}
hi : i < o'
⊢ g i hi < o

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i < a

Tactic:
by

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

Goal state before:
pp: ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ lift.{u, v} (⨆ i, f i)
⊢ sum f = lift.{u, v} (⨆ i, f i)

Tactic:
by

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

Goal state before:
pp: a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ a.IsFundamentalSequence o' fun i hi ↦ f (g i hi) ⋯

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, f i
⊢ sum f = ⨆ i, f i

Tactic:
by

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

Goal state before:
pp: 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
⊢ #↑S = o.cof

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{u}
h : ∃ o f, a.IsFundamentalSequence o f
⊢ ∃ f, a.IsFundamentalSequence a.cof.ord f

Tactic:
by

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

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
⊢ ℵ_ o₁ + ℵ_ o₂ = ℵ_ (max o₁ o₂)

Tactic:
by

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

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : α ≤ β
⊢ α + γ ≤ β + γ

Tactic:
by

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

Goal state before:
pp: case limit
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

Tactic:
(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isSuccLimit hb

Goal state after:
case limit
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
⊢ (⨆ b_1, a ^ ↑b_1).card ≤ max a.card b.card
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case limit
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

Tactic:
rw [(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isSuccLimit hb]

Goal state after:
case limit
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
⊢ (⨆ b_1, a ^ ↑b_1).card ≤ max a.card b.card
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
by

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

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
⊢ β + γ ≤ α + γ

Tactic:
by

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

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
⊢ α + γ ≤ β + γ ↔ α ≤ β

Tactic:
by

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

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a + c < b + c ↔ a < b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ c + a < c + b ↔ a < b

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
hb : ω ≤ b
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
by

Goal state after:
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 ≤ b

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ lsub f < c

Tactic:
by

Goal state after: