awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.sumLexCongr (RelIso.preimage Equiv.ulift _) (RelIso.preimage Equiv.ulift _)).symm⟩

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{v}
⊢ lift.{u, v} (a + 1) = lift.{u, v} a + 1

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{v}
⊢ lift.{u, v} (succ a) = succ (lift.{u, v} a)

Tactic:
lift_add_one a

Premises used: Order.succ, Ordinal.lift_add_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
⊢ c + a ≤ c + b → a ≤ b

Tactic:
inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦ ?_

Premises used: Ordinal.inductionOn₃
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
refine :
  ∀ (α : Type u) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type u) (s : β → β → Prop) (x_1 : IsWellOrder β s)
    (γ : Type u) (t : γ → γ → Prop) (x_2 : IsWellOrder γ t),
    type t + type r ≤ type t + type s → ∀ (f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)), type r ≤ type s
⊢ c + a ≤ c + b → a ≤ b

Tactic:
refine inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦ ?_
-- 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 : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
a : γ
⊢ Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)

Tactic:
simpa using ((InitialSeg.leAdd t r).trans f).eq (InitialSeg.leAdd t s) a

Premises used: InitialSeg.leAdd, InitialSeg.trans, InitialSeg.eq
-- 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}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
⊢ ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)

Tactic:
have H₁ a : f (Sum.inl a) = Sum.inl a := by
      simpa using ((InitialSeg.leAdd t r).trans f).eq (InitialSeg.leAdd t s) a
-- 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 : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
a : α
generalize : ∀ (x : γ ⊕ β) (hx : (f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) = x), ∃ (b : β), x = Sum.inr b
⊢ ∃ (b : β), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr b : γ ⊕ β)

Tactic:
generalize hx : f (Sum.inr a) = x

Premises used: Sum.inr, 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 : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
a : α
x : γ ⊕ β
hx : (f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) = x
inl :
  ∀ (x : γ) (hx : Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inl x : γ ⊕ β)),
    ∃ (b : β), Sum.inl x = Sum.inr b
inr :
  ∀ (x : β) (hx : Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr x : γ ⊕ β)),
    ∃ (b : β), Eq (α := γ ⊕ β) (Sum.inr x) (Sum.inr b)
⊢ ∃ (b : β), x = Sum.inr b

Tactic:
obtain x | x := x
-- 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 : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
a : α
x : γ
hx : Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inl x : γ ⊕ β)
⊢ Sum.inr a = Sum.inl x

Tactic:
rw [← H₁, f.inj] at hx

Premises used: InitialSeg.inj
-- 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 : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
a : α
x : γ
hx : Sum.inr a = Sum.inl x
⊢ ∃ (b : β), Sum.inl x = Sum.inr b

Tactic:
contradiction
-- 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 : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
a : α
x : β
hx : Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr x : γ ⊕ β)
⊢ ∃ (b : β), Eq (α := γ ⊕ β) (Sum.inr x) (Sum.inr b)

Tactic:
⟨x, rfl⟩

Premises used: Exists.intro, rfl
-- 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 : Ordinal.{u}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
a : α
x : β
hx : Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr x : γ ⊕ β)
⊢ ∃ (b : β), Eq (α := γ ⊕ β) (Sum.inr x) (Sum.inr b)

Tactic:
exact ⟨x, rfl⟩
-- 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}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
⊢ ∀ (a : α), ∃ (b : β), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr b : γ ⊕ β)

Tactic:
have H₂ a : ∃ b, f (Sum.inr a) = Sum.inr b := by
      generalize hx : f (Sum.inr a) = x
      obtain x | x := x
      · rw [← H₁, f.inj] at hx
        contradiction
      · exact ⟨x, rfl⟩
-- 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}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
H₂ : ∀ (a : α), ∃ (b : β), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr b : γ ⊕ β)
choose :
  ∀ (g : (a : α) → β)
    (hg : ∀ (a : α), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr (g a) : γ ⊕ β)),
    type r ≤ type s
⊢ type r ≤ type s

Tactic:
choose g hg using 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}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
g : (a : α) → β
hg : ∀ (a : α), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr (g a) : γ ⊕ β)
⊢ type r ≤ type s

Tactic:
(RelEmbedding.ofMonotone g fun _ _ h ↦ ?_).ordinal_type_le

Premises used: RelEmbedding.ordinal_type_le, RelEmbedding.ofMonotone
-- 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}
α : Type u
r : α → α → Prop
h : IsWellOrder α r
β : Type u
s : β → β → Prop
h_1 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_2 : IsWellOrder γ t
h_3 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
g : (a : α) → β
hg : ∀ (a : α), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr (g a) : γ ⊕ β)
refine : ∀ (x x_1 : α) (h : r x x_1), s (g x) (g x_1)
⊢ type r ≤ type s

Tactic:
refine (RelEmbedding.ofMonotone g fun _ _ h ↦ ?_).ordinal_type_le

Premises used: RelEmbedding.ordinal_type_le, RelEmbedding.ofMonotone
-- 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}
α : Type u
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type u
s : β → β → Prop
h_2 : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
h_3 : IsWellOrder γ t
h_4 : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inl a) : γ ⊕ β) (Sum.inl a : γ ⊕ β)
g : (a : α) → β
hg : ∀ (a : α), Eq (α := γ ⊕ β) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr a) : γ ⊕ β) (Sum.inr (g a) : γ ⊕ β)
x x_1 : α
h : r x x_1
rwa : Sum.Lex t s (Sum.inr (g x)) (Sum.inr (g x_1))
rwa₁ : Sum.Lex t s ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr x)) (Sum.inr (g x_1))
rwa₂ : Sum.Lex t s ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr x)) ((f : (a : γ ⊕ α) → γ ⊕ β) (Sum.inr x_1))
rwa₃ : Sum.Lex t r (Sum.inr x) (Sum.inr x_1)
rwa₄ rwa₅ rwa₆ rwa₇ : r x x_1
⊢ s (g x) (g x_1)

Tactic:
rwa [← @Sum.lex_inr_inr _ t _ s, ← hg, ← hg, f.map_rel_iff, Sum.lex_inr_inr]

Premises used: InitialSeg.map_rel_iff, Sum.lex_inr_inr
-- 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_4}
h : Eq.{u_4 + 2} (α := Ordinal.{u_4}) ((fun (x : Ordinal.{u_4}) ↦ a + x) b) ((fun (x : Ordinal.{u_4}) ↦ a + x) c)
⊢ b = c

Tactic:
simpa only [le_antisymm_iff, add_le_add_iff_left] using h

Premises used: add_le_add_iff_left, le_antisymm_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
rw : ¬a + c ≤ a + b ↔ b < c
rw₁ : ¬a + c ≤ a + b ↔ ¬c ≤ b
rw₂ rw₃ : ¬c ≤ b ↔ ¬c ≤ b
⊢ a + b < a + c ↔ b < c

Tactic:
rw [← not_le, ← not_le, add_le_add_iff_left]

Premises used: not_le, add_le_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ AddLeftStrictMono Ordinal.{u}

Tactic:
⟨fun a _b _c ↦ (add_lt_add_iff_left' a).2⟩

Premises used: CovariantClass.mk, Iff.mpr, _private.0.Ordinal.add_lt_add_iff_left'
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ AddLeftReflectLT Ordinal.{u}

Tactic:
⟨fun a _b _c ↦ (add_lt_add_iff_left' a).1⟩

Premises used: ContravariantClass.mk, Iff.mp, _private.0.Ordinal.add_lt_add_iff_left'
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ AddRightReflectLT Ordinal.{u}

Tactic:
⟨fun _a _b _c ↦ lt_imp_lt_of_le_imp_le fun h => add_le_add_left h _⟩

Premises used: add_le_add_left, ContravariantClass.mk, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ a + (↑0 : Ordinal.{u_4}) ≤ b + (↑0 : Ordinal.{u_4}) ↔ a ≤ b

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
n : ℕ
⊢ a + (↑(n + 1) : Ordinal.{u_4}) ≤ b + (↑(n + 1) : Ordinal.{u_4}) ↔ a ≤ b

Tactic:
simpa [← add_assoc] using add_le_add_iff_right n

Premises used: add_assoc
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
n : ℕ
⊢ a + (↑n : Ordinal.{u_4}) = b + (↑n : Ordinal.{u_4}) ↔ a = b

Tactic:
simp only [le_antisymm_iff, add_le_add_iff_right]

Premises used: le_antisymm_iff, Ordinal.add_le_add_iff_right
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
h : IsWellOrder α r
β : Type u_4
s : β → β → Prop
h_1 : IsWellOrder β s
simp_rw : IsEmpty.{u_4 + 1} (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
⊢ type r + type s = 0 ↔ type r = 0 ∧ type s = 0

Tactic:
simp_rw [← type_sum_lex, type_eq_zero_iff_isEmpty]

Premises used: Ordinal.type_sum_lex, Ordinal.type_eq_zero_iff_isEmpty
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
h : IsWellOrder α r
β : Type u_4
s : β → β → Prop
h_1 : IsWellOrder β s
⊢ IsEmpty.{u_4 + 1} (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

Tactic:
isEmpty_sum

Premises used: isEmpty_sum
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
h : IsWellOrder α r
β : Type u_4
s : β → β → Prop
h_1 : IsWellOrder β s
⊢ IsEmpty.{u_4 + 1} (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

Tactic:
exact isEmpty_sum

Premises used: isEmpty_sum
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a + b = 0
⊢ a = 0

Tactic:
(add_eq_zero_iff.1 h).1

Premises used: Ordinal.add_eq_zero_iff, And.left, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a + b = 0
⊢ b = 0

Tactic:
(add_eq_zero_iff.1 h).2

Premises used: Ordinal.add_eq_zero_iff, And.right, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
⊢ IsSuccLimit o ↔ o ≠ 0 ∧ IsSuccPrelimit o

Tactic:
isSuccLimit_iff_of_orderBot

Premises used: Order.isSuccLimit_iff_of_orderBot
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ IsSuccPrelimit.{u_4 + 1} (α := Ordinal.{u_4}) 0

Tactic:
isSuccPrelimit_bot

Premises used: Order.isSuccPrelimit_bot
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ ¬IsSuccLimit.{u_4 + 1} (α := Ordinal.{u_4}) 0

Tactic:
not_isSuccLimit_bot

Premises used: Order.not_isSuccLimit_bot
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{v}
⊢ IsSuccPrelimit (lift.{u, v} o) ↔ IsSuccPrelimit o

Tactic:
liftInitialSeg.isSuccPrelimit_apply_iff

Premises used: Ordinal.lift, Ordinal.liftInitialSeg, InitialSeg.isSuccPrelimit_apply_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{v}
⊢ IsSuccLimit (lift.{u, v} o) ↔ IsSuccLimit o

Tactic:
liftInitialSeg.isSuccLimit_apply_iff

Premises used: Ordinal.lift, Ordinal.liftInitialSeg, InitialSeg.isSuccLimit_apply_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
h : IsSuccLimit o
n : ℕ
⊢ (↑n : Ordinal.{u_4}) < o

Tactic:
simpa using h.add_natCast_lt h.bot_lt n

Premises used: Order.IsSuccLimit.add_natCast_lt, Order.IsSuccLimit.bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
h : IsSuccLimit o
⊢ 1 < o

Tactic:
mod_cast natCast_lt_of_isSuccLimit h 1

Premises used: congrArg, cast, LT.lt, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_one, Ordinal.natCast_lt_of_isSuccLimit, Eq.trans
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
⊢ o = 0 ∨ Membership.mem (γ := Set Ordinal.{u_4}) (range succ) o ∨ IsSuccLimit o

Tactic:
simpa using isMin_or_mem_range_succ_or_isSuccLimit o

Premises used: Order.isMin_or_mem_range_succ_or_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
motive : Ordinal.{u_4} → Sort u_5
H₁ : motive 0
H₂ : (o : Ordinal.{u_4}) → motive o → motive (o + 1)
H₃ : (o : Ordinal.{u_4}) → IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o
⊢ limitRecOn (motive := motive) 0 H₁ H₂ H₃ = H₁

Tactic:
SuccOrder.limitRecOn_isMin _ _ _ isMin_bot

Premises used: Ordinal.limitRecOn, isMin_bot, SuccOrder.limitRecOn_isMin
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
motive : Ordinal.{u_4} → Sort u_5
o : Ordinal.{u_4}
H₁ : motive 0
H₂ : (o : Ordinal.{u_4}) → motive o → motive (o + 1)
H₃ : (o : Ordinal.{u_4}) → IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o
⊢ limitRecOn (motive := motive) (o + 1) H₁ H₂ H₃ = H₂ o (limitRecOn (motive := motive) o H₁ H₂ H₃)

Tactic:
SuccOrder.limitRecOn_succ ..

Premises used: SuccOrder.limitRecOn_succ, Order.succ, Ordinal.limitRecOn
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
motive : Ordinal.{u_4} → Sort u_5
o : Ordinal.{u_4}
H₁ : motive 0
H₂ : (o : Ordinal.{u_4}) → motive o → motive (o + 1)
H₃ : (o : Ordinal.{u_4}) → IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o
⊢ limitRecOn (motive := motive) (succ o) H₁ H₂ H₃ = H₂ o (limitRecOn (motive := motive) o H₁ H₂ H₃)

Tactic:
limitRecOn_add_one ..

Premises used: Order.succ, Ordinal.limitRecOn_add_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
motive : Ordinal.{u_4} → Sort u_5
o : Ordinal.{u_4}
H₁ : motive 0
H₂ : (o : Ordinal.{u_4}) → motive o → motive (o + 1)
H₃ : (o : Ordinal.{u_4}) → IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o
h : IsSuccLimit o
⊢ limitRecOn (motive := motive) o H₁ H₂ H₃ =
    H₃ o h fun (x : Ordinal.{u_4}) (_h : x < o) ↦ limitRecOn (motive := motive) x H₁ H₂ H₃

Tactic:
SuccOrder.limitRecOn_of_isSuccLimit ..

Premises used: Ordinal.limitRecOn, SuccOrder.limitRecOn_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
l : Ordinal.{u_5}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_5 + 1)) → Sort u_4
o : (↑(Iio l) : Type (u_5 + 1))
zero : motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ⋯)
succ :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (Order.succ (↑o : Ordinal.{u_5})) ⋯)
limit :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_5}) → ((o' : (↑(Iio l) : Type (u_5 + 1))) → o' < o → motive o') → motive o
obtain : (o : Ordinal.{u_5}) → (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)
⊢ motive o

Tactic:
obtain ⟨o, ho⟩ := o
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
l : Ordinal.{u_5}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_5 + 1)) → Sort u_4
zero : motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ⋯)
succ :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (Order.succ (↑o : Ordinal.{u_5})) ⋯)
limit :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_5}) → ((o' : (↑(Iio l) : Type (u_5 + 1))) → o' < o → motive o') → motive o
ho : 0 ∈ Iio l
⊢ motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ho)

Tactic:
exact zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
l : Ordinal.{u_5}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_5 + 1)) → Sort u_4
zero : motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ⋯)
succ :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (Order.succ (↑o : Ordinal.{u_5})) ⋯)
limit :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_5}) → ((o' : (↑(Iio l) : Type (u_5 + 1))) → o' < o → motive o') → motive o
o : Ordinal.{u_5}
IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)
ho : o + 1 ∈ Iio l
add_one : (ho' : o < l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (o + 1) ho)
⊢ motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (o + 1) ho)

Tactic:
have ho' : o < l := (lt_succ o).trans ho
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
l : Ordinal.{u_5}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_5 + 1)) → Sort u_4
zero : motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ⋯)
succ :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (Order.succ (↑o : Ordinal.{u_5})) ⋯)
limit :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_5}) → ((o' : (↑(Iio l) : Type (u_5 + 1))) → o' < o → motive o') → motive o
o : Ordinal.{u_5}
IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)
ho : o + 1 ∈ Iio l
ho' : o < l
⊢ motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (o + 1) ho)

Tactic:
exact succ ⟨o, ho'⟩ (IH ho')

Premises used: Subtype.mk
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
l : Ordinal.{u_5}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_5 + 1)) → Sort u_4
zero : motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ⋯)
succ :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (Order.succ (↑o : Ordinal.{u_5})) ⋯)
limit :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_5}) → ((o' : (↑(Iio l) : Type (u_5 + 1))) → o' < o → motive o') → motive o
o : Ordinal.{u_5}
ho' : IsSuccLimit o
IH :
  (o' : Ordinal.{u_5}) →
    o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o' ho)
ho : o ∈ Iio l
⊢ motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)

Tactic:
exact limit _ ho' fun a ha ↦ IH a.1 ha (ha.trans (c := l) ho)

Premises used: LT.lt.trans, Subtype.val