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

Goal state before:
pp: case succ.inr
α : 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)
a b : α
hb : ¬IsMax b
IH : a < b → f a < f b
hab : a < succ b
h : a < b
⊢ f a < f (succ b)

Tactic:
·

Goal state after:
case succ.inr
α : 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)
a b : α
hb : ¬IsMax b
IH : a < b → f a < f b
hab : a < succ b
h : a < b
⊢ f a < f (succ b)
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case mp
α : 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)

pp: case mpr
α : 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 ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)) → f = g

Tactic:
·

Goal state after:
case mp
α : 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)
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_1
α : 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
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ f (sSup (f ⁻¹' Iic x)) ≤ x

pp: case refine_2
α : 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
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))

Tactic:
·

Goal state after:
case refine_1
α : 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
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ f (sSup (f ⁻¹' Iic x)) ≤ x
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_2
α : 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
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))

Tactic:
·

Goal state after:
case refine_2
α : 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
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

pp: case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding

Tactic:
·

Goal state after:
case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding

Tactic:
·

Goal state after:
case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr.type.refine_1
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ β → α

pp: case mpr.type.refine_2
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ ∀ (a b : β), s a b → r (?mpr.type.refine_1 a) (?mpr.type.refine_1 b)

pp: case mpr.type.refine_3
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ Function.Surjective ⇑(RelEmbedding.ofMonotone ?mpr.type.refine_1 ?mpr.type.refine_2)

Tactic:
·

Goal state after:
case mpr.type.refine_1
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ β → α
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr.type.refine_2
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ ∀ (a b : β), s a b → r ((enum r) ⟨f a, ⋯⟩) ((enum r) ⟨f b, ⋯⟩)

pp: case mpr.type.refine_3
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ Function.Surjective ⇑(RelEmbedding.ofMonotone (fun b ↦ (enum r) ⟨f b, ⋯⟩) ?mpr.type.refine_2)

Tactic:
·

Goal state after:
case mpr.type.refine_2
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ ∀ (a b : β), s a b → r ((enum r) ⟨f a, ⋯⟩) ((enum r) ⟨f b, ⋯⟩)
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr.type.refine_3
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ Function.Surjective ⇑(RelEmbedding.ofMonotone (fun b ↦ (enum r) ⟨f b, ⋯⟩) ⋯)

Tactic:
·

Goal state after:
case mpr.type.refine_3
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ Function.Surjective ⇑(RelEmbedding.ofMonotone (fun b ↦ (enum r) ⟨f b, ⋯⟩) ⋯)
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mp
α : Type u
⊢ Small.{v, u} α → ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

pp: case mpr
α : Type u
⊢ (∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c') → Small.{v, u} α

Tactic:
·

Goal state after:
case mp
α : Type u
⊢ Small.{v, u} α → ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr
α : Type u
⊢ (∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c') → Small.{v, u} α

Tactic:
·

Goal state after:
case mpr
α : Type u
⊢ (∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c') → Small.{v, u} α
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
α✝ : 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 : α
x : γ
hx : f (Sum.inr a) = Sum.inl x
⊢ ∃ b, Sum.inl x = Sum.inr b

pp: case inr
α✝ : 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 : α
x : β
hx : f (Sum.inr a) = Sum.inr x
⊢ ∃ b, Sum.inr x = Sum.inr b

Tactic:
·

Goal state after:
case inl
α✝ : 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 : α
x : γ
hx : f (Sum.inr a) = Sum.inl x
⊢ ∃ b, Sum.inl x = Sum.inr b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
α✝ : 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 : α
x : β
hx : f (Sum.inr a) = Sum.inr x
⊢ ∃ b, Sum.inr x = Sum.inr b

Tactic:
·

Goal state after:
case inr
α✝ : 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 : α
x : β
hx : f (Sum.inr a) = Sum.inr x
⊢ ∃ b, Sum.inr x = Sum.inr b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case e'_1
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ x = (enum r) ?h.convert_4

pp: case h.convert_4
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ↑(Iio (type r))

pp: case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ?h.convert_4 < ⟨succ ((typein r).toRelEmbedding x), ⋯⟩

Tactic:
·

Goal state after:
case e'_1
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ x = (enum r) ?h.convert_4
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

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

pp: case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Subsingleton α
h✝ : Nonempty α
⊢ typeLT α ≤ (cof α).ord

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Subsingleton α
h✝ : IsEmpty α
⊢ typeLT α ≤ (cof α).ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

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

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Subsingleton α
h✝ : Nonempty α
⊢ typeLT α ≤ (cof α).ord
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ⟨(typein r).toRelEmbedding x, ⋯⟩ < ⟨succ ((typein r).toRelEmbedding x), ⋯⟩

Tactic:
·

Goal state after:
case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ⟨(typein r).toRelEmbedding x, ⋯⟩ < ⟨succ ((typein r).toRelEmbedding x), ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
⊢ a.pred ≤ b ↔ a ≤ succ b

Tactic:
·

Goal state after:
case inl
b a : Ordinal.{u_4}
⊢ (succ a).pred ≤ b ↔ succ a ≤ succ b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

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

Tactic:
ord_le,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ cof α ≤ (typeLT α).card
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
·

Goal state after:
case inr
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
⊢ a.pred ≤ b ↔ a ≤ succ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
obtain ⟨a, rfl⟩ | ha := mem_range_succ_or_isSuccPrelimit a
  · simp
  · rw [ha.ordinalPred_eq, ha.le_succ_iff]

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

Goal state before:
pp: case inl
a : Ordinal.{u_4}
⊢ (succ a).pred = succ a ↔ IsSuccPrelimit (succ a)

pp: case inr
o : Ordinal.{u_4}
ho : IsSuccPrelimit o
⊢ o.pred = o ↔ IsSuccPrelimit o

Tactic:
·

Goal state after:
case inl
a : Ordinal.{u_4}
⊢ (succ a).pred = succ a ↔ IsSuccPrelimit (succ a)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
·

Goal state after:
case inr
o : Ordinal.{u_4}
ho : IsSuccPrelimit o
⊢ o.pred = o ↔ IsSuccPrelimit o
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ ∀ (a_1 : { x // r x a }), (PrincipalSeg.ofElement r a).toRelEmbedding a_1 ∈ fun x ↦ r x b

pp: case refine_2
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ (PrincipalSeg.ofElement r a).top ∈ fun x ↦ r x b

pp: case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) → a < type r

pp: case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)

Tactic:
·

Goal state after:
case refine_1
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ ∀ (a_1 : { x // r x a }), (PrincipalSeg.ofElement r a).toRelEmbedding a_1 ∈ fun x ↦ r x b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ (#α).ord ≤ type fun x1 x2 ↦ x1 < x2

Tactic:
ord_le,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ #α ≤ (type fun x1 x2 ↦ x1 < x2).card
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ (PrincipalSeg.ofElement r a).top ∈ fun x ↦ r x b

pp: case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) → a < type r

pp: case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)

Tactic:
·

Goal state after:
case refine_2
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ (PrincipalSeg.ofElement r a).top ∈ fun x ↦ r x b
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) → a < type r

pp: case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)

Tactic:
·

Goal state after:
case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) → a < type r
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)

Tactic:
·

Goal state after:
case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
a : Ordinal.{v}
⊢ lift.{u, v} (succ a).pred = (lift.{u, v} (succ a)).pred

pp: case inr
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
·

Goal state after:
case inl
a : Ordinal.{v}
⊢ lift.{u, v} (succ a).pred = (lift.{u, v} (succ a)).pred
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
·

Goal state after:
case inr
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
a b : Ordinal.{u_4}
h : a < b
⊢ a ≤ b + (a - b)

Tactic:
·

Goal state after:
case inl
a b : Ordinal.{u_4}
h : b ≤ a
⊢ a ≤ b + (a - b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
·

Goal state after:
case inr
a b : Ordinal.{u_4}
h : a < b
⊢ a ≤ b + (a - b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : b ≤ a
⊢ a - b ≤ c

pp: case inr
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : a < b
⊢ a - b ≤ c

Tactic:
·

Goal state after:
case inl
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : b ≤ a
⊢ a - b ≤ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: case mp
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ Subtype.val ∘ ⇑(enum s hs) = f → StrictMono f ∧ range f = s

pp: case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ StrictMono f ∧ range f = s → Subtype.val ∘ ⇑(enum s hs) = f

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ Subtype.val ∘ ⇑(enum s hs) = f → StrictMono f ∧ range f = s
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : a < b
⊢ a - b ≤ c

Tactic:
·

Goal state after:
case inr
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : a < b
⊢ a - b ≤ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ StrictMono f ∧ range f = s → Subtype.val ∘ ⇑(enum s hs) = f

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ StrictMono f ∧ range f = s → Subtype.val ∘ ⇑(enum s hs) = f