awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
x x_1 x_2 : WellOrder
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
β : Type u
s : β → β → Prop
wo_1 : IsWellOrder β s
h : ⟦{ α := α, r := r, wo := wo : WellOrder.{u} }⟧ ≤ ⟦{ α := β, r := s, wo := wo_1 }⟧
γ : Type u
t : γ → γ → Prop
wo_2 : IsWellOrder γ t
f : InitialSeg r s
a₁ : γ
b₁ : α
a₂ : γ
b₂ : α
h' : t a₁ a₂
⊢ Prod.Lex t s ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) (a₁, b₁))
    ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) (a₂, b₂))

Tactic:
Prod.Lex.left _ _ h'

Premises used: Prod.Lex.left
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
x x_1 x_2 : WellOrder
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
β : Type u
s : β → β → Prop
wo_1 : IsWellOrder β s
h : ⟦{ α := α, r := r, wo := wo : WellOrder.{u} }⟧ ≤ ⟦{ α := β, r := s, wo := wo_1 }⟧
γ : Type u
t : γ → γ → Prop
wo_2 : IsWellOrder γ t
f : InitialSeg r s
a₁ : γ
b₁ : α
a₂ : γ
b₂ : α
h' : t a₁ a₂
⊢ Prod.Lex t s ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) (a₁, b₁))
    ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) (a₂, b₂))

Tactic:
exact Prod.Lex.left _ _ h'

Premises used: Prod.Lex.left
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
x x_1 x_2 : WellOrder
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
β : Type u
s : β → β → Prop
wo_1 : IsWellOrder β s
h : ⟦{ α := α, r := r, wo := wo : WellOrder.{u} }⟧ ≤ ⟦{ α := β, r := s, wo := wo_1 }⟧
γ : Type u
t : γ → γ → Prop
wo_2 : IsWellOrder γ t
f : InitialSeg r s
a_1 : γ
b₁ b₂ : α
h' : r b₁ b₂
⊢ Prod.Lex t s ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) (a_1, b₁))
    ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) (a_1, b₂))

Tactic:
Prod.Lex.right _ (f.toRelEmbedding.map_rel_iff.2 h')

Premises used: Iff.mpr, RelEmbedding.map_rel_iff, Prod.Lex.right, InitialSeg.toRelEmbedding
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
c a b : Ordinal.{u}
x x_1 x_2 : WellOrder
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
β : Type u
s : β → β → Prop
wo_1 : IsWellOrder β s
h : ⟦{ α := α, r := r, wo := wo : WellOrder.{u} }⟧ ≤ ⟦{ α := β, r := s, wo := wo_1 }⟧
γ : Type u
t : γ → γ → Prop
wo_2 : IsWellOrder γ t
f : InitialSeg r s
a_1 : γ
b₁ b₂ : α
h' : r b₁ b₂
⊢ Prod.Lex t s ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) (a_1, b₁))
    ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) (a_1, b₂))

Tactic:
exact Prod.Lex.right _ (f.toRelEmbedding.map_rel_iff.2 h')

Premises used: Iff.mpr, RelEmbedding.map_rel_iff, Prod.Lex.right, InitialSeg.toRelEmbedding
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a * 1 ≤ a * b

Tactic:
mul_le_mul_right (one_le_iff_pos.2 hb) a

Premises used: Iff.mpr, mul_le_mul_right, Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
hb : 0 < b
h : a = a * 1
⊢ a ≤ a * b

Tactic:
convert! mul_le_mul_right (one_le_iff_pos.2 hb) a

Premises used: Iff.mpr, mul_le_mul_right, Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
hb : 0 < b
h h₁ : a = a
⊢ a = a * 1

Tactic:
rw [mul_one a]

Premises used: mul_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
hb : 0 < b
⊢ 1 * a ≤ b * a

Tactic:
mul_le_mul_left (one_le_iff_pos.2 hb) a

Premises used: Iff.mpr, mul_le_mul_left, Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
hb : 0 < b
h : a = 1 * a
⊢ a ≤ b * a

Tactic:
convert! mul_le_mul_left (one_le_iff_pos.2 hb) a

Premises used: Iff.mpr, mul_le_mul_left, Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
hb : 0 < b
h h₁ : a = a
⊢ a = 1 * a

Tactic:
rw [one_mul a]

Premises used: one_mul
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
suffices :
  ∀ (a : α) (b : β),
    Prod.Lex s r (b, a)
      ((enum (Prod.Lex s r) : (a : (↑(Iio (type (Prod.Lex s r))) : Type (u_4 + 1))) → β × α)
        (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type (Prod.Lex s r))) c l))
⊢ False

Tactic:
suffices ∀ a b, Prod.Lex s r (b, a) (enum _ ⟨_, l⟩) from irrefl _ (this _ _)
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
rw :
  ((typein (Prod.Lex s r)).toRelEmbedding (r := Prod.Lex s r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) :
        (a : β × α) → Ordinal.{u_4})
      (b, a) <
    c
⊢ Prod.Lex s r (b, a)
    ((enum (Prod.Lex s r) : (a : (↑(Iio (type (Prod.Lex s r))) : Type (u_4 + 1))) → β × α)
      (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type (Prod.Lex s r))) c l))

Tactic:
rw [← typein_lt_typein (Prod.Lex s r), typein_enum]

Premises used: Ordinal.typein_lt_typein, Prod.Lex, Ordinal.typein_enum
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
⊢ HMul.hMul (β := Ordinal.{u_4}) (type r)
      (succ
          (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4})
            b) :
        Ordinal.{u_4}) ≤
    c

Tactic:
have := H _ (h.succ_lt (typein_lt_type s b))
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this :
  HMul.hMul (β := Ordinal.{u_4}) (type r)
      (succ
          (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4})
            b) :
        Ordinal.{u_4}) ≤
    c
⊢ HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}) +
      type r ≤
    c

Tactic:
rw [mul_succ] at this

Premises used: Ordinal.mul_succ
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this :
  HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}) +
      type r ≤
    c
⊢ HAdd.hAdd (β := Ordinal.{u_4})
      (HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) a :
        Ordinal.{u_4}) <
    c

Tactic:
have := ((add_lt_add_iff_left _).2 (typein_lt_type _ a)).trans_le this
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this_1 :
  HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}) +
      type r ≤
    c
this :
  HAdd.hAdd (β := Ordinal.{u_4})
      (HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) a :
        Ordinal.{u_4}) <
    c
⊢ ((typein (Prod.Lex s r)).toRelEmbedding (r := Prod.Lex s r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) :
        (a : β × α) → Ordinal.{u_4})
      (b, a) <
    c

Tactic:
(RelEmbedding.ofMonotone (fun a => ?_) fun a b => ?_).ordinal_type_le.trans_lt this

Premises used: RelEmbedding.ordinal_type_le, RelEmbedding.ofMonotone, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a_1 : α
b : β
this_1 :
  HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}) +
      type r ≤
    c
this :
  HAdd.hAdd (β := Ordinal.{u_4})
      (HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) a_1 :
        Ordinal.{u_4}) <
    c
a : { x : β × α // Prod.Lex s r x (b, a_1) }
refine_1 : (b' : β) → (a' : α) → (h : Prod.Lex s r (b', a') (b, a_1)) → { x : β // s x b } × α ⊕ { x : α // r x a_1 }
⊢ { x : β // s x b } × α ⊕ { x : α // r x a_1 }

Tactic:
rcases a with ⟨⟨b', a'⟩, h⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h_1 : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this_1 :
  HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}) +
      type r ≤
    c
this :
  HAdd.hAdd (β := Ordinal.{u_4})
      (HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) a :
        Ordinal.{u_4}) <
    c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
pos : (e : b = b') → { x : β // s x b } × α ⊕ { x : α // r x a }
neg : (e : ¬b = b') → { x : β // s x b } × α ⊕ { x : α // r x a }
⊢ { x : β // s x b } × α ⊕ { x : α // r x a }

Tactic:
by_cases e : b = b'
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h_1 : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this_1 :
  HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}) +
      type r ≤
    c
this :
  HAdd.hAdd (β := Ordinal.{u_4})
      (HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) a :
        Ordinal.{u_4}) <
    c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : b = b'
⊢ r a' a

Tactic:
grind [asymm_of s]

Premises used: asymm_of
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h_1 : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this_1 :
  HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}) +
      type r ≤
    c
this :
  HAdd.hAdd (β := Ordinal.{u_4})
      (HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) a :
        Ordinal.{u_4}) <
    c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : b = b'
⊢ { x : β // s x b } × α ⊕ { x : α // r x a }

Tactic:
exact .inr ⟨a', by grind [asymm_of s]⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h_1 : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this_1 :
  HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}) +
      type r ≤
    c
this :
  HAdd.hAdd (β := Ordinal.{u_4})
      (HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) a :
        Ordinal.{u_4}) <
    c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : ¬b = b'
⊢ s b' b

Tactic:
grind
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h_1 : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this_1 :
  HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}) +
      type r ≤
    c
this :
  HAdd.hAdd (β := Ordinal.{u_4})
      (HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4}) b :
          Ordinal.{u_4}))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) a :
        Ordinal.{u_4}) <
    c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : ¬b = b'
⊢ { x : β // s x b } × α ⊕ { x : α // r x a }

Tactic:
exact .inl (⟨b', by grind⟩, a')
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a_1 : α
b_1 : β
this_1 :
  HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4})
            b_1 :
          Ordinal.{u_4}) +
      type r ≤
    c
this :
  HAdd.hAdd (β := Ordinal.{u_4})
      (HMul.hMul (β := Ordinal.{u_4}) (type r)
        (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : β) → Ordinal.{u_4})
            b_1 :
          Ordinal.{u_4}))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) a_1 :
        Ordinal.{u_4}) <
    c
a b : { x : β × α // Prod.Lex s r x (b_1, a_1) }
⊢ Subrel (Prod.Lex s r) (fun (x : β × α) ↦ Prod.Lex s r x (b_1, a_1)) a b →
    Sum.Lex (α := { x : β // s x b_1 } × α) (β := { x : α // r x a_1 }) (Prod.Lex (Subrel s fun (x : β) ↦ s x b_1) r)
      (Subrel r fun (x : α) ↦ r x a_1)
      ((fun (a : { x : β × α // Prod.Lex s r x (b_1, a_1) }) ↦
          (Subtype.casesOn (p := fun (x : β × α) ↦ Prod.Lex s r x (b_1, a_1)) (motive :=
              fun (x : { x : β × α // Prod.Lex s r x (b_1, a_1) }) ↦ { x : β // s x b_1 } × α ⊕ { x : α // r x a_1 }) a
              fun (val : β × α) (h : Prod.Lex s r val (b_1, a_1)) ↦
              Prod.casesOn (motive := fun (x : β × α) ↦
                (h : Prod.Lex s r x (b_1, a_1)) → { x : β // s x b_1 } × α ⊕ { x : α // r x a_1 }) val
                (fun (b' : β) (a' : α) (h : Prod.Lex s r (b', a') (b_1, a_1)) ↦
                  if e : b_1 = b' then Sum.inr (Subtype.mk (p := fun (x : α) ↦ r x a_1) a' ⋯)
                  else Sum.inl (Subtype.mk (p := fun (x : β) ↦ s x b_1) b' ⋯, a'))
                h :
            { x : β // s x b_1 } × α ⊕ { x : α // r x a_1 }))
        a)
      ((fun (a : { x : β × α // Prod.Lex s r x (b_1, a_1) }) ↦
          (Subtype.casesOn (p := fun (x : β × α) ↦ Prod.Lex s r x (b_1, a_1)) (motive :=
              fun (x : { x : β × α // Prod.Lex s r x (b_1, a_1) }) ↦ { x : β // s x b_1 } × α ⊕ { x : α // r x a_1 }) a
              fun (val : β × α) (h : Prod.Lex s r val (b_1, a_1)) ↦
              Prod.casesOn (motive := fun (x : β × α) ↦
                (h : Prod.Lex s r x (b_1, a_1)) → { x : β // s x b_1 } × α ⊕ { x : α // r x a_1 }) val
                (fun (b' : β) (a' : α) (h : Prod.Lex s r (b', a') (b_1, a_1)) ↦
                  if e : b_1 = b' then Sum.inr (Subtype.mk (p := fun (x : α) ↦ r x a_1) a' ⋯)
                  else Sum.inl (Subtype.mk (p := fun (x : β) ↦ s x b_1) b' ⋯, a'))
                h :
            { x : β // s x b_1 } × α ⊕ { x : α // r x a_1 }))
        b)

Tactic:
grind [subrel_val, Sum.Lex.sep, asymm_of s]

Premises used: asymm_of, subrel_val, Sum.Lex.sep
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : IsSuccLimit b
⊢ a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c

Tactic:
⟨fun h _ l ↦ (mul_le_mul_right l.le _).trans h, fun H ↦ le_of_not_gt ?_⟩

Premises used: mul_le_mul_right, le_of_not_gt, LT.lt.le, Iff.intro, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : IsSuccLimit b
refine : ∀ (H : ∀ b' < b, a * b' ≤ c), ¬c < a * b
⊢ a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c

Tactic:
refine ⟨fun h _ l ↦ (mul_le_mul_right l.le _).trans h, fun H ↦ le_of_not_gt ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : IsSuccLimit b
H : ∀ b' < b, a * b' ≤ c
type :
  ∀ (α : Type u_4) (r : α → α → Prop) [inst : IsWellOrder α r] (β : Type u_4) (s : β → β → Prop)
    [inst_1 : IsWellOrder β s] (h : IsSuccLimit (Ordinal.type s)) (H : ∀ b' < Ordinal.type s, Ordinal.type r * b' ≤ c),
    ¬c < Ordinal.type r * Ordinal.type s
⊢ ¬c < a * b

Tactic:
induction a, b using inductionOn₂ with | type α r β s

Premises used: Ordinal.type
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst_1 : IsWellOrder β s
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
⊢ ¬c < type r * type s

Tactic:
mul_le_of_limit_aux h H

Premises used: _private.0.Ordinal.mul_le_of_limit_aux, Not
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst_1 : IsWellOrder β s
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
⊢ ¬c < type r * type s

Tactic:
exact mul_le_of_limit_aux h H

Premises used: _private.0.Ordinal.mul_le_of_limit_aux
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
h : 0 < a
⊢ IsNormal (β := Ordinal.{u_4}) fun (x : Ordinal.{u_4}) ↦ a * x

Tactic:
.of_succ_lt (fun b ↦ ?_) fun hb ↦ ?_

Premises used: Order.IsNormal.of_succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
h : 0 < a
refine_1 : ∀ (b : Ordinal.{u_4}), a * b < a * succ b
refine_2 :
  ∀ {a_1 : Ordinal.{u_4}} (hb : IsSuccLimit a_1), IsLUB ((fun (x : Ordinal.{u_4}) ↦ a * x) '' Iio a_1) (a * a_1)
⊢ IsNormal (β := Ordinal.{u_4}) fun (x : Ordinal.{u_4}) ↦ a * x

Tactic:
refine .of_succ_lt (fun b ↦ ?_) fun hb ↦ ?_
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
h : 0 < a
b : Ordinal.{u_4}
⊢ a * b < a * succ b

Tactic:
simpa [mul_add_one] using (add_lt_add_iff_left (a * b)).2 h

Premises used: Iff.mpr, HMul.hMul, mul_add_one, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
h : 0 < a
a_1 : Ordinal.{u_4}
hb : IsSuccLimit a_1
⊢ IsLUB ((fun (x : Ordinal.{u_4}) ↦ a * x) '' Iio a_1) (a * a_1)

Tactic:
simpa [IsLUB, IsLeast, upperBounds, lowerBounds, mul_le_iff_of_isSuccLimit hb] using
      fun c hc ↦ mul_le_mul_right hc.le a

Premises used: lowerBounds, mul_le_mul_right, upperBounds, IsLeast, IsLUB, Ordinal.mul_le_iff_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : IsSuccLimit c
⊢ a < b * c ↔ ∃ c' < c, a < b * c'

Tactic:
simpa using (mul_le_iff_of_isSuccLimit h).not

Premises used: Iff.not, Ordinal.mul_le_iff_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
inl : a < 0 * (c + 1) ↔ ∃ d < 0, a ≤ 0 * c + d
inr : ∀ (hb : b ≠ 0), a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
⊢ a < 0 * (c + 1) ↔ ∃ d < 0, a ≤ 0 * c + d

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hb : b ≠ 0
inr : a < b * c + b ↔ ∃ d < b, a ≤ b * c + d
inr₁ inr₂ : (∃ d < b, a ≤ b * c + d) ↔ ∃ d < b, a ≤ b * c + d
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

Tactic:
rw [mul_add_one, lt_add_iff hb]

Premises used: Ordinal.lt_add_iff, mul_add_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
a0 : 0 < a
l : IsSuccLimit b
⊢ IsSuccLimit (a * b)

Tactic:
(isNormal_mul_right a0).map_isSuccLimit l

Premises used: Ordinal.isNormal_mul_right, Order.IsNormal.map_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
hb : IsSuccLimit b
inl : IsSuccPrelimit (0 * b)
inr : ∀ (ha : 0 < a), IsSuccPrelimit (a * b)
⊢ IsSuccPrelimit (a * b)

Tactic:
obtain rfl | ha := eq_zero_or_pos a

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b : Ordinal.{u_4}
hb : IsSuccLimit b
inl : IsSuccPrelimit.{u_4 + 1} (α := Ordinal.{u_4}) 0
⊢ IsSuccPrelimit (0 * b)

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit.{u_4 + 1} (α := Ordinal.{u_4}) 0

Tactic:
isSuccPrelimit_zero

Premises used: Ordinal.isSuccPrelimit_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit.{u_4 + 1} (α := Ordinal.{u_4}) 0

Tactic:
exact isSuccPrelimit_zero

Premises used: Ordinal.isSuccPrelimit_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
hb : IsSuccLimit b
ha : 0 < a
⊢ IsSuccPrelimit (a * b)

Tactic:
(isSuccLimit_mul_right ha hb).isSuccPrelimit

Premises used: Order.IsSuccLimit.isSuccPrelimit, Ordinal.isSuccLimit_mul_right
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
hb : IsSuccLimit b
ha : 0 < a
⊢ IsSuccPrelimit (a * b)

Tactic:
exact (isSuccLimit_mul_right ha hb).isSuccPrelimit

Premises used: Order.IsSuccLimit.isSuccPrelimit, Ordinal.isSuccLimit_mul_right