awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
h₁ :
  x =
    (enum r : (a : (↑(Iio (type r)) : Type (u_4 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
            x)
          ⋯ :
        { x : Ordinal.{u_4} // x ∈ Iio (type r) })
h₂ : (↑(Iio (type r)) : Type (u_4 + 1))
h₃ :
  LT.lt (α := (↑(Iio (type r)) : Type (u_4 + 1)))
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x)
        ⋯ :
      { x : Ordinal.{u_4} // x ∈ Iio (type r) })
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
        (succ
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
            x))
        ⋯ :
      { x : Ordinal.{u_4} // x ∈ Iio (type r) })
⊢ r x
    ((enum r : (a : (↑(Iio (type r)) : Type (u_4 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
              x))
          ⋯ :
        { x : Ordinal.{u_4} // x ∈ Iio (type r) }))

Tactic:
convert! enum_lt_enum.mpr _

Premises used: Iff.mpr, Ordinal.enum_lt_enum
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
h₁ : x = x
h₂ : α
h₃ : x = x
h₄ : α
⊢ x =
    (enum r : (a : (↑(Iio (type r)) : Type (u_4 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
            x)
          ⋯ :
        { x : Ordinal.{u_4} // x ∈ Iio (type r) })

Tactic:
rw [enum_typein]

Premises used: Ordinal.enum_typein
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
h₁ :
  LT.lt (α := Ordinal.{u_4})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x :
      Ordinal.{u_4})
    (succ
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
          x) :
      Ordinal.{u_4})
h₂ h₃ :
  LE.le (α := Ordinal.{u_4})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x :
      Ordinal.{u_4})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x :
      Ordinal.{u_4})
⊢ LT.lt (α := (↑(Iio (type r)) : Type (u_4 + 1)))
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x)
        ⋯ :
      { x : Ordinal.{u_4} // x ∈ Iio (type r) })
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
        (succ
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
            x))
        ⋯ :
      { x : Ordinal.{u_4} // x ∈ Iio (type r) })

Tactic:
rw [Subtype.mk_lt_mk, lt_succ_iff]

Premises used: Subtype.mk_lt_mk, Order.lt_succ_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
ho : ∀ a < o, succ a < o
⊢ NoMaxOrder.{u_4} o.ToType

Tactic:
⟨has_succ_of_type_succ_lt (type_toType _ ▸ ho)⟩

Premises used: Ordinal.has_succ_of_type_succ_lt, NoMaxOrder.mk
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
hr : IsSuccLimit (type r)
x : α
⊢ Bounded r {x}

Tactic:
⟨enum r ⟨succ (typein r x), hr.succ_lt (typein_lt_type r x)⟩, ?_⟩

Premises used: Order.succ, Set.Bounded, PrincipalSeg.toRelEmbedding, Ordinal.typein_lt_type, Order.IsSuccLimit.succ_lt, Subtype.mk, Exists.intro, Ordinal.enum, DFunLike.coe, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
hr : IsSuccLimit (type r)
x : α
refine :
  ∀ (b : α),
    Membership.mem (γ := Set α) {x} b →
      r b
        ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
          (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
              (succ
                (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) :
                    (a : α) → Ordinal.{u_1})
                  x))
              ⋯ :
            { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
⊢ Bounded r {x}

Tactic:
refine ⟨enum r ⟨succ (typein r x), hr.succ_lt (typein_lt_type r x)⟩, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : Membership.mem (γ := Set α) {x} b
rw :
  r x
    ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
              x))
          ⋯ :
        { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
⊢ r b
    ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
              x))
          ⋯ :
        { x : Ordinal.{u_1} // x ∈ Iio (type r) }))

Tactic:
rw [mem_singleton_iff.1 hb]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : Membership.mem (γ := Set α) {x} b
nth_rw :
  r
    ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
            x)
          ⋯ :
        { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
    ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
              x))
          ⋯ :
        { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
⊢ r x
    ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
              x))
          ⋯ :
        { x : Ordinal.{u_1} // x ∈ Iio (type r) }))

Tactic:
nth_rw 1 [← enum_typein r x]

Premises used: Ordinal.enum_typein
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : Membership.mem (γ := Set α) {x} b
rw :
  LT.lt (α := Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) x :
      Ordinal.{u_1})
    (succ
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
          x) :
      Ordinal.{u_1})
⊢ r
    ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
            x)
          ⋯ :
        { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
    ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
              x))
          ⋯ :
        { x : Ordinal.{u_1} // x ∈ Iio (type r) }))

Tactic:
rw [@enum_lt_enum _ r, Subtype.mk_lt_mk]

Premises used: Ordinal.enum_lt_enum, Subtype.mk_lt_mk
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : Membership.mem (γ := Set α) {x} b
⊢ LT.lt (α := Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) x :
      Ordinal.{u_1})
    (succ
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
          x) :
      Ordinal.{u_1})

Tactic:
apply lt_succ

Premises used: Order.lt_succ
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
⊢ (o + 1).pred = o

Tactic:
isSuccPrelimitRecOn_succ ..

Premises used: Order.succ, Order.isSuccPrelimitRecOn_succ, Ordinal.pred
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
⊢ (succ o).pred = o

Tactic:
pred_add_one o

Premises used: Order.succ, Ordinal.pred_add_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
⊢ IsSuccPrelimit o → o.pred = o

Tactic:
isSuccPrelimitRecOn_of_isSuccPrelimit _ _

Premises used: Order.isSuccPrelimitRecOn_of_isSuccPrelimit, Ordinal.pred
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
ho : IsSuccLimit o
⊢ o.pred = o

Tactic:
ho.isSuccPrelimit.ordinalPred_eq

Premises used: Order.IsSuccPrelimit.ordinalPred_eq, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ pred 0 = 0

Tactic:
isSuccPrelimit_zero.ordinalPred_eq

Premises used: Ordinal.isSuccPrelimit_zero, Order.IsSuccPrelimit.ordinalPred_eq
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
inl : ∀ (a : Ordinal.{u_4}), (succ a).pred ≤ b ↔ succ a ≤ succ b
inr : ∀ (ha : IsSuccPrelimit a), a.pred ≤ b ↔ a ≤ succ b
⊢ a.pred ≤ b ↔ a ≤ succ b

Tactic:
obtain ⟨a, rfl⟩ | ha := mem_range_succ_or_isSuccPrelimit a

Premises used: Order.mem_range_succ_or_isSuccPrelimit, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b a : Ordinal.{u_4}
⊢ (succ a).pred ≤ b ↔ succ a ≤ succ b

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
inr : a ≤ b ↔ a ≤ succ b
inr₁ inr₂ : a ≤ b ↔ a ≤ b
⊢ a.pred ≤ b ↔ a ≤ succ b

Tactic:
rw [ha.ordinalPred_eq, ha.le_succ_iff]

Premises used: Order.IsSuccPrelimit.le_succ_iff, Order.IsSuccPrelimit.ordinalPred_eq
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ a < b.pred ↔ succ a < b

Tactic:
le_iff_le_iff_lt_iff_lt.1 pred_le_iff_le_succ

Premises used: le_iff_le_iff_lt_iff_lt, Ordinal.pred_le_iff_le_succ, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
⊢ o.pred ≤ o

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ∀ (b : Ordinal.{u_4}), b ≤ (succ b).pred

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ Surjective pred

Tactic:
pred_succ_gi.l_surjective

Premises used: Ordinal.pred_succ_gi, GaloisInsertion.l_surjective
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
⊢ o ≤ succ o.pred

Tactic:
pred_succ_gi.gc.le_u_l o

Premises used: GaloisConnection.le_u_l, Ordinal.pred_succ_gi, GaloisInsertion.gc
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
inl : ∀ (a : Ordinal.{u_4}), (succ a).pred = succ a ↔ IsSuccPrelimit (succ a)
inr : ∀ (ho : IsSuccPrelimit o), o.pred = o ↔ IsSuccPrelimit o
⊢ o.pred = o ↔ IsSuccPrelimit o

Tactic:
obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o

Premises used: Order.mem_range_succ_or_isSuccPrelimit, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ (succ a).pred = succ a ↔ IsSuccPrelimit (succ a)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
ho : IsSuccPrelimit o
inr : True ↔ IsSuccPrelimit o
⊢ o.pred = o ↔ IsSuccPrelimit o

