awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₂ : Ordinal.{u_1}
hcomm : AddCommute 0 o₂
ih :
  ∀ y < 0 + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : 0 ≤ o₂
⊢ o₂ * (↑0 : Ordinal.{u_1}) = 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₂ : Ordinal.{u_1}
hcomm : AddCommute 0 o₂
ih :
  ∀ y < 0 + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : 0 ≤ o₂
⊢ o₂ * (↑1 : Ordinal.{u_1}) = o₂

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₂ : Ordinal.{u_1}
hcomm : AddCommute 0 o₂
ih :
  ∀ y < 0 + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : 0 ≤ o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = 0 ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂

Tactic:
exact ⟨o₂, 0, 1, by simp, by simp⟩
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
⊢ o₁ + o₃ = o₂

Tactic:
have hsub : o₁ + o₃ = o₂ := Ordinal.add_sub_cancel_of_le hle
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
⊢ o₁ + (o₁ + o₃) = o₁ + (o₃ + o₁)

Tactic:
grind
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
⊢ AddCommute o₁ o₃

Tactic:
have hcomm' : AddCommute o₁ o₃ := add_left_cancel (a := o₁) <| by grind
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
⊢ o₁ + o₃ < o₁ + o₂

Tactic:
simpa [hsub, hcomm.eq] using h₁.pos

Premises used: Ne.pos, AddCommute.eq
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
⊢ o₁ + o₃ < o₁ + o₂

Tactic:
have hlt : o₁ + o₃ < o₁ + o₂ := by simpa [hsub, hcomm.eq] using h₁.pos
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
inr :
  ∀ (o : Ordinal.{u_1}) (n₁ n₃ : ℕ) (hn₁ : o * (↑n₁ : Ordinal.{u_1}) = o₁) (hn₃ : o * (↑n₃ : Ordinal.{u_1}) = o₃),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂

Tactic:
rcases ih _ hlt hcomm' rfl with ⟨o, n₁, n₃, hn₁, hn₃⟩

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * (↑n₁ : Ordinal.{u_1}) = o₁
hn₃ : o * (↑n₃ : Ordinal.{u_1}) = o₃
right : o * (↑(n₁ + n₃) : Ordinal.{u_1}) = o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂

Tactic:
use o, n₁, n₁ + n₃, hn₁
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * (↑n₁ : Ordinal.{u_1}) = o₁
hn₃ : o * (↑n₃ : Ordinal.{u_1}) = o₃
right : o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₃ : Ordinal.{u_1}) = o₂
right₁ : o * (↑n₁ : Ordinal.{u_1}) + o * (↑n₃ : Ordinal.{u_1}) = o₂
right₂ : o₁ + o * (↑n₃ : Ordinal.{u_1}) = o₂
right₃ : o₁ + o₃ = o₂
right₄ right₅ : o₂ = o₂
⊢ o * (↑(n₁ + n₃) : Ordinal.{u_1}) = o₂

Tactic:
rw [Nat.cast_add, mul_add, hn₁, hn₃, hsub]

Premises used: Nat.cast_add, mul_add
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o : Ordinal.{u_1}
n₁ n₂ : ℕ
refine_2 : o * (↑n₁ : Ordinal.{u_1}) + o * (↑n₂ : Ordinal.{u_1}) = o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
refine_2₁ :
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) =
    o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
refine_2₂ :
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) =
    o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
refine_2₃ :
  o * (↑(n₁ + n₂) : Ordinal.{u_1}) = o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
refine_2₄ :
  o * (↑(n₂ + n₁) : Ordinal.{u_1}) = o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
refine_2₅ refine_2₆ :
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) =
    o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
⊢ AddCommute (o * (↑n₁ : Ordinal.{u_1})) (o * (↑n₂ : Ordinal.{u_1}))

Tactic:
rw [addCommute_iff_eq, ← mul_add, ← mul_add, ← Nat.cast_add, add_comm, Nat.cast_add]

Premises used: addCommute_iff_eq, add_comm, Nat.cast_add, mul_add
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
o a : Ordinal.{u}
s : Set Ordinal.{u}
ha : a ∈ s
H : ∀ b < o, enumOrd s b < a
rw : sInf (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}) ≤ a
⊢ enumOrd s o ≤ a

Tactic:
rw [enumOrd]

Premises used: Ordinal.enumOrd
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
o a : Ordinal.{u}
s : Set Ordinal.{u}
ha : a ∈ s
H : ∀ b < o, enumOrd s b < a
⊢ sInf (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}) ≤ a

Tactic:
csInf_le' ⟨ha, H⟩

Premises used: csInf_le', And.intro
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
o a : Ordinal.{u}
s : Set Ordinal.{u}
ha : a ∈ s
H : ∀ b < o, enumOrd s b < a
⊢ sInf (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}) ≤ a

Tactic:
exact csInf_le' ⟨ha, H⟩
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
rw :
  ∀ (hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y) (o : Ordinal.{u}),
    (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty
⊢ (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
rw [not_bddAbove_iff] at hs

Premises used: not_bddAbove_iff
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o : Ordinal.{u}
obtain :
  ∀ (a : Ordinal.{u}) (ha : a ∈ upperBounds (enumOrd s '' Iio o)),
    (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty
⊢ (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
obtain ⟨a, ha⟩ := bddAbove_of_small (s := enumOrd s '' Iio o)

Premises used: Ordinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o a : Ordinal.{u}
ha : a ∈ upperBounds (enumOrd s '' Iio o)
obtain : ∀ (b : Ordinal.{u}) (hb : b ∈ s) (hba : a < b), (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty
⊢ (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
obtain ⟨b, hb, hba⟩ := hs a
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o a : Ordinal.{u}
ha : a ∈ upperBounds (enumOrd s '' Iio o)
b : Ordinal.{u}
hb : b ∈ s
hba : a < b
⊢ (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
⟨b, hb, fun c hc ↦ (ha (mem_image_of_mem _ hc)).trans_lt hba⟩

Premises used: Ordinal.enumOrd, Set.Nonempty, Set.mem_image_of_mem, And.intro, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o a : Ordinal.{u}
ha : a ∈ upperBounds (enumOrd s '' Iio o)
b : Ordinal.{u}
hb : b ∈ s
hba : a < b
⊢ (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
exact ⟨b, hb, fun c hc ↦ (ha (mem_image_of_mem _ hc)).trans_lt hba⟩
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
rw : sInf (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}) ∈ s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}
⊢ enumOrd s o ∈ s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}

Tactic:
rw [enumOrd]

Premises used: Ordinal.enumOrd
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ sInf (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}) ∈ s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}

Tactic:
csInf_mem (enumOrd_nonempty hs o)

Premises used: csInf_mem, _private.0.Ordinal.enumOrd_nonempty
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ sInf (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}) ∈ s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}

Tactic:
exact csInf_mem (enumOrd_nonempty hs o)

Premises used: csInf_mem, _private.0.Ordinal.enumOrd_nonempty
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ enumOrd s o ∈ s

Tactic:
(enumOrd_mem_aux hs o).1

Premises used: And.left, _private.0.Ordinal.enumOrd_mem_aux
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono (enumOrd s)

Tactic:
fun a b ↦ (enumOrd_mem_aux hs b).2 a

Premises used: StrictMono, And.right, _private.0.Ordinal.enumOrd_mem_aux
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ Function.Injective (enumOrd s)

Tactic:
(enumOrd_strictMono hs).injective

Premises used: StrictMono.injective, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a b : Ordinal.{u}
⊢ enumOrd s a = enumOrd s b ↔ a = b

Tactic:
(enumOrd_injective hs).eq_iff

Premises used: Function.Injective.eq_iff, Ordinal.enumOrd_injective
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a b : Ordinal.{u}
⊢ enumOrd s a ≤ enumOrd s b ↔ a ≤ b

Tactic:
(enumOrd_strictMono hs).le_iff_le

Premises used: StrictMono.le_iff_le, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a b : Ordinal.{u}
⊢ enumOrd s a < enumOrd s b ↔ a < b

Tactic:
(enumOrd_strictMono hs).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ id ≤ enumOrd s

Tactic:
(enumOrd_strictMono hs).id_le

Premises used: StrictMono.id_le, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
⊢ a ≤ enumOrd s a

Tactic:
(enumOrd_strictMono hs).le_apply

Premises used: StrictMono.le_apply, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
apply : ∀ b_1 < succ b, enumOrd s b_1 < a
⊢ enumOrd s (succ b) ≤ a

Tactic:
apply enumOrd_le_of_forall_lt ha

Premises used: Ordinal.enumOrd_le_of_forall_lt
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
c : Ordinal.{u}
hc : c < succ b
⊢ c ≤ b

Tactic:
rw [lt_succ_iff] at hc

Premises used: Order.lt_succ_iff
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
c : Ordinal.{u}
hc : c ≤ b
⊢ enumOrd s c < a

Tactic:
((enumOrd_strictMono hs).monotone hc).trans_lt hb

Premises used: StrictMono.monotone, LE.le.trans_lt, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
c : Ordinal.{u}
hc : c ≤ b
⊢ enumOrd s c < a

Tactic:
exact ((enumOrd_strictMono hs).monotone hc).trans_lt hb

Premises used: StrictMono.monotone, LE.le.trans_lt, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
h : ∀ (a : Ordinal.{u}), a ∈ range (enumOrd s) ↔ a ∈ s
⊢ range (enumOrd s) = s

Tactic:
ext a
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
h : a ∈ range (enumOrd s) → a ∈ s
h₁ : a ∈ s → a ∈ range (enumOrd s)
⊢ a ∈ range (enumOrd s) ↔ a ∈ s

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
t : Set Ordinal.{u} := {b_1 : Ordinal.{u} | enumOrd s b ≤ enumOrd s b_1}
⊢ enumOrd s b ∈ s

Tactic:
enumOrd_mem hs b

Premises used: Ordinal.enumOrd_mem
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
t : Set Ordinal.{u} := {b_1 : Ordinal.{u} | enumOrd s b ≤ enumOrd s b_1}
⊢ enumOrd s b ∈ s

Tactic:
exact enumOrd_mem hs b

Premises used: Ordinal.enumOrd_mem
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ∈ range (enumOrd s)

Tactic:
⟨sInf t, (enumOrd_le_of_forall_lt ha ?_).antisymm ?_⟩

Premises used: Set.Mem, setOf, LE.le.antisymm, Ordinal.enumOrd_le_of_forall_lt, Exists.intro, Set.range, InfSet.sInf
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
ha : a ∈ s
h : ∀ b < sInf t, enumOrd s b < a
h₁ : a ≤ enumOrd s (sInf t)
⊢ a ∈ range (enumOrd s)

Tactic:
refine ⟨sInf t, (enumOrd_le_of_forall_lt ha ?_).antisymm ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
ha : a ∈ s
b : Ordinal.{u}
hb : b < sInf t
h : ∀ (hb' : a ≤ enumOrd s b), False
⊢ enumOrd s b < a

Tactic:
by_contra! hb'
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
ha : a ∈ s
b : Ordinal.{u}
hb : b < sInf t
hb' : a ≤ enumOrd s b
⊢ False

Tactic:
hb.not_ge (csInf_le' hb')

Premises used: csInf_le', LT.lt.not_ge
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
ha : a ∈ s
b : Ordinal.{u}
hb : b < sInf t
hb' : a ≤ enumOrd s b
⊢ False

Tactic:
exact hb.not_ge (csInf_le' hb')

Premises used: csInf_le', LT.lt.not_ge
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ≤ enumOrd s (sInf t)

Tactic:
csInf_mem (s := t) ⟨a, (enumOrd_strictMono hs).id_le a⟩

Premises used: csInf_mem, Set.Mem, setOf, Exists.intro, StrictMono.id_le, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ≤ enumOrd s (sInf t)

Tactic:
exact csInf_mem (s := t) ⟨a, (enumOrd_strictMono hs).id_le a⟩

Premises used: csInf_mem, Exists.intro, StrictMono.id_le, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
hb : b ∈ s
rwa rwa₁ rwa₂ rwa₃ : ∀ (hb : b ∈ range (enumOrd s)), ∃ (a : Ordinal.{u}), enumOrd s a = b
⊢ ∃ (a : Ordinal.{u}), enumOrd s a = b

Tactic:
rwa [← range_enumOrd hs] at hb

Premises used: Ordinal.range_enumOrd
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
rw : sInf (t ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd t c < b}) ≤ sInf (s ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd s c < b})
⊢ enumOrd t a ≤ enumOrd s a

Tactic:
rw [enumOrd, enumOrd]

Premises used: Ordinal.enumOrd
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
h₁ : (s ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd s c < b}).Nonempty
h₂ : ∀ (b c : Ordinal.{u}), c < a → enumOrd t c ≤ enumOrd s c
⊢ sInf (t ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd t c < b}) ≤ sInf (s ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd s c < b})

Tactic:
gcongr with b c
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ (s ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd s c < b}).Nonempty

Tactic:
enumOrd_nonempty hs a

Premises used: _private.0.Ordinal.enumOrd_nonempty
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a b c : Ordinal.{u}
h : c < a
⊢ enumOrd t c ≤ enumOrd s c

Tactic:
enumOrd_le_of_subset hs hst c
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ (s ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd s c < b}).Nonempty

Tactic:
exacts [enumOrd_nonempty hs a, enumOrd_le_of_subset hs hst c]

Premises used: _private.0.Ordinal.enumOrd_nonempty
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
mp : enumOrd s = f → StrictMono f ∧ range f = s
mpr : StrictMono f ∧ range f = s → enumOrd s = f
⊢ enumOrd s = f ↔ StrictMono f ∧ range f = s

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono (enumOrd s) ∧ range (enumOrd s) = s

Tactic:
⟨enumOrd_strictMono hs, range_enumOrd hs⟩

