awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : b ≤ a
⊢ a - b < c ↔ a < b + c

Tactic:
lt_iff_lt_of_le_iff_le (le_sub_of_le h)

Premises used: Ordinal.le_sub_of_le, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ a - 0 = a

Tactic:
simpa only [zero_add] using add_sub_cancel 0 a

Premises used: Ordinal.add_sub_cancel, zero_add, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ 0 - a = 0

Tactic:
simpa using sub_le_self 0 _

Premises used: Ordinal.sub_le_self, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ a - a = 0

Tactic:
simpa only [add_zero] using add_sub_cancel a 0

Premises used: Ordinal.add_sub_cancel, add_zero, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ a - b = 0 ↔ a ≤ b

Tactic:
simp [← nonpos_iff_eq_zero, sub_le]

Premises used: Ordinal.sub_le, nonpos_iff_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ a - b ≠ 0 ↔ b < a

Tactic:
simpa using Ordinal.sub_eq_zero_iff_le.not

Premises used: Ordinal.sub_eq_zero_iff_le, Iff.not
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c d : Ordinal.{u_4}
rw : a - b ≤ c + d ↔ a - (b + c) ≤ d
rw₁ : a ≤ b + (c + d) ↔ a - (b + c) ≤ d
rw₂ : a ≤ b + (c + d) ↔ a ≤ b + c + d
rw₃ rw₄ : a ≤ b + (c + d) ↔ a ≤ b + (c + d)
⊢ a - b - c ≤ d ↔ a - (b + c) ≤ d

Tactic:
rw [sub_le, sub_le, sub_le, add_assoc]

Premises used: add_assoc, Ordinal.sub_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
rw : a + b - a - c = b - c
rw₁ rw₂ : b - c = b - c
⊢ a + b - (a + c) = b - c

Tactic:
rw [← sub_sub, add_sub_cancel]

Premises used: Ordinal.add_sub_cancel, Ordinal.sub_sub
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : b + c ≤ a
rw : b + c ≤ b + (a - b)
⊢ c ≤ a - b

Tactic:
rw [← add_le_add_iff_left b]

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

Tactic:
h.trans (le_add_sub a b)

Premises used: LE.le.trans, Ordinal.le_add_sub
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : b + c ≤ a
⊢ b + c ≤ b + (a - b)

Tactic:
exact h.trans (le_add_sub a b)

Premises used: LE.le.trans, Ordinal.le_add_sub
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
inl : ∀ (hab : a < b), a - b < c
inr : ∀ (hba : b ≤ a), a - b < c
⊢ a - b < c

Tactic:
obtain hab | hba := lt_or_ge a b

Premises used: lt_or_ge
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hab : a < b
inl inl₁ inl₂ inl₃ : 0 < c
⊢ a - b < c

Tactic:
rwa [Ordinal.sub_eq_zero_iff_le.2 hab.le]

Premises used: Iff.mpr, Ordinal.sub_eq_zero_iff_le, LT.lt.le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hba : b ≤ a
inr inr₁ inr₂ inr₃ : a < b + c
⊢ a - b < c

Tactic:
rwa [sub_lt_of_le hba]

Premises used: Ordinal.sub_lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : c ≠ 0
mpr : (∃ d < c, a ≤ b + d) → a < b + c
⊢ a < b + c ↔ ∃ d < c, a ≤ b + d

Tactic:
use fun h ↦ ⟨_, sub_lt_of_lt_add h hc.bot_lt, le_add_sub a b⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : c ≠ 0
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ b + d < b + c

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : c ≠ 0
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ a < b + c

Tactic:
exact ha.trans_lt (by gcongr)

Premises used: LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a + b ≤ c ↔ ∀ d < b, a + d < c

Tactic:
simpa using (lt_add_iff hb).not

Premises used: Ordinal.lt_add_iff, Iff.not
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
rw : (∃ d < c, a ≤ b + d) ↔ ∃ d < c, a < b + d
⊢ a < b + c ↔ ∃ d < c, a < b + d

Tactic:
rw [lt_add_iff hc.ne_bot]

Premises used: Order.IsSuccLimit.ne_bot, Ordinal.lt_add_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
mp : (∃ d < c, a ≤ b + d) → ∃ d < c, a < b + d
mpr : (∃ d < c, a < b + d) → ∃ d < c, a ≤ b + d
⊢ (∃ d < c, a ≤ b + d) ↔ ∃ d < c, a < b + d

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ ∃ d < c, a < b + d

Tactic:
⟨_, hc.succ_lt hd, ?_⟩

Premises used: Order.IsSuccLimit.succ_lt, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
mp : a < b + succ d
⊢ ∃ d < c, a < b + d

Tactic:
refine ⟨_, hc.succ_lt hd, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
mp : a < b + (d + 1)
mp₁ : a < b + d + 1
mp₂ mp₃ mp₄ mp₅ : a ≤ b + d
⊢ a < b + succ d

Tactic:
rwa [succ_eq_add_one, ← add_assoc, lt_add_one_iff]

Premises used: Order.succ_eq_add_one, add_assoc, Order.lt_add_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a < b + d
⊢ ∃ d < c, a ≤ b + d

Tactic:
⟨d, hd, ha.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a < b + d
⊢ ∃ d < c, a ≤ b + d

Tactic:
exact ⟨d, hd, ha.le⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ a + b ≤ c ↔ ∀ d < b, a + d ≤ c

Tactic:
simpa using (lt_add_iff_of_isSuccLimit hb).not

Premises used: Ordinal.lt_add_iff_of_isSuccLimit, Iff.not
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
rw :
  (StrictMono (β := Ordinal.{u_4}) fun (x : Ordinal.{u_4}) ↦ a + x) ∧
    ∀ (o : Ordinal.{u_4}), IsSuccLimit o → ∀ (a_2 : Ordinal.{u_4}), (∀ b < o, a + b ≤ a_2) → a + o ≤ a_2
⊢ IsNormal (β := Ordinal.{u_4}) fun (x : Ordinal.{u_4}) ↦ a + x

Tactic:
rw [isNormal_iff]

Premises used: Order.isNormal_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ (StrictMono (β := Ordinal.{u_4}) fun (x : Ordinal.{u_4}) ↦ a + x) ∧
    ∀ (o : Ordinal.{u_4}), IsSuccLimit o → ∀ (a_2 : Ordinal.{u_4}), (∀ b < o, a + b ≤ a_2) → a + o ≤ a_2

Tactic:
⟨add_right_strictMono, fun _ l _ ↦ (add_le_iff_of_isSuccLimit l).2⟩

Premises used: add_right_strictMono, Iff.mpr, Ordinal.add_le_iff_of_isSuccLimit, And.intro
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ (StrictMono (β := Ordinal.{u_4}) fun (x : Ordinal.{u_4}) ↦ a + x) ∧
    ∀ (o : Ordinal.{u_4}), IsSuccLimit o → ∀ (a_2 : Ordinal.{u_4}), (∀ b < o, a + b ≤ a_2) → a + o ≤ a_2

Tactic:
exact ⟨add_right_strictMono, fun _ l _ ↦ (add_le_iff_of_isSuccLimit l).2⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ IsSuccLimit b → IsSuccLimit (a + b)

Tactic:
(isNormal_add_right a).map_isSuccLimit

Premises used: Order.IsNormal.map_isSuccLimit, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
rw : b < a ∧ ∀ a_1 < a - b, succ a_1 < a - b
⊢ IsSuccLimit (a - b)

Tactic:
rw [isSuccLimit_iff, Ordinal.sub_ne_zero_iff_lt, isSuccPrelimit_iff_succ_lt]

Premises used: Order.isSuccPrelimit_iff_succ_lt, Ordinal.isSuccLimit_iff, Ordinal.sub_ne_zero_iff_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
⊢ b < a ∧ ∀ a_1 < a - b, succ a_1 < a - b

Tactic:
⟨h, fun c hc ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
refine : ∀ (c : Ordinal.{u_4}) (hc : c < a - b), succ c < a - b
⊢ b < a ∧ ∀ a_1 < a - b, succ a_1 < a - b

Tactic:
refine ⟨h, fun c hc ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : c < a - b
rw : ∀ (hc : b + c < a), b + succ c < a
⊢ succ c < a - b

Tactic:
rw [lt_sub] at hc ⊢

Premises used: Ordinal.lt_sub
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
rw : b + c + 1 < a
⊢ b + succ c < a

Tactic:
rw [succ_eq_add_one, ← add_assoc]

Premises used: Order.succ_eq_add_one, add_assoc
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + c + 1 < a

Tactic:
ha.succ_lt hc

Premises used: Order.succ, Order.IsSuccPrelimit.succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + c + 1 < a

Tactic:
exact ha.succ_lt hc

Premises used: Order.IsSuccPrelimit.succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal.{u}
x x_1 x_2 : WellOrder
⊢ ∀ {a b : (x_2.α × x_1.α) × x.α},
    Prod.Lex x_2.r (Prod.Lex x_1.r x.r)
        ((prodAssoc x_2.α x_1.α x.α : (a : (x_2.α × x_1.α) × x.α) → x_2.α × x_1.α × x.α) a)
        ((prodAssoc x_2.α x_1.α x.α : (a : (x_2.α × x_1.α) × x.α) → x_2.α × x_1.α × x.α) b) ↔
      Prod.Lex (Prod.Lex x_2.r x_1.r) x.r a b

Tactic:
grind [Prod.mk.injEq]

Premises used: Prod.mk.injEq
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
r : α_1 → α_1 → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal.{u}
α : Type u
x : α → α → Prop
h : IsWellOrder α x
⊢ ∀ {a b : α × PUnit.{u + 1}},
    x ((prodPUnit α : (a : α × PUnit.{u + 1}) → α) a) ((prodPUnit α : (a : α × PUnit.{u + 1}) → α) b) ↔
      Prod.Lex x emptyRelation a b

Tactic:
simp [Prod.lex_def]

Premises used: Prod.lex_def
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
r : α_1 → α_1 → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal.{u}
α : Type u
x : α → α → Prop
h : IsWellOrder α x
⊢ ∀ {a b : PUnit.{u + 1} × α},
    x ((punitProd α : (a : PUnit.{u + 1} × α) → α) a) ((punitProd α : (a : PUnit.{u + 1} × α) → α) b) ↔
      Prod.Lex emptyRelation x a b

Tactic:
simp [Prod.lex_def]

Premises used: Prod.lex_def
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ type (Prod.Lex s r) = type r * type s

Tactic:
rfl

Premises used: Ordinal.type, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
type :
  ∀ (α : Type u_4) (r : α → α → Prop) [inst : IsWellOrder α r] (β : Type u_4) (s : β → β → Prop)
    [inst_1 : IsWellOrder β s], Ordinal.type r * Ordinal.type s = 0 ↔ Ordinal.type r = 0 ∨ Ordinal.type s = 0
⊢ a * b = 0 ↔ a = 0 ∨ b = 0

Tactic:
induction a, b using inductionOn₂ with | _ α _ β _
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_4
r : α → α → Prop
inst : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst_1 : IsWellOrder β s
type : Ordinal.type (Prod.Lex s r) = 0 ↔ Ordinal.type r = 0 ∨ Ordinal.type s = 0
type₁ : IsEmpty.{u_4 + 1} (β × α) ↔ IsEmpty α ∨ IsEmpty β
type₂ : IsEmpty β ∨ IsEmpty α ↔ IsEmpty α ∨ IsEmpty β
⊢ Ordinal.type r * Ordinal.type s = 0 ↔ Ordinal.type r = 0 ∨ Ordinal.type s = 0

Tactic:
simp_rw [← type_prod_lex, type_eq_zero_iff_isEmpty, isEmpty_prod, iff_true_intro or_comm]

Premises used: isEmpty_prod, Ordinal.type_prod_lex, iff_true_intro, or_comm, Ordinal.type_eq_zero_iff_isEmpty
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : Ordinal.{u_4}
⊢ 0 * x = 0

Tactic:
mul_eq_zero'.2 (.inl rfl)

Premises used: Iff.mpr, _private.0.Ordinal.mul_eq_zero', Or.inl, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : Ordinal.{u_4}
⊢ 0 * x = 0

Tactic:
exact mul_eq_zero'.2 (.inl rfl)

Premises used: Iff.mpr, _private.0.Ordinal.mul_eq_zero', Or.inl, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : Ordinal.{u_4}
⊢ x * 0 = 0

Tactic:
mul_eq_zero'.2 (.inr rfl)

Premises used: Iff.mpr, _private.0.Ordinal.mul_eq_zero', Or.inr, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : Ordinal.{u_4}
⊢ x * 0 = 0

Tactic:
exact mul_eq_zero'.2 (.inr rfl)

Premises used: Iff.mpr, _private.0.Ordinal.mul_eq_zero', Or.inr, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{v}
⊢ lift.{u, v} (a * b) = lift.{u, v} a * lift.{u, v} b

Tactic:
Quotient.inductionOn₂ a b fun ⟨_α, _r, _⟩ ⟨_β, _s, _⟩ =>
    Quotient.sound
      ⟨(RelIso.preimage Equiv.ulift _).trans
          (RelIso.prodLexCongr (RelIso.preimage Equiv.ulift _)
              (RelIso.preimage Equiv.ulift _)).symm⟩

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ (a * b).card = a.card * b.card

Tactic:
Quotient.inductionOn₂ a b fun ⟨α, _r, _⟩ ⟨β, _s, _⟩ => mul_comm #β #α

Premises used: Quotient.inductionOn₂
-- 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
a b c : Ordinal.{u_4}
x x_1 x_2 : WellOrder
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
β : Type u_4
s : β → β → Prop
wo_1 : IsWellOrder β s
γ : Type u_4
t : γ → γ → Prop
wo_2 : IsWellOrder γ t
⊢ ∀ {a b : (β ⊕ γ) × α},
    Sum.Lex (Prod.Lex s r) (Prod.Lex t r) ((sumProdDistrib β γ α : (a : (β ⊕ γ) × α) → β × α ⊕ γ × α) a)
        ((sumProdDistrib β γ α : (a : (β ⊕ γ) × α) → β × α ⊕ γ × α) b) ↔
      Prod.Lex (Sum.Lex s t) r a b

Tactic:
simp [Prod.lex_def]

Premises used: Prod.lex_def
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ a * succ b = a * b + a

Tactic:
mul_add_one a b

Premises used: Order.succ, mul_add_one
-- 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
⊢ ⟦{ α := γ, r := t, wo := wo_2 : WellOrder.{u} }⟧ * ⟦{ α := α, r := r, wo := wo : WellOrder.{u} }⟧ ≤
    ⟦{ α := γ, r := t, wo := wo_2 : WellOrder.{u} }⟧ * ⟦{ α := β, r := s, wo := wo_1 : WellOrder.{u} }⟧

Tactic:
(RelEmbedding.ofMonotone (fun a : α × γ => (f a.1, a.2)) fun a b h => ?_).ordinal_type_le

Premises used: Prod.mk, Prod.fst, RelEmbedding.ordinal_type_le, RelEmbedding.ofMonotone, Prod.snd, DFunLike.coe
-- 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₁ :
  ∀ (a b : α × γ) (h : Prod.Lex r t a b),
    Prod.Lex s t ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) a)
      ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) b)
⊢ ⟦{ α := γ, r := t, wo := wo_2 : WellOrder.{u} }⟧ * ⟦{ α := α, r := r, wo := wo : WellOrder.{u} }⟧ ≤
    ⟦{ α := γ, r := t, wo := wo_2 : WellOrder.{u} }⟧ * ⟦{ α := β, r := s, wo := wo_1 : WellOrder.{u} }⟧

Tactic:
refine
        (RelEmbedding.ofMonotone (fun a : α × γ => (f a.1, a.2)) fun a b h => ?_).ordinal_type_le

Premises used: Prod.mk, Prod.fst, RelEmbedding.ordinal_type_le, RelEmbedding.ofMonotone, Prod.snd, DFunLike.coe
-- 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_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₂))
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₂))
⊢ Prod.Lex s t ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) a)
    ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) b)

Tactic:
obtain ⟨-, -, h'⟩ | ⟨-, h'⟩ := h
-- 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' : 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₂))

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

Premises used: Iff.mpr, RelEmbedding.map_rel_iff, InitialSeg.toRelEmbedding, 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' : 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₂))

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

Premises used: Iff.mpr, RelEmbedding.map_rel_iff, InitialSeg.toRelEmbedding, 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' : t b₁ b₂
⊢ Prod.Lex s t ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) (a_1, b₁))
    ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) (a_1, b₂))

Tactic:
Prod.Lex.right _ h'

Premises used: Prod.Lex.right
-- 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' : t b₁ b₂
⊢ Prod.Lex s t ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) (a_1, b₁))
    ((fun (a : α × γ) ↦ (((f : (a : α) → β) a.1, a.2) : β × γ)) (a_1, b₂))

Tactic:
exact Prod.Lex.right _ h'

Premises used: Prod.Lex.right
-- 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
⊢ 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})

Tactic:
(RelEmbedding.ofMonotone (fun a : γ × α => (a.1, f a.2)) fun a b h => ?_).ordinal_type_le

Premises used: Prod.mk, Prod.fst, RelEmbedding.ordinal_type_le, RelEmbedding.ofMonotone, Prod.snd, DFunLike.coe
-- 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₁ :
  ∀ (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)
⊢ 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})

Tactic:
refine
        (RelEmbedding.ofMonotone (fun a : γ × α => (a.1, f a.2)) fun a b h => ?_).ordinal_type_le

Premises used: Prod.mk, Prod.fst, RelEmbedding.ordinal_type_le, RelEmbedding.ofMonotone, Prod.snd, DFunLike.coe
-- 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_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₂))
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₂))
⊢ Prod.Lex t s ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) a)
    ((fun (a : γ × α) ↦ ((a.1, (f : (a : α) → β) a.2) : γ × β)) b)

Tactic:
obtain ⟨-, -, h'⟩ | ⟨-, h'⟩ := h