Tactic:
simp_rw [ho.ordinalPred_eq, ho]

Premises used: Order.IsSuccPrelimit.ordinalPred_eq
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
rw : o.pred ≠ o ↔ ¬IsSuccPrelimit o
⊢ o.pred < o ↔ ¬IsSuccPrelimit o

Tactic:
rw [(pred_le_self o).lt_iff_ne]

Premises used: Ordinal.pred_le_self, LE.le.lt_iff_ne
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
⊢ o.pred ≠ o ↔ ¬IsSuccPrelimit o

Tactic:
pred_eq_iff_isSuccPrelimit.not

Premises used: Iff.not, Ordinal.pred_eq_iff_isSuccPrelimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
⊢ o.pred ≠ o ↔ ¬IsSuccPrelimit o

Tactic:
exact pred_eq_iff_isSuccPrelimit.not

Premises used: Iff.not, Ordinal.pred_eq_iff_isSuccPrelimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
rw : succ o.pred ≤ o ↔ ¬IsSuccPrelimit o
rw₁ : o.pred < o ↔ ¬IsSuccPrelimit o
rw₂ rw₃ : ¬IsSuccPrelimit o ↔ ¬IsSuccPrelimit o
⊢ succ o.pred = o ↔ ¬IsSuccPrelimit o

Tactic:
rw [← (self_le_succ_pred o).ge_iff_eq', succ_le_iff, pred_lt_iff_not_isSuccPrelimit]

Premises used: Ordinal.pred_lt_iff_not_isSuccPrelimit, LE.le.ge_iff_eq', Order.succ_le_iff, Ordinal.self_le_succ_pred
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{v}
inl : ∀ (a : Ordinal.{v}), lift.{u, v} (succ a).pred = (lift.{u, v} (succ a)).pred
inr : ∀ (ho : IsSuccPrelimit o), lift.{u, v} o.pred = (lift.{u, v} o).pred
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o

Premises used: Order.mem_range_succ_or_isSuccPrelimit, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{v}
⊢ lift.{u, v} (succ a).pred = (lift.{u, v} (succ a)).pred

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{v}
ho : IsSuccPrelimit o
inr : lift.{u, v} o = (lift.{u, v} o).pred
inr₁ : (lift.{u, v} o).pred = lift.{u, v} o
inr₂ : IsSuccPrelimit (lift.{u, v} o)
inr₃ inr₄ inr₅ inr₆ : IsSuccPrelimit o
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
rwa [ho.ordinalPred_eq, eq_comm, pred_eq_iff_isSuccPrelimit, isSuccPrelimit_lift]

Premises used: eq_comm, Ordinal.pred_eq_iff_isSuccPrelimit, Ordinal.isSuccPrelimit_lift, Order.IsSuccPrelimit.ordinalPred_eq
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : Ordinal.IsNormal f
o : Ordinal.{u_4}
⊢ IsSuccLimit o → ∀ {a : Ordinal.{u_5}}, f o ≤ a ↔ ∀ b < o, f b ≤ a

Tactic:
H.le_iff_forall_le

Premises used: Order.IsNormal.le_iff_forall_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : Ordinal.IsNormal f
o : Ordinal.{u_4}
h : IsSuccLimit o
a : Ordinal.{u_5}
⊢ a < f o ↔ ∃ b < o, a < f b

Tactic:
H.lt_iff_exists_lt h

Premises used: Order.IsNormal.lt_iff_exists_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : Ordinal.IsNormal f
⊢ StrictMono f

Tactic:
Order.IsNormal.strictMono H

Premises used: Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : Ordinal.IsNormal f
⊢ Monotone f

Tactic:
H.strictMono.monotone

Premises used: StrictMono.monotone, Ordinal.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
⊢ Ordinal.IsNormal f ↔
    StrictMono f ∧ ∀ (o : Ordinal.{u_4}), IsSuccLimit o → ∀ (a : Ordinal.{u_5}), (∀ b < o, f b ≤ a) → f o ≤ a

Tactic:
isNormal_iff

Premises used: Ordinal.IsNormal, Order.isNormal_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : Ordinal.IsNormal f
a b : Ordinal.{u_4}
⊢ f a < f b ↔ a < b

Tactic:
H.strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Ordinal.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : Ordinal.IsNormal f
a b : Ordinal.{u_4}
⊢ f a ≤ f b ↔ a ≤ b

Tactic:
H.strictMono.le_iff_le

Premises used: Ordinal.IsNormal.strictMono, StrictMono.le_iff_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : Ordinal.IsNormal f
a b : Ordinal.{u_4}
⊢ f a = f b ↔ a = b

Tactic:
H.strictMono.injective.eq_iff

Premises used: Function.Injective.eq_iff, StrictMono.injective, Ordinal.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_4}
H : Ordinal.IsNormal f
⊢ id ≤ f

Tactic:
H.strictMono.id_le

Premises used: Ordinal.IsNormal.strictMono, StrictMono.id_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_4}
H : Ordinal.IsNormal f
a : Ordinal.{u_4}
⊢ a ≤ f a

Tactic:
H.strictMono.le_apply

Premises used: StrictMono.le_apply, Ordinal.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_4}
H : Ordinal.IsNormal f
a : Ordinal.{u_4}
⊢ f a ≤ a ↔ f a = a

Tactic:
H.le_apply.ge_iff_eq'

Premises used: Ordinal.IsNormal.le_apply, LE.le.ge_iff_eq'
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : Ordinal.IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
b : Ordinal.{u_4}
H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o
⊢ IsLUB (f '' p) (f b)

Tactic:
have hp := H.map_isLUB ⟨(H₂ b).1 le_rfl, fun a ↦ (H₂ _).2⟩ p0
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : Ordinal.IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
b : Ordinal.{u_4}
H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o
hp : IsLUB (f '' p) (f b)
⊢ f b ≤ o ↔ ∀ a ∈ p, f a ≤ o

Tactic:
⟨fun hb a ha ↦ (hp.1 (mem_image_of_mem _ ha)).trans hb, fun H ↦ hp.2 ?_⟩

Premises used: And.right, And.left, Set.mem_image_of_mem, Iff.intro, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : Ordinal.IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
b : Ordinal.{u_4}
H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o
hp : IsLUB (f '' p) (f b)
refine : ∀ (H : ∀ a ∈ p, f a ≤ o), o ∈ upperBounds (f '' p)
⊢ f b ≤ o ↔ ∀ a ∈ p, f a ≤ o

Tactic:
refine ⟨fun hb a ha ↦ (hp.1 (mem_image_of_mem _ ha)).trans hb, fun H ↦ hp.2 ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H_1 : Ordinal.IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
b : Ordinal.{u_4}
H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o
hp : IsLUB (f '' p) (f b)
H : ∀ a ∈ p, f a ≤ o
⊢ o ∈ upperBounds (f '' p)

Tactic:
simpa [mem_upperBounds]

Premises used: mem_upperBounds
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : Ordinal.IsNormal f
p : Set α
p0 : p.Nonempty
g : α → Ordinal.{u_4}
b : Ordinal.{u_4}
H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, g a ≤ o
⊢ f b ≤ o ↔ ∀ a ∈ p, f (g a) ≤ o

Tactic:
simpa [H₂] using H.le_set (g '' p) (p0.image g) b

Premises used: Set.Nonempty.image, Set.image, Ordinal.IsNormal.le_set
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ Ordinal.IsNormal.{u_4, u_4} id

Tactic:
.id

Premises used: Ordinal.IsNormal, Order.IsNormal.id
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
g : Ordinal.{u_6} → Ordinal.{u_4}
H₁ : Ordinal.IsNormal f
H₂ : Ordinal.IsNormal g
⊢ IsNormal (f ∘ g)

Tactic:
H₁.comp H₂

Premises used: Order.IsNormal.comp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : Ordinal.IsNormal f
o : Ordinal.{u_4}
ho : IsSuccLimit o
⊢ IsSuccLimit (f o)

Tactic:
H.map_isSuccLimit ho

Premises used: Order.IsNormal.map_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a < b
⊢ a - b = 0

Tactic:
dif_neg h.not_ge

Premises used: dif_neg, LT.lt.not_ge
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : b ≤ a
change : (b + if h : b ≤ a then Classical.choose (p := fun (x : Ordinal.{u_4}) ↦ a = b + x) ⋯ else 0) = a
⊢ b + (a - b) = a

Tactic:
change b + dite _ _ _ = a

Premises used: dite
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : b ≤ a
rw : b + Classical.choose (p := fun (x : Ordinal.{u_4}) ↦ a = b + x) ⋯ = a
⊢ (b + if h : b ≤ a then Classical.choose (p := fun (x : Ordinal.{u_4}) ↦ a = b + x) ⋯ else 0) = a

Tactic:
rw [dif_pos h]

Premises used: dif_pos
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : b ≤ a
⊢ b + Classical.choose (p := fun (x : Ordinal.{u_4}) ↦ a = b + x) ⋯ = a

Tactic:
(Classical.choose_spec (exists_add_of_le h)).symm

Premises used: ExistsAddOfLE.exists_add_of_le, Classical.choose_spec, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : b ≤ a
⊢ b + Classical.choose (p := fun (x : Ordinal.{u_4}) ↦ a = b + x) ⋯ = a

Tactic:
exact (Classical.choose_spec (exists_add_of_le h)).symm

Premises used: ExistsAddOfLE.exists_add_of_le, Classical.choose_spec, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ a + b - a = b

Tactic:
simpa using Ordinal.add_sub_cancel_of_le le_self_add

Premises used: Ordinal.add_sub_cancel_of_le, le_self_add
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
inl : ∀ (h : b ≤ a), a ≤ b + (a - b)
inr : ∀ (h : a < b), a ≤ b + (a - b)
⊢ a ≤ b + (a - b)

Tactic:
obtain h | h := le_or_gt b a

Premises used: le_or_gt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : b ≤ a
⊢ a ≤ b + (a - b)

Tactic:
(Ordinal.add_sub_cancel_of_le h).ge

Premises used: Eq.ge, Ordinal.add_sub_cancel_of_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : b ≤ a
⊢ a ≤ b + (a - b)

Tactic:
exact (Ordinal.add_sub_cancel_of_le h).ge

Premises used: Eq.ge, Ordinal.add_sub_cancel_of_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a < b
⊢ a ≤ b + (a - b)

Tactic:
simpa [sub_eq_zero_of_lt h] using h.le

Premises used: LT.lt.le, _private.0.Ordinal.sub_eq_zero_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : a - b ≤ c
⊢ b + (a - b) ≤ b + c

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
refine : ∀ (h : a ≤ b + c), a - b ≤ c
⊢ a - b ≤ c ↔ a ≤ b + c

Tactic:
refine ⟨fun h ↦ (le_add_sub a b).trans (by gcongr), fun h ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : a ≤ b + c
inl : ∀ (h' : b ≤ a), a - b ≤ c
inr : ∀ (h' : a < b), a - b ≤ c
⊢ a - b ≤ c

Tactic:
obtain h' | h' := le_or_gt b a

Premises used: le_or_gt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : b ≤ a
inl : b + (a - b) ≤ b + c
inl₁ inl₂ inl₃ inl₄ : a ≤ b + c
⊢ a - b ≤ c

Tactic:
rwa [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h']

Premises used: add_le_add_iff_left, Ordinal.add_sub_cancel_of_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : a < b
⊢ a - b ≤ c

Tactic:
simp [sub_eq_zero_of_lt h']

Premises used: _private.0.Ordinal.sub_eq_zero_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
⊢ a < b - c ↔ c + a < b

Tactic:
lt_iff_lt_of_le_iff_le sub_le

Premises used: Ordinal.sub_le, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : a + b = c
⊢ c - a = b

Tactic:
h ▸ add_sub_cancel _ _

Premises used: Eq.rec, Ordinal.add_sub_cancel
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ a - b ≤ a

Tactic:
sub_le.2 le_add_self

Premises used: Iff.mpr, Ordinal.sub_le, le_add_self
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : b ≤ a
rw : b + c ≤ b + (a - b) ↔ b + c ≤ a
rw₁ rw₂ : b + c ≤ a ↔ b + c ≤ a
⊢ c ≤ a - b ↔ b + c ≤ a

Tactic:
rw [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h]

Premises used: add_le_add_iff_left, Ordinal.add_sub_cancel_of_le