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

Goal state before:
pp: f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ ⨆ i, f (familyOfBFamily' r ?ho✝ g i) = iSup (familyOfBFamily' r ?ho fun a h ↦ f (g a h))

pp: case ho
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ type r = type r

pp: case ho
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ type r = type r

Tactic:
]

Goal state after:
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ ⨆ i, f (familyOfBFamily' r ?ho✝ g i) = iSup (familyOfBFamily' r ?ho fun a h ↦ f (g a h))

case ho
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ type r = type r

case ho
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ type r = type r
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ iSup (o.familyOfBFamily f)
a : Ordinal.{max u v}
⊢ a < iSup (o.familyOfBFamily f) → succ a < iSup (o.familyOfBFamily f)

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ iSup (o.familyOfBFamily f)
a : Ordinal.{max u v}
⊢ a < iSup (o.familyOfBFamily f) → succ a < iSup (o.familyOfBFamily f)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
h : o.bsup f = 0
i : Ordinal.{u_3}
hi : i < o
⊢ f i hi ≤ o.bsup f

Tactic:
]

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
h : o.bsup f = 0
i : Ordinal.{u_3}
hi : i < o
⊢ f i hi ≤ o.bsup f
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
⊢ range f = s

Tactic:
]

Goal state after:
case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
⊢ range f = s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ g j hj ≤ o'.bsup g

Tactic:
]

Goal state after:
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ g j hj ≤ o'.bsup g
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp.refine_1
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ a ≤ a

Tactic:
]

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

Goal state before:
pp: case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding b < typeLT α

Tactic:
]

Goal state after:
case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding b < typeLT α
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
⊢ o ≤ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a ↔ o < typeLT α

Tactic:
]

Goal state after:
case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
⊢ o ≤ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a ↔ o < typeLT α
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < typeLT α
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨o, h⟩ ≤ a

Tactic:
]

Goal state after:
case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < typeLT α
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨o, h⟩ ≤ a
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w✝ : ι
hf : f w✝ = iSup f
⊢ f w✝ < lsub f

Tactic:
]

Goal state after:
case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w✝ : ι
hf : f w✝ = iSup f
⊢ f w✝ < lsub f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_1
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
⊢ ∀ a < iSup f, succ a < iSup f

Tactic:
]

Goal state after:
case refine_1
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
⊢ ∀ a < iSup f, succ a < iSup f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsMax x) ↔ ¬∀ (x : α), ¬IsMax x

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsMax x) ↔ ¬∀ (x : α), ¬IsMax x
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: ⊢ enumOrd (range id) = id

Tactic:
]

Goal state after:
⊢ enumOrd (range id) = id
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
⊢ ?m.88 < succ (iSup f)

Tactic:
]

Goal state after:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
⊢ ?m.88 < succ (iSup f)
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
⊢ sInf (s ∩ {b | ∀ c < 0, enumOrd s c < b}) = sInf s

Tactic:
]

Goal state after:
s : Set Ordinal.{u}
⊢ sInf (s ∩ {b | ∀ c < 0, enumOrd s c < b}) = sInf s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: x : ToType 1
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding ((enum fun x1 x2 ↦ x1 < x2) ⟨0, uniqueToTypeOne._proof_2⟩) = 0

Tactic:
typein_enum

Goal state after:
x : ToType 1
⊢ 0 = 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: x : ToType 1
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
this : lsub f < lsub f
⊢ False

Tactic:
]

Goal state after:
case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
this : lsub f < lsub f
⊢ False
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
i : ι
⊢ f i < lsub f

Tactic:
]

Goal state after:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
i : ι
⊢ f i < lsub f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
a : (succ o).ToType
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a < succ o

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
a : (succ o).ToType
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a < succ o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ ∀ (i : ι), f i < 0

Tactic:
]

Goal state after:
ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ ∀ (i : ι), f i < 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ (∃ d < b, a ≤ b * c + d) ↔ ∃ d < b, a ≤ b * c + d

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : b ≤ 1
n : ℕ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ n < b ^ (2 * fuel)

Tactic:
]

Goal state after:
n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ n < b ^ (2 * fuel)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub f = 0
i : ι
this : 0 < 0
⊢ False

Tactic:
]

Goal state after:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub f = 0
i : ι
this : 0 < 0
⊢ False
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit 0

Tactic:
]

