mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LinearOrder α
⊢ DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : LinearOrder α
⊢ DirSupInaccOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
⊢ Module.Finite R≥0 R

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LinearOrder α
⊢ DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
hb : b₁ < b₂
⊢ a • b₁ < a • b₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : CompleteLattice α
⊢ DirSupClosedOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d ⊆ s → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → sSup d ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : CompleteLattice α
⊢ DirSupInaccOn D s ↔
    ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : CompleteLattice α
⊢ DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → sSup d ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
h : a • b₁ ≤ a • b₂
⊢ a • f b₁ ≤ a • f b₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : CompleteLattice α
⊢ DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₁ • b ≤ a₂ • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • b < a₂ • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b ≤ a₂ • b
⊢ a₁ ≤ a₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
⊢ a₁ < a₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ IsNormal f ↔ StrictMono f ∧ ∀ (o : α), IsSuccLimit o → ∀ (a : β), (∀ b < o, f b ≤ a) → f o ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : IsNormal f
a : α
ha : IsSuccLimit a
⊢ IsLUB (f '' Iio a) (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
⊢ f a ≤ b ↔ ∀ a' < a, f a' ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
⊢ b < f a ↔ ∃ a' < a, b < f a'

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ IsSuccLimit (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
⊢ f a ∈ upperBounds (f '' s)

pp: case refine_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
⊢ f a ≤ b

Tactic:
· simpa [mem_upperBounds, hf.strictMono.le_iff_le] using hs.1

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
⊢ f a ≤ b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
⊢ IsLUB (f '' s) (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α ≤i β
a✝ : α
ha : IsSuccLimit a✝
⊢ f a✝ ∈ lowerBounds (upperBounds (⇑f '' Iio a✝))

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
⊢ IsNormal (g ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
a : α
⊢ IsNormal fun x ↦ ⟨f ↑x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst✝ : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ ⨆ n, f^[n] a ∈ Function.fixedPoints f

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
⊢ f ⁻¹' Iic x = Iic (sSup (f ⁻¹' Iic x))

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ f a = ⨆ b, f ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : SuccOrder α
inst✝ : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
⊢ IsNormal f

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
⊢ f = g ↔ f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
⊢ ∃ a, f a ≤ x ∧ x < f (succ a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ (f ⁻¹' s).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
⊢ DirSupClosed (range f)

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (b : Ordinal.{max (u + 1) v}), b ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ b < univ.{u, v}

Tactic:
by

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

Goal state before:
pp: ⊢ liftPrincipalSeg.top = typeLT Ordinal.{u}

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{u + 1, u} c < univ.{u, u + 1}

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
by

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

Goal state before:
pp: ⊢ ℵ₀ < univ.{u, v}

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ ?m.25 < Ordinal.liftPrincipalSeg.top

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
⊢ ?m.46 < Ordinal.liftPrincipalSeg.top

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
c' : Cardinal.{u}
h' : lift.{u + 1, u} c' < univ.{u, u + 1}
e : lift.{v, u + 1} (lift.{u + 1, u} c') = c
⊢ c = lift.{max (u + 1) v, u} c'

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{max (u + 1) v}
h✝ : c < Cardinal.univ.{u, v}
w : Cardinal.{u}
h : c = lift.{max (u + 1) v, u} w
⊢ 2 ^ c = lift.{max (u + 1) v, u} (2 ^ w)

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ Small.{v, u} α ↔ lift.{v + 1, u} #α < univ.{v, max u (v + 1)}

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{v}
⊢ lift.{u, v} (a + 1) = lift.{u, v} a + 1

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
a : γ
⊢ f (Sum.inl a) = Sum.inl a

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
a : α
⊢ ∃ b, f (Sum.inr a) = Sum.inr b

Tactic:
by

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ type r = 0 ↔ IsEmpty α

Tactic:
by

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ type r ≠ 0 ↔ Nonempty α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
⊢ c + a ≤ c + b → a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal.{u_4}
h : (fun x ↦ a + x) b = (fun x ↦ a + x) c
⊢ b = c

Tactic:
by

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝² : IsWellOrder α r
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
⊢ type r = 1

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a + b < a + c ↔ b < c

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a + ↑0 ≤ b + ↑0 ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ IsEmpty o.ToType ↔ o = 0

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
n : ℕ
⊢ a + ↑(n + 1) ≤ b + ↑(n + 1) ↔ a ≤ b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ type (Sum.Lex r s) = 0 ↔ type r = 0 ∧ type s = 0

Tactic:
type_eq_zero_iff_isEmpty

Goal state after:
a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ Nonempty o.ToType ↔ o ≠ 0

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ type r + type s = 0 ↔ type r = 0 ∧ type s = 0

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_4}
h : IsSuccLimit o
n : ℕ
⊢ ↑n < o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o = 0 ∨ o ∈ range succ ∨ IsSuccLimit o

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ typeLT ℕ ≤ (cof ℕ).ord

Tactic:
by

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

Goal state before:
pp: α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ∃ y, r x y

Tactic:
by

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

Goal state before:
pp: δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
    [inst_3 : WellFoundedLT β], typeLT α = typeLT β → f α = f β
γ : Type u_1
inst✝¹ : LinearOrder γ
inst✝ : WellFoundedLT γ
⊢ (typeLT γ).liftOnWellOrder f c = f γ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Subsingleton α
⊢ typeLT α ≤ (cof α).ord

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
⊢ typeLT ↑s ≤ typeLT α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s t : Set α
h : s ⊆ t
⊢ typeLT ↑s ≤ typeLT ↑t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x : α
⊢ Bounded r {x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ typeLT Ordinal.{u_2} ≤ (cof Ordinal.{u_2}).ord

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α ≤ β
⊢ α.ToType ≤i β.ToType

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a.pred ≤ b ↔ a ≤ succ b

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o.pred ≤ o

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ (cof α).ord = typeLT α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ∀ (b : Ordinal.{?u.26}), b ≤ (succ b).pred

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ cof α = #α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ (#α).ord = typeLT α

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α < β
⊢ α.ToType <i β.ToType

Tactic:
by

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

Goal state before:
pp: ⊢ cof Ordinal.{u} = Cardinal.univ.{u, u + 1}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ ∀ (a b : { x // x ∈ s }), a < b → ↑a < ↑b

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o.pred = o ↔ IsSuccPrelimit o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o.pred < o ↔ ¬IsSuccPrelimit o

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ typeLT ↑s = typeLT α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
a o : α
ho : o ∈ s
H : ∀ b < a, ↑((enum s hs) b) < o
⊢ ↑((enum s hs) a) ≤ o

Tactic:
← Subtype.coe_mk o ho,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
a o : α
ho : o ∈ s
H : ∀ b < a, ↑((enum s hs) b) < o
⊢ ↑((enum s hs) a) ≤ ↑⟨o, ho⟩
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ succ o.pred = o ↔ ¬IsSuccPrelimit o

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ r ≺i fun x1 x2 ↦ x1 < x2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
a o : α
ho : o ∈ s
H : ∀ b < a, ↑((enum s hs) b) < o
⊢ ↑((enum s hs) a) ≤ o

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
inst✝ : SuccOrder α
a o : α
ha : o ∈ s
H : ↑((enum s hs) a) < o
⊢ ↑((enum s hs) (succ a)) ≤ o

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{v}
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
by

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
⊢ (typein r).toRelEmbedding a ≤ (typein r).toRelEmbedding b ↔ ¬r b a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
x : α
⊢ (enum Set.univ ⋯) x = ⟨x, ⋯⟩

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≤ a
⊢ b + (a - b) = a

Tactic:
by

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : ↑(Iio (type r))
⊢ ¬r ((enum r) o₁) ((enum r) o₂) ↔ o₂ ≤ o₁

Tactic:
by

Goal state after: