awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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_1 b_1 : Ordinal.{u}
x x_1 x_2 : WellOrder
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
β : Type u
s : β → β → Prop
wo_1 : IsWellOrder β s
h_1 : ⟦{ α := α, 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 : α × γ
h : Prod.Lex r t a b
left :
  ∀ {a₁ : α} (b₁ : γ) {a₂ : α} (b₂ : γ) (h' : r a₁ a₂),
    Prod.Lex s t ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) (a₁, b₁))
      ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) (a₂, b₂))
⊢ Prod.Lex s t ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) a)
    ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) b)
have right : ∀ (a : α) {b₁ b₂ : γ} (h' : t b₁ b₂),
  Prod.Lex s t ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) (a, b₁))
    ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) (a, b₂))
Tactic: obtain ⟨-, -, h'⟩ | ⟨-, h'⟩ := h
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ LE.le (α := Ordinal.{u})
    (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2)
        ⟦{ α := γ, r := t, wo := wo_2 : WellOrder.{u} }⟧ ⟦{ α := α, r := r, wo := wo : WellOrder.{u} }⟧ :
      Ordinal.{u})
    (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2)
        ⟦{ α := γ, r := t, wo := wo_2 : WellOrder.{u} }⟧ ⟦{ α := β, r := s, wo := wo_1 : WellOrder.{u} }⟧ :
      Ordinal.{u})
have a₁ : ∀ (a b : γ × α) (h : Prod.Lex t r a b),
  Prod.Lex t s ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) a)
    ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) b)
Tactic: refine
        (RelEmbedding.ofMonotone (fun a : γ × α => (a.1, f a.2)) fun a b h => ?_).ordinal_type_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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_1 b_1 : Ordinal.{u}
x x_1 x_2 : WellOrder
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
β : Type u
s : β → β → Prop
wo_1 : IsWellOrder β s
h_1 : ⟦{ α := α, 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 : γ × α
h : Prod.Lex t r a b
⊢ Prod.Lex t s ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) a)
    ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) b)
have left : ∀ {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: obtain ⟨-, -, h'⟩ | ⟨-, h'⟩ := h
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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_1 b_1 : Ordinal.{u}
x x_1 x_2 : WellOrder
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
β : Type u
s : β → β → Prop
wo_1 : IsWellOrder β s
h_1 : ⟦{ α := α, 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 : γ × α
h : Prod.Lex t r a b
left :
  ∀ {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₂))
⊢ Prod.Lex t s ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) a)
    ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) b)
have right : ∀ (a : γ) {b₁ b₂ : α} (h' : r b₁ b₂),
  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: obtain ⟨-, -, h'⟩ | ⟨-, h'⟩ := h
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a ≤ a * b
have h : a = a * 1
Tactic: convert! mul_le_mul_right (one_le_iff_pos.2 hb) a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = a * 1
have h : a = a
Tactic: rw [mul_one a]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a ≤ b * a
have h : a = 1 * a
Tactic: convert! mul_le_mul_left (one_le_iff_pos.2 hb) a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = 1 * a
have h : a = a
Tactic: rw [one_mul a]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ False
have 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))
Tactic: suffices ∀ a b, Prod.Lex s r (b, a) (enum _ ⟨_, l⟩) from irrefl _ (this _ _)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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 : β
⊢ 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))
have 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
Tactic: rw [← typein_lt_typein (Prod.Lex s r), typein_enum]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (hypothesis)
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 : β
⊢ ((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
have 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
Tactic: have := H _ (h.succ_lt (typein_lt_type s b))
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (hypothesis)
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
⊢ ((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
have 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
Tactic: rw [mul_succ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (hypothesis)
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
⊢ ((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
have 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
Tactic: have := ((add_lt_add_iff_left _).2 (typein_lt_type _ a)).trans_le this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
have refine_1 : (a_1 : { x : β × α // Prod.Lex s r x (b, a) }) → { x : β // s x b } × α ⊕ { x : α // r x a }
Tactic: refine (RelEmbedding.ofMonotone (fun a => ?_) fun a b => ?_).ordinal_type_le.trans_lt this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
refine_1 : (a_1 : { x : β × α // Prod.Lex s r x (b, a) }) → { x : β // s x b } × α ⊕ { x : α // r x a }
⊢ ((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
have refine_2 : ∀ (a_1 b_1 : { x : β × α // Prod.Lex s r x (b, a) }),
  Subrel (Prod.Lex s r) (fun (x : β × α) ↦ Prod.Lex s r x (b, a)) a_1 b_1 →
    Sum.Lex (α := { x : β // s x b } × α) (β := { x : α // r x a }) (Prod.Lex (Subrel s fun (x : β) ↦ s x b) r)
      (Subrel r fun (x : α) ↦ r x a)
      ((fun (a_3 : { x : β × α // Prod.Lex s r x (b, a) }) ↦
          (Subtype.casesOn (p := fun (x : β × α) ↦ Prod.Lex s r x (b, a)) (motive :=
              fun (x : { x : β × α // Prod.Lex s r x (b, a) }) ↦ { x : β // s x b } × α ⊕ { x : α // r x a }) a_3
              fun (val : β × α) (h : Prod.Lex s r val (b, a)) ↦
              Prod.casesOn (motive := fun (x : β × α) ↦
                (h : Prod.Lex s r x (b, a)) → { x : β // s x b } × α ⊕ { x : α // r x a }) val
                (fun (b' : β) (a' : α) (h : Prod.Lex s r (b', a') (b, a)) ↦
                  if e : b = b' then Sum.inr (Subtype.mk (p := fun (x : α) ↦ r x a) a' sorry)
                  else Sum.inl (Subtype.mk (p := fun (x : β) ↦ s x b) b' sorry, a'))
                h :
            { x : β // s x b } × α ⊕ { x : α // r x a }))
        a_1)
      ((fun (a_3 : { x : β × α // Prod.Lex s r x (b, a) }) ↦
          (Subtype.casesOn (p := fun (x : β × α) ↦ Prod.Lex s r x (b, a)) (motive :=
              fun (x : { x : β × α // Prod.Lex s r x (b, a) }) ↦ { x : β // s x b } × α ⊕ { x : α // r x a }) a_3
              fun (val : β × α) (h : Prod.Lex s r val (b, a)) ↦
              Prod.casesOn (motive := fun (x : β × α) ↦
                (h : Prod.Lex s r x (b, a)) → { x : β // s x b } × α ⊕ { x : α // r x a }) val
                (fun (b' : β) (a' : α) (h : Prod.Lex s r (b', a') (b, a)) ↦
                  if e : b = b' then Sum.inr (Subtype.mk (p := fun (x : α) ↦ r x a) a' sorry)
                  else Sum.inl (Subtype.mk (p := fun (x : β) ↦ s x b) b' sorry, a'))
                h :
            { x : β // s x b } × α ⊕ { x : α // r x a }))
        b_1)
Tactic: refine (RelEmbedding.ofMonotone (fun a => ?_) fun a b => ?_).ordinal_type_le.trans_lt this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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) }
⊢ { x : β // s x b } × α ⊕ { x : α // r x a_1 }
have refine_1 : (b' : β) → (a' : α) → (h : Prod.Lex s r (b', a') (b, a_1)) → { x : β // s x b } × α ⊕ { x : α // r x a_1 }
Tactic: rcases a with ⟨⟨b', a'⟩, h⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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)
⊢ { x : β // s x b } × α ⊕ { x : α // r x a }
have pos : (e : b = b') → { x : β // s x b } × α ⊕ { x : α // r x a }
Tactic: by_cases e : b = b'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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 }
⊢ { x : β // s x b } × α ⊕ { x : α // r x a }
have neg : (e : ¬b = b') → { x : β // s x b } × α ⊕ { x : α // r x a }
Tactic: by_cases e : b = b'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : IsSuccLimit b
⊢ a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c
have refine : ∀ (H : ∀ b' < b, a * b' ≤ c), ¬c < a * b
Tactic: refine ⟨fun h _ l ↦ (mul_le_mul_right l.le _).trans h, fun H ↦ le_of_not_gt ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : IsSuccLimit b
H : ∀ b' < b, a * b' ≤ c
⊢ ¬c < a * b
have type : ∀ (α : 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: induction a, b using inductionOn₂ with | type α r β s
Cleared hypotheses: a, b, h, H
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
h : 0 < a
⊢ IsNormal (β := Ordinal.{u_4}) fun (x : Ordinal.{u_4}) ↦ a * x
have refine_1 : ∀ (b : Ordinal.{u_4}), a * b < a * succ b
Tactic: refine .of_succ_lt (fun b ↦ ?_) fun hb ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
h : 0 < a
refine_1 : ∀ (b : Ordinal.{u_4}), a * b < a * succ b
⊢ IsNormal (β := Ordinal.{u_4}) fun (x : Ordinal.{u_4}) ↦ a * x
have 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)
Tactic: refine .of_succ_lt (fun b ↦ ?_) fun hb ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d
have inl : a < 0 * (c + 1) ↔ ∃ d < 0, a ≤ 0 * c + d
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
inl : a < 0 * (c + 1) ↔ ∃ d < 0, a ≤ 0 * c + d
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d
have inr : ∀ (hb : b ≠ 0), a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d
have inr : a < b * c + b ↔ ∃ d < b, a ≤ b * c + d
Tactic: rw [mul_add_one, lt_add_iff hb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
hb : b ≠ 0
inr : a < b * c + b ↔ ∃ d < b, a ≤ b * c + d
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d
have inr₁ : (∃ d < b, a ≤ b * c + d) ↔ ∃ d < b, a ≤ b * c + d
Tactic: rw [mul_add_one, lt_add_iff hb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit (a * b)
have inl : IsSuccPrelimit (0 * b)
Tactic: obtain rfl | ha := eq_zero_or_pos a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
hb : IsSuccLimit b
inl : IsSuccPrelimit (0 * b)
⊢ IsSuccPrelimit (a * b)
have inr : ∀ (ha : 0 < a), IsSuccPrelimit (a * b)
Tactic: obtain rfl | ha := eq_zero_or_pos a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit (0 * b)
have inl : IsSuccPrelimit.{u_4 + 1} (α := Ordinal.{u_4}) 0
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
⊢ IsSuccLimit (a * b)
have inl : ∀ (b0 : LT.lt.{u_4 + 1} (α := Ordinal.{u_4}) 0 0), IsSuccLimit (a * 0)
Tactic: rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨b, rfl⟩ | lb)
Cleared hypotheses: b, b0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
inl : ∀ (b0 : LT.lt.{u_4 + 1} (α := Ordinal.{u_4}) 0 0), IsSuccLimit (a * 0)
⊢ IsSuccLimit (a * b)
have inr : ∀ (b : Ordinal.{u_4}) (b0 : 0 < succ b), IsSuccLimit (a * succ b)
Tactic: rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨b, rfl⟩ | lb)
Cleared hypotheses: b, b0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
inl : ∀ (b0 : LT.lt.{u_4 + 1} (α := Ordinal.{u_4}) 0 0), IsSuccLimit (a * 0)
inr : ∀ (b : Ordinal.{u_4}) (b0 : 0 < succ b), IsSuccLimit (a * succ b)
⊢ IsSuccLimit (a * b)
have inr₁ : ∀ (lb : IsSuccLimit b), IsSuccLimit (a * b)
Tactic: rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨b, rfl⟩ | lb)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * succ b)
have inr : IsSuccLimit (a * b + a)
Tactic: rw [mul_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit (a * b)
have inl : IsSuccPrelimit (a * 0)
Tactic: obtain rfl | hb := eq_zero_or_pos b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
ha : IsSuccLimit a
inl : IsSuccPrelimit (a * 0)
⊢ IsSuccPrelimit (a * b)
have inr : ∀ (hb : 0 < b), IsSuccPrelimit (a * b)
Tactic: obtain rfl | hb := eq_zero_or_pos b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit (a * 0)
have inl : IsSuccPrelimit.{u_4 + 1} (α := Ordinal.{u_4}) 0
Tactic: rw [mul_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
⊢ HSMul.hSMul (α := ℕ) 0 a = a * (↑0 : Ordinal.{u_4})
have rw : 0 = a * (↑0 : Ordinal.{u_4})
Tactic: rw [zero_nsmul, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
rw : 0 = a * (↑0 : Ordinal.{u_4})
⊢ HSMul.hSMul (α := ℕ) 0 a = a * (↑0 : Ordinal.{u_4})
have rw₁ : 0 = a * 0
Tactic: rw [zero_nsmul, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
rw : 0 = a * (↑0 : Ordinal.{u_4})
rw₁ : 0 = a * 0
⊢ HSMul.hSMul (α := ℕ) 0 a = a * (↑0 : Ordinal.{u_4})
have rw₂ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) 0 0
Tactic: rw [zero_nsmul, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
n : ℕ
a : Ordinal.{u_4}
⊢ (n + 1) • a = a * (↑(n + 1) : Ordinal.{u_4})
have rw : n • a + a = a * (↑(n + 1) : Ordinal.{u_4})
Tactic: rw [succ_nsmul, nsmul_eq_mul, Nat.cast_add_one, mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
n : ℕ
a : Ordinal.{u_4}
rw : n • a + a = a * (↑(n + 1) : Ordinal.{u_4})
⊢ (n + 1) • a = a * (↑(n + 1) : Ordinal.{u_4})
have rw₁ : a * (↑n : Ordinal.{u_4}) + a = a * (↑(n + 1) : Ordinal.{u_4})
Tactic: rw [succ_nsmul, nsmul_eq_mul, Nat.cast_add_one, mul_add_one]