Premises used: And.intro, Ordinal.range_enumOrd, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono (enumOrd s) ∧ range (enumOrd s) = s

Tactic:
exact ⟨enumOrd_strictMono hs, range_enumOrd hs⟩
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
mpr : range (enumOrd s) = range f
mpr₁ : s = range f
mpr₂ mpr₃ mpr₄ mpr₅ : range f = s
⊢ enumOrd s = f

Tactic:
rwa [← (enumOrd_strictMono hs).range_inj h₁, range_enumOrd hs, eq_comm]

Premises used: eq_comm, StrictMono.range_inj, Ordinal.range_enumOrd, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : StrictMono f
⊢ enumOrd (range f) = f

Tactic:
(eq_enumOrd _ hf.not_bddAbove_range_of_wellFoundedLT).2 ⟨hf, rfl⟩

Premises used: Iff.mpr, StrictMono.not_bddAbove_range_of_wellFoundedLT, And.intro, rfl, Ordinal.eq_enumOrd
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
⊢ IsNormal (enumOrd s)

Tactic:
isNormal_iff.2 ⟨enumOrd_strictMono hs, fun o ho a ha ↦ ?_⟩

Premises used: Iff.mpr, And.intro, Order.isNormal_iff, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
refine : ∀ (o : Ordinal.{u}) (ho : IsSuccLimit o) (a : Ordinal.{u}) (ha : ∀ b < o, enumOrd s b ≤ a), enumOrd s o ≤ a
⊢ IsNormal (enumOrd s)

Tactic:
refine isNormal_iff.2 ⟨enumOrd_strictMono hs, fun o ho a ha ↦ ?_⟩

Premises used: Iff.mpr, And.intro, Order.isNormal_iff, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
trans : enumOrd s o ≤ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u})
trans₁ : ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u}) ≤ a
⊢ enumOrd s o ≤ a

Tactic:
trans ⨆ b : Iio o, enumOrd s b

Premises used: Set.Iio
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ enumOrd s o ≤ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u})

Tactic:
enumOrd_le_of_forall_lt ?_ (fun b hb ↦ (enumOrd_strictMono hs (lt_succ b)).trans_le ?_)

Premises used: Order.lt_succ, Ordinal.enumOrd_le_of_forall_lt, LT.lt.trans_le, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
refine_1 : ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u}) ∈ s
refine_2 :
  ∀ (b : Ordinal.{u}) (hb : b < o), enumOrd s (succ b) ≤ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u})
⊢ enumOrd s o ≤ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u})

Tactic:
refine enumOrd_le_of_forall_lt ?_ (fun b hb ↦ (enumOrd_strictMono hs (lt_succ b)).trans_le ?_)

Premises used: Order.lt_succ, Ordinal.enumOrd_le_of_forall_lt, LT.lt.trans_le, Ordinal.enumOrd_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ Nonempty.{u + 2} (↑(Iio o) : Type (u + 1))

Tactic:
have : Nonempty (Iio o) := ⟨0, ho.bot_lt⟩
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
this : Nonempty.{u + 2} (↑(Iio o) : Type (u + 1))
apply : (range fun (b : (↑(Iio o) : Type (u + 1))) ↦ enumOrd s (↑b : Ordinal.{u})) ⊆ s
⊢ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u}) ∈ s

Tactic:
apply H _ _ (range_nonempty _) bddAbove_of_small

Premises used: Ordinal.bddAbove_of_small, Set.range_nonempty
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
this : Nonempty.{u + 2} (↑(Iio o) : Type (u + 1))
c : (↑(Iio o) : Type (u + 1))
⊢ (fun (b : (↑(Iio o) : Type (u + 1))) ↦ enumOrd s (↑b : Ordinal.{u})) c ∈ s

Tactic:
enumOrd_mem hs c

Premises used: Set.Mem, Ordinal.enumOrd_mem, Subtype.val