Goal state after:
case inl
b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr.inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * b + a)

Tactic:
]

Goal state after:
case inr.inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * b + a)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
ho : ∀ a < o, succ a < o
⊢ ∀ a < o, succ a < o

Tactic:
]

Goal state after:
o : Ordinal.{u}
ho : ∀ a < o, succ a < o
⊢ ∀ a < o, succ a < o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
ho : IsSuccPrelimit o
⊢ sSup {b | b < (typein fun x1 x2 ↦ x1 < x2).top} = o

Tactic:
]

Goal state after:
o : Ordinal.{u}
ho : IsSuccPrelimit o
⊢ sSup {b | b < (typein fun x1 x2 ↦ x1 < x2).top} = o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
a : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit 0

Tactic:
]

Goal state after:
case inl
a : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit 0
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
⊢ sSup {b | b < (typein fun x1 x2 ↦ x1 < x2).top} = sSup (Iic o)

Tactic:
]

Goal state after:
o : Ordinal.{u_3}
⊢ sSup {b | b < (typein fun x1 x2 ↦ x1 < x2).top} = sSup (Iic o)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.blsub f = o.blsub f

Tactic:
]

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

Goal state before:
pp: n : ℕ
a : Ordinal.{u_4}
⊢ a * ↑n + a = a * ↑n + a

Tactic:
]

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

Goal state before:
pp: case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : type r ≤ type s
⊢ #α ≤ (type s).card

Tactic:
]

Goal state after:
case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : type r ≤ type s
⊢ #α ≤ (type s).card
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ lsub f = lsub f

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
⊢ o.card ≤ c ↔ o.card ≤ c

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c.ord.card

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c.ord.card
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ a * c ≤ a * c

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ iSup (o.familyOfBFamily f) = lsub (o.familyOfBFamily f) ∨
    succ (iSup (o.familyOfBFamily f)) = lsub (o.familyOfBFamily f)

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ iSup (o.familyOfBFamily f) = lsub (o.familyOfBFamily f) ∨
    succ (iSup (o.familyOfBFamily f)) = lsub (o.familyOfBFamily f)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n fuel : ℕ
hb : 1 < b
hn : n ≠ 0
hfuel : n < b ^ fuel
⊢ (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)

Tactic:
induction fuel generalizing b with
  | zero => simp_all
  | succ fuel ih =>
    cases Nat.lt_or_ge n b with
    | inl hnb =>
      simp [go, hnb, one_le_iff_ne_zero, hn]
    | inr hnb =>
      rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb) (go_aux hb hfuel hnb)
        with ⟨ih₁, ih₂, ih₃⟩
      simp_all only [go, if_neg (Nat.not_lt_of_le hnb), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul, Nat.pow_pos (Nat.zero_lt_of_lt hb), Nat.div_div_eq_div_mul,
        ← Nat.pow_add_one, ← Nat.pow_add_one', Nat.mul_add_one]
      split <;> simp_all

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

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
⊢ a * c ≤ a * c

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
⊢ (log.go y b y).snd < x ↔ y < b ^ x

Tactic:
]

Goal state after:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
⊢ (log.go y b y).snd < x ↔ y < b ^ x
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{0}
ho : o < typeLT ℕ
h : Ordinal.lift.{u, 0} o < ω
⊢ ((typein fun x1 x2 ↦ x1 < x2).toRelEmbedding ((enum fun x1 x2 ↦ x1 < x2) ⟨o, ho⟩)).card < ℵ₀

Tactic:
]

Goal state after:
o : Ordinal.{0}
ho : o < typeLT ℕ
h : Ordinal.lift.{u, 0} o < ω
⊢ ((typein fun x1 x2 ↦ x1 < x2).toRelEmbedding ((enum fun x1 x2 ↦ x1 < x2) ⟨o, ho⟩)).card < ℵ₀
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ f w✝¹ w✝ < o.blsub f

Tactic:
]

Goal state after:
case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ f w✝¹ w✝ < o.blsub f
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case add_one
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
IH : (a + b) * (c + 1) = a * (c + 1) + b
⊢ a * (c + 1 + 1) + b = a * (c + 1 + 1) + b

Tactic:
]

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

Goal state before:
pp: case refine_1
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ Ordinal.lift.{?u.37, v} a < Ordinal.lift.{?u.37, v} c.ord

Tactic:
]

Goal state after:
case refine_1
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ Ordinal.lift.{?u.37, v} a < Ordinal.lift.{?u.37, v} c.ord
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case limit
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
l : IsSuccLimit c
IH : ∀ o' < c, (a + b) * (o' + 1) = a * (o' + 1) + b
⊢ a * c + (a + b) = a * c + (a + b)

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ iSup (o.familyOfBFamily f) = lsub (o.familyOfBFamily f) ↔
    ∀ a < lsub (o.familyOfBFamily f), succ a < lsub (o.familyOfBFamily f)

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ iSup (o.familyOfBFamily f) = lsub (o.familyOfBFamily f) ↔
    ∀ a < lsub (o.familyOfBFamily f), succ a < lsub (o.familyOfBFamily f)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_2
c : Cardinal.{v}
⊢ lift.{u, v} c ≤ lift.{u, v} c

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o + o = o + o

Tactic:
]

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ (typein r).toRelEmbedding x < type r

Tactic:
]

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ (typein r).toRelEmbedding x < type r
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : o.bsup f = o.blsub f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < o.blsub f

Tactic:
]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : o.bsup f = o.blsub f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < o.blsub f
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a / b ≤ a / b

Tactic:
]

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ 0 < a ↔ 0 < a

Tactic:
]

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ ℵ₀ ≤ a ↔ ℵ₀ ≤ a

Tactic:
]

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

Goal state before:
pp: a b c : Ordinal.{u_4}
b0 : b ≠ 0
⊢ a < b * succ c ↔ a < b * succ c

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u}
ho : IsSuccLimit o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯
⊢ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f

Tactic:
]

Goal state after:
o : Ordinal.{u}
ho : IsSuccLimit o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯
⊢ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
⊢ a ≤ ℵ₀ ↔ a ≤ ℵ₀

Tactic:
]

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

Goal state before:
pp: c : Cardinal.{u_1}
h : c ≠ 0
⊢ ¬c = 0

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
h : c ≠ 0
⊢ ¬c = 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : c ≠ 0
⊢ c * succ a ≤ b ↔ c * succ a ≤ b

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑n ≤ o ↔ ↑n ≤ o

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ω ≤ o ↔ ω ≤ o

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ IsEmpty o.ToType ↔ o = 0

Tactic:
]

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ IsEmpty o.ToType ↔ o = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl.inr
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n < b ↔ n < b

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑(n + 1) ≤ o ↔ succ ↑n ≤ o

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
n : ℕ
⊢ ↑(n + 1) ≤ o ↔ succ ↑n ≤ o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : (a : Ordinal.{u_3}) → a < 0 → Ordinal.{max u_3 u_4}
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inl
a b : Ordinal.{u_4}
h : a ≤ b
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ c * (a / c) ≤ b

Tactic:
]

Goal state after:
case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ c * (a / c) ≤ b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (h : i < type r), f i h < o) ↔ ∀ (i : α), f ((typein r).toRelEmbedding i) ⋯ < o

Tactic:
]

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (h : i < type r), f i h < o) ↔ ∀ (i : α), f ((typein r).toRelEmbedding i) ⋯ < o
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < lift.{v, u} (succ a).ord
⊢ b ∈ range lift.{v, u}

Tactic:
]

Goal state after:
a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < lift.{v, u} (succ a).ord
⊢ b ∈ range lift.{v, u}
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝¹ : IsWellOrder α r
inst✝ : Fintype α
⊢ ↑(Fintype.card α) = ↑(Fintype.card α)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ b ≤ n ∧ 1 < b ↔ b ≤ n ∧ 1 < b

Tactic:
]

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ ∃ p, #↑p = #↑s

Tactic:
]

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ ∃ p, #↑p = #↑s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ #↑s < #↑univ

Tactic:
]

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ #↑s < #↑univ
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ c < b * (c / b) + b

Tactic:
]

Goal state after:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ c < b * (c / b) + b
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ #↑s ≤ #↑s

Tactic:
]

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

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * (c / b) ≤ c

Tactic:
]

Goal state after:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * (c / b) ≤ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : a < b
⊢ a < b * succ 0

Tactic:
]

Goal state after:
a b : Ordinal.{u_4}
h : a < b
⊢ a < b * succ 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
⊢ 0 = 0

Tactic:
]

Goal state after: