awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
h_2 : IsWellOrder β s
f : s ≺i r
h :
  (RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦ x1 < x2)
          lift.{u, v} liftInitialSeg._proof_1 :
        (a : Ordinal.{v}) → Ordinal.{max u v})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) : (a : α) → Ordinal.{v})
        (f.top (r := s) (s := r))) =
    type s
⊢ Membership.mem (γ := Set Ordinal.{max u v})
    (range (ι := Ordinal.{v})
      (⇑(RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦
            x1 < x2) lift.{u, v} liftInitialSeg._proof_1) :
        (a : Ordinal.{v}) → Ordinal.{max u v}))
    (type s)

Tactic:
use typein r f.top

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.top, DFunLike.coe, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
h_2 : IsWellOrder β s
f : s ≺i r
h :
  lift.{u, v}
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) : (a : α) → Ordinal.{v})
        (f.top (r := s) (s := r))) =
    type s
h₁ :
  lift.{max v u, v}
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) : (a : α) → Ordinal.{v})
        (f.top (r := s) (s := r))) =
    type s
h₂ : lift.{v, max u v} (type s) = type s
h₃ h₄ : type s = type s
⊢ (RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦ x1 < x2)
          lift.{u, v} liftInitialSeg._proof_1 :
        (a : Ordinal.{v}) → Ordinal.{max u v})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) : (a : α) → Ordinal.{v})
        (f.top (r := s) (s := r))) =
    type s

Tactic:
rw [RelEmbedding.ofMonotone_coe, ← lift_umax, lift_typein_top, lift_id']

Premises used: RelEmbedding.ofMonotone_coe, Ordinal.lift_id', Ordinal.lift_typein_top, Ordinal.lift_umax
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ (⇑liftInitialSeg : (a : Ordinal.{u}) → Ordinal.{max v u}) = lift.{v, u}

Tactic:
rfl

Premises used: Ordinal.lift, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Ordinal.{u}
⊢ lift.{w, max v u} (lift.{v, u} a) = lift.{max v w, u} a

Tactic:
(liftInitialSeg.trans liftInitialSeg).eq liftInitialSeg a

Premises used: Ordinal.lift, Ordinal.liftInitialSeg, InitialSeg.trans, Order.Preimage, InitialSeg.eq
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ lift.{u_2, u_1} 0 = 0

Tactic:
type_eq_zero_of_empty _

Premises used: Ordinal.type_eq_zero_of_empty, Ordinal.lift
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ lift.{u_2, u_1} 1 = 1

Tactic:
type_eq_one_of_unique _

Premises used: Ordinal.lift, Ordinal.type_eq_one_of_unique
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Ordinal.{v}
⊢ Cardinal.lift.{u, v} a.card = (lift.{u, v} a).card

Tactic:
inductionOn a fun _ _ _ => rfl

Premises used: Ordinal.inductionOn
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Ordinal.{u}
b : Ordinal.{max u v}
h : b ≤ lift.{v, u} a
⊢ b ∈ range lift.{v, u}

Tactic:
liftInitialSeg.mem_range_of_le h

Premises used: InitialSeg.mem_range_of_le, Set.Mem, Ordinal.lift, Ordinal.liftInitialSeg
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Ordinal.{u}
b : Ordinal.{max u v}
⊢ b ≤ lift.{v, u} a ↔ ∃ a' ≤ a, lift.{v, u} a' = b

Tactic:
liftInitialSeg.le_apply_iff

Premises used: Ordinal.lift, Ordinal.liftInitialSeg, InitialSeg.le_apply_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Ordinal.{u}
b : Ordinal.{max u v}
⊢ b < lift.{v, u} a ↔ ∃ a' < a, lift.{v, u} a' = b

Tactic:
liftInitialSeg.lt_apply_iff

Premises used: Ordinal.lift, InitialSeg.lt_apply_iff, Ordinal.liftInitialSeg
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u}
rw :
  #(↑(Iio o) : Type (u + 1)) =
    card
      ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
          (a : Ordinal.{u}) → Ordinal.{u + 1})
        o)
⊢ #(↑(Iio o) : Type (u + 1)) = Cardinal.lift.{u + 1, u} o.card

Tactic:
rw [lift_card, ← typein_ordinal]

Premises used: Ordinal.typein_ordinal, Ordinal.lift_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u}
⊢ #(↑(Iio o) : Type (u + 1)) =
    card
      ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
          (a : Ordinal.{u}) → Ordinal.{u + 1})
        o)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ (type fun (x1 x2 : ℕ) ↦ x1 < x2) = ω

Tactic:
(lift_id _).symm

Premises used: Ordinal.omega0, Ordinal.lift_id, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ ω.card = ℵ₀

Tactic:
rfl

Premises used: Quotient.map, Cardinal.lift, Cardinal.aleph0, Cardinal.map, Quot.map, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ lift.{u_1, u_2} ω = ω

Tactic:
lift_lift _

Premises used: Ordinal.omega0, Ordinal.lift_lift
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x x_1 x_2 : WellOrder
⊢ ∀ {a b : (x.α ⊕ x_1.α) ⊕ x_2.α},
    Sum.Lex x.r (Sum.Lex x_1.r x_2.r) ((sumAssoc x.α x_1.α x_2.α : (a : (x.α ⊕ x_1.α) ⊕ x_2.α) → x.α ⊕ x_1.α ⊕ x_2.α) a)
        ((sumAssoc x.α x_1.α x_2.α : (a : (x.α ⊕ x_1.α) ⊕ x_2.α) → x.α ⊕ x_1.α ⊕ x_2.α) b) ↔
      Sum.Lex (Sum.Lex x.r x_1.r) x_2.r a b

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ (o₁ + o₂).card = o₁.card + o₂.card

Tactic:
inductionOn₂ o₁ o₂ fun _ _ _ _ _ _ ↦ rfl

Premises used: Ordinal.inductionOn₂
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ (o + 1).card = o.card + 1

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ type (Sum.Lex r s) = type r + type s

Tactic:
rfl

Premises used: Ordinal.type, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
n : ℕ
zero : card (↑0 : Ordinal.{u}) = (↑0 : Cardinal.{u})
succ :
  ∀ (n : ℕ), card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u}) → card (↑(n + 1) : Ordinal.{u}) = (↑(n + 1) : Cardinal.{u})
⊢ card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u})

Tactic:
induction n
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ card (↑0 : Ordinal.{u}) = (↑0 : Cardinal.{u})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
n : ℕ
h : card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u})
⊢ card (↑(n + 1) : Ordinal.{u}) = (↑(n + 1) : Cardinal.{u})

Tactic:
simp only [card_add, card_one, Nat.cast_succ, *]

Premises used: Nat.cast_succ, Ordinal.card_one, Ordinal.card_add
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
n : ℕ
zero : card (↑0 : Ordinal.{u}) = (↑0 : Cardinal.{u})
succ :
  ∀ (n : ℕ), card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u}) → card (↑(n + 1) : Ordinal.{u}) = (↑(n + 1) : Cardinal.{u})
zero₁ : card (↑0 : Ordinal.{u}) = (↑0 : Cardinal.{u})
succ₁ :
  ∀ (n : ℕ), card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u}) → card (↑(n + 1) : Ordinal.{u}) = (↑(n + 1) : Cardinal.{u})
⊢ card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u})

Tactic:
induction n <;> [simp; simp only [card_add, card_one, Nat.cast_succ, *]]

Premises used: Nat.cast_succ, Ordinal.card_one, Ordinal.card_add
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ card (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
card_nat n

Premises used: Ordinal.card_nat
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) a b →
    (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) ((fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c a)
      ((fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c b)

Tactic:
inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦
      (RelEmbedding.ofMonotone (Sum.recOn · Sum.inl (Sum.inr ∘ f)) ?_).ordinal_type_le

Premises used: Ordinal.inductionOn₃
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
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),
    IsWellOrder γ t →
      (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) (type r) (type s) →
        ∀ (f : r ≼i s) (a b : γ ⊕ α),
          Sum.Lex t r a b →
            Sum.Lex t s
              ((fun (x : γ ⊕ α) ↦
                  (Sum.recOn (motive := fun (x : γ ⊕ α) ↦ γ ⊕ β) x Sum.inl (Sum.inr ∘ (⇑f : (a : α) → β)) : γ ⊕ β))
                a)
              ((fun (x : γ ⊕ α) ↦
                  (Sum.recOn (motive := fun (x : γ ⊕ α) ↦ γ ⊕ β) x Sum.inl (Sum.inr ∘ (⇑f : (a : α) → β)) : γ ⊕ β))
                b)
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) a b →
    (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) ((fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c a)
      ((fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c b)

Tactic:
refine inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦
      (RelEmbedding.ofMonotone (Sum.recOn · Sum.inl (Sum.inr ∘ f)) ?_).ordinal_type_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ_1 : Type w
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 : (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) (type r) (type s)
f : r ≼i s
⊢ ∀ (a b : γ ⊕ α),
    Sum.Lex t r a b →
      Sum.Lex t s
        ((fun (x : γ ⊕ α) ↦
            (Sum.recOn (motive := fun (x : γ ⊕ α) ↦ γ ⊕ β) x Sum.inl (Sum.inr ∘ (⇑f : (a : α) → β)) : γ ⊕ β))
          a)
        ((fun (x : γ ⊕ α) ↦
            (Sum.recOn (motive := fun (x : γ ⊕ α) ↦ γ ⊕ β) x Sum.inl (Sum.inr ∘ (⇑f : (a : α) → β)) : γ ⊕ β))
          b)

Tactic:
simp [f.map_rel_iff]

Premises used: InitialSeg.map_rel_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) a b →
    (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2)
      (Function.swap (φ := fun (a a_2 : Ordinal.{u}) ↦ Ordinal.{u}) (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c a)
      (Function.swap (φ := fun (a a_2 : Ordinal.{u}) ↦ Ordinal.{u}) (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c b)

Tactic:
inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦
      (RelEmbedding.ofMonotone (Sum.recOn · (Sum.inl ∘ f) Sum.inr) ?_).ordinal_type_le

Premises used: Ordinal.inductionOn₃
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
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),
    IsWellOrder γ t →
      (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) (type r) (type s) →
        ∀ (f : r ≼i s) (a b : α ⊕ γ),
          Sum.Lex r t a b →
            Sum.Lex s t
              ((fun (x : α ⊕ γ) ↦
                  (Sum.recOn (motive := fun (x : α ⊕ γ) ↦ β ⊕ γ) x (Sum.inl ∘ (⇑f : (a : α) → β)) Sum.inr : β ⊕ γ))
                a)
              ((fun (x : α ⊕ γ) ↦
                  (Sum.recOn (motive := fun (x : α ⊕ γ) ↦ β ⊕ γ) x (Sum.inl ∘ (⇑f : (a : α) → β)) Sum.inr : β ⊕ γ))
                b)
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) a b →
    (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2)
      (Function.swap (φ := fun (a a_2 : Ordinal.{u}) ↦ Ordinal.{u}) (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c a)
      (Function.swap (φ := fun (a a_2 : Ordinal.{u}) ↦ Ordinal.{u}) (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c b)

Tactic:
refine inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦
      (RelEmbedding.ofMonotone (Sum.recOn · (Sum.inl ∘ f) Sum.inr) ?_).ordinal_type_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ_1 : Type w
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 : (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) (type r) (type s)
f : r ≼i s
⊢ ∀ (a b : α ⊕ γ),
    Sum.Lex r t a b →
      Sum.Lex s t
        ((fun (x : α ⊕ γ) ↦
            (Sum.recOn (motive := fun (x : α ⊕ γ) ↦ β ⊕ γ) x (Sum.inl ∘ (⇑f : (a : α) → β)) Sum.inr : β ⊕ γ))
          a)
        ((fun (x : α ⊕ γ) ↦
            (Sum.recOn (motive := fun (x : α ⊕ γ) ↦ β ⊕ γ) x (Sum.inl ∘ (⇑f : (a : α) → β)) Sum.inr : β ⊕ γ))
          b)

Tactic:
simp [f.map_rel_iff]

Premises used: InitialSeg.map_rel_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ b → ∃ (c : Ordinal.{u_1}), b = a + c

Tactic:
inductionOn₂ a b fun α r _ β s _ ⟨f⟩ ↦ ?_

Premises used: Ordinal.inductionOn₂
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
refine :
  ∀ (α : Type u_1) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type u_1) (s : β → β → Prop) (x_1 : IsWellOrder β s),
    type r ≤ type s → ∀ (f : r ≼i s), ∃ (c : Ordinal.{u_1}), type s = type r + c
⊢ a ≤ b → ∃ (c : Ordinal.{u_1}), b = a + c

Tactic:
refine inductionOn₂ a b fun α r _ β s _ ⟨f⟩ ↦ ?_
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
h_2 : type r ≤ type s
f : r ≼i s
obtain :
  ∀ (γ : Type u_1) (t : γ → γ → Prop),
    IsWellOrder γ t → ∀ (g : Sum.Lex r t ≃r s), ∃ (c : Ordinal.{u_1}), type s = type r + c
⊢ ∃ (c : Ordinal.{u_1}), type s = type r + c

Tactic:
obtain ⟨γ, t, _, ⟨g⟩⟩ := f.exists_sum_relIso

Premises used: InitialSeg.exists_sum_relIso
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ_1 : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
h_2 : type r ≤ type s
f : r ≼i s
γ : Type u_1
t : γ → γ → Prop
left : IsWellOrder γ t
g : Sum.Lex r t ≃r s
⊢ ∃ (c : Ordinal.{u_1}), type s = type r + c

Tactic:
⟨type t, g.ordinal_type_eq.symm⟩

Premises used: Ordinal.type, Exists.intro, RelIso.ordinal_type_eq, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α_1 : Type u
β_1 : Type v
γ_1 : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t_1 : γ_1 → γ_1 → Prop
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
h_2 : type r ≤ type s
f : r ≼i s
γ : Type u_1
t : γ → γ → Prop
left : IsWellOrder γ t
g : Sum.Lex r t ≃r s
⊢ ∃ (c : Ordinal.{u_1}), type s = type r + c

Tactic:
exact ⟨type t, g.ordinal_type_eq.symm⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ b + a

Tactic:
simpa using add_le_add_left bot_le a

Premises used: add_le_add_left, bot_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ a + b

Tactic:
simpa using add_le_add_right bot_le a

Premises used: add_le_add_right, bot_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{u_1}
⊢ a ≤ a + b

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{u_1}
⊢ a ≤ b + a

Tactic:
le_add_self

Premises used: le_add_self
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ ∀ (a : Ordinal.{u_1}), max 0 a = a

Tactic:
zero_max

Premises used: zero_max
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ ∀ (a : Ordinal.{u_1}), max a 0 = a

Tactic:
max_zero

Premises used: max_zero
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{u_1}
⊢ max a b = 0 ↔ a = 0 ∧ b = 0

Tactic:
max_eq_zero

Premises used: max_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sInf ∅) 0

Tactic:
dif_neg Set.not_nonempty_empty

Premises used: Set.not_nonempty_empty, dif_neg
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{u_1}
⊢ a + 1 ≤ b ↔ a < b

Tactic:
inductionOn₂ a b fun α r _ β s _ ↦ ⟨?_, ?_⟩

Premises used: Ordinal.inductionOn₂
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{u_1}
refine_1 :
  ∀ (α : Type u_1) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type u_1) (s : β → β → Prop) (x_1 : IsWellOrder β s),
    type r + 1 ≤ type s → type r < type s
refine_2 :
  ∀ (α : Type u_1) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type u_1) (s : β → β → Prop) (x_1 : IsWellOrder β s),
    type r < type s → type r + 1 ≤ type s
⊢ a + 1 ≤ b ↔ a < b

Tactic:
refine inductionOn₂ a b fun α r _ β s _ ↦ ⟨?_, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
f : InitialSeg (α := α ⊕ PUnit.{u_1 + 1}) (Sum.Lex r emptyRelation) s
⊢ type r < type s

Tactic:
⟨((InitialSeg.leAdd _ _).trans f).toPrincipalSeg fun h ↦ ?_⟩

Premises used: Nonempty.intro, InitialSeg.leAdd, InitialSeg.trans, InitialSeg.toPrincipalSeg
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
f : InitialSeg (α := α ⊕ PUnit.{u_1 + 1}) (Sum.Lex r emptyRelation) s
refine_1 :
  ∀
    (h :
      Surjective (α := α) (β := β)
        (⇑(InitialSeg.trans (r := r) (s := Sum.Lex r emptyRelation) (t := s) (InitialSeg.leAdd r emptyRelation) f) :
          (a : α) → β)),
    False
⊢ type r < type s

Tactic:
refine ⟨((InitialSeg.leAdd _ _).trans f).toPrincipalSeg fun h ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type u_1
s : β → β → Prop
h_2 : IsWellOrder β s
f : InitialSeg (α := α ⊕ PUnit.{u_1 + 1}) (Sum.Lex r emptyRelation) s
h :
  Surjective (α := α) (β := β)
    (⇑(InitialSeg.trans (r := r) (s := Sum.Lex r emptyRelation) (t := s) (InitialSeg.leAdd r emptyRelation) f) :
      (a : α) → β)
⊢ False

Tactic:
simpa using h (f (Sum.inr PUnit.unit))

Premises used: Sum.inr, PUnit.unit, DFunLike.coe
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
f : r ≺i s
apply :
  ∀ (a b : α ⊕ PUnit.{u_1 + 1}),
    Sum.Lex r emptyRelation a b →
      s
        ((fun (x : α ⊕ PUnit.{u_1 + 1}) ↦
            (Sum.recOn (motive := fun (x : α ⊕ PUnit.{u_1 + 1}) ↦ β) x
                (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β) fun (x : PUnit.{u_1 + 1}) ↦
                f.top (r := r) (s := s) :
              β))
          a)
        ((fun (x : α ⊕ PUnit.{u_1 + 1}) ↦
            (Sum.recOn (motive := fun (x : α ⊕ PUnit.{u_1 + 1}) ↦ β) x
                (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β) fun (x : PUnit.{u_1 + 1}) ↦
                f.top (r := r) (s := s) :
              β))
          b)
⊢ type r + 1 ≤ type s

Tactic:
apply (RelEmbedding.ofMonotone (Sum.recOn · f fun _ ↦ f.top) ?_).ordinal_type_le

Premises used: RelEmbedding.ordinal_type_le, RelEmbedding.ofMonotone
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
f : r ≺i s
⊢ ∀ (a b : α ⊕ PUnit.{u_1 + 1}),
    Sum.Lex r emptyRelation a b →
      s
        ((fun (x : α ⊕ PUnit.{u_1 + 1}) ↦
            (Sum.recOn (motive := fun (x : α ⊕ PUnit.{u_1 + 1}) ↦ β) x
                (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β) fun (x : PUnit.{u_1 + 1}) ↦
                f.top (r := r) (s := s) :
              β))
          a)
        ((fun (x : α ⊕ PUnit.{u_1 + 1}) ↦
            (Sum.recOn (motive := fun (x : α ⊕ PUnit.{u_1 + 1}) ↦ β) x
                (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β) fun (x : PUnit.{u_1 + 1}) ↦
                f.top (r := r) (s := s) :
              β))
          b)

Tactic:
simpa [f.map_rel_iff] using f.lt_top

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.lt_top, RelEmbedding.map_rel_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ NoMaxOrder Ordinal.{u_1}

Tactic:
⟨fun _ => ⟨_, succ_le_iff'.1 le_rfl⟩⟩

Premises used: le_rfl, NoMaxOrder.mk, HAdd.hAdd, Exists.intro, Iff.mp, OfNat.ofNat, _private.0.Ordinal.succ_le_iff'
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u}
⊢ (fun (o : Ordinal.{u}) ↦ o + 1) a ≤ b ↔ a < b

Tactic:
succ_le_iff'

Premises used: _private.0.Ordinal.succ_le_iff'
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ∀ {a b : Ordinal.{u}}, (fun (o : Ordinal.{u}) ↦ o + 1) a ≤ b ↔ a < b

Tactic:
exact succ_le_iff'

Premises used: _private.0.Ordinal.succ_le_iff'
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ o + 1 = succ o

Tactic:
rfl

Premises used: Order.succ, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (succ 0) 1

Tactic:
zero_add 1

Premises used: Order.succ, zero_add, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (succ 1) 2

Tactic:
one_add_one_eq_two

Premises used: Order.succ, one_add_one_eq_two
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ o₁ + succ o₂ = succ (o₁ + o₂)

Tactic:
(add_assoc _ _ _).symm

Premises used: Order.succ, add_assoc, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ 1 ≤ o ↔ o ≠ 0

Tactic:
Order.one_le_iff_ne_zero

Premises used: Order.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ 0 < succ o

Tactic:
add_pos_of_right zero_lt_one o

Premises used: Order.succ, add_pos_of_right, zero_lt_one
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ o + 1 ≠ 0

Tactic:
(add_pos_of_right zero_lt_one o).ne'

Premises used: add_pos_of_right, LT.lt.ne', zero_lt_one
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ succ o ≠ 0

Tactic:
(add_pos_of_right zero_lt_one o).ne'

Premises used: Order.succ, add_pos_of_right, LT.lt.ne', zero_lt_one
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Ordinal.{u_1}
⊢ a < 1 ↔ a = 0

Tactic:
Order.lt_one_iff

Premises used: Order.lt_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Ordinal.{u_1}
⊢ a ≤ 1 ↔ a = 0 ∨ a = 1

Tactic:
Order.le_one_iff

Premises used: Order.le_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ (succ o).card = o.card + 1

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
n : ℕ
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (↑n.succ : Ordinal.{u_1}) (succ (↑n : Ordinal.{u_1}))

Tactic:
n.cast_add_one

Premises used: Order.succ, Nat.cast_add_one
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ Eq (α := (↑(Iio 1) : Type (u_1 + 1))) (default : (↑(Iio 1) : Type (u_1 + 1)))
    (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ Membership.mem (γ := Set Ordinal.{u_1}) (Iio 1) x) 0 ⋯ :
      { x : Ordinal.{u_1} // Membership.mem (γ := Set Ordinal.{u_1}) (Iio 1) x })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ 0 ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)

Tactic:
simp