awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ LT.lt (α := (↑(Iio (type r)) : Type (u_4 + 1)))
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x)
        ⋯ :
      { x : Ordinal.{u_4} // x ∈ Iio (type r) })
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
        (succ
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
            x))
        ⋯ :
      { x : Ordinal.{u_4} // x ∈ Iio (type r) })
have h₁ : LT.lt (α := Ordinal.{u_4})
  (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x :
    Ordinal.{u_4})
  (succ
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x) :
    Ordinal.{u_4})
Tactic: rw [Subtype.mk_lt_mk, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
h₁ :
  LT.lt (α := Ordinal.{u_4})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x :
      Ordinal.{u_4})
    (succ
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
          x) :
      Ordinal.{u_4})
⊢ LT.lt (α := (↑(Iio (type r)) : Type (u_4 + 1)))
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x)
        ⋯ :
      { x : Ordinal.{u_4} // x ∈ Iio (type r) })
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
        (succ
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
            x))
        ⋯ :
      { x : Ordinal.{u_4} // x ∈ Iio (type r) })
have h₂ : LE.le (α := Ordinal.{u_4})
  (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x :
    Ordinal.{u_4})
  (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x :
    Ordinal.{u_4})
Tactic: rw [Subtype.mk_lt_mk, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
hr : IsSuccLimit (type r)
x : α
⊢ Bounded r {x}
have refine : ∀ (b : α),
  Membership.mem (γ := Set α) {x} b →
    r b
      ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
        (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
            (succ
              (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) :
                  (a : α) → Ordinal.{u_1})
                x))
            sorry :
          { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
Tactic: refine ⟨enum r ⟨succ (typein r x), hr.succ_lt (typein_lt_type r x)⟩, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : Membership.mem (γ := Set α) {x} b
⊢ r b
    ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
              x))
          ⋯ :
        { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
have rw : r x
  ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
    (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
        (succ
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
            x))
        sorry :
      { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
Tactic: rw [mem_singleton_iff.1 hb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : Membership.mem (γ := Set α) {x} b
⊢ r x
    ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
              x))
          ⋯ :
        { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
have nth_rw : r
  ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
    (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) x)
        sorry :
      { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
  ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
    (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
        (succ
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
            x))
        sorry :
      { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
Tactic: nth_rw 1 [← enum_typein r x]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : Membership.mem (γ := Set α) {x} b
⊢ r
    ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
            x)
          ⋯ :
        { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
    ((enum r : (a : (↑(Iio (type r)) : Type (u_1 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1})
              x))
          ⋯ :
        { x : Ordinal.{u_1} // x ∈ Iio (type r) }))
have rw : LT.lt (α := Ordinal.{u_1})
  (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) x :
    Ordinal.{u_1})
  (succ
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) x) :
    Ordinal.{u_1})
Tactic: rw [@enum_lt_enum _ r, Subtype.mk_lt_mk]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
⊢ a.pred ≤ b ↔ a ≤ succ b
have inl : ∀ (a : Ordinal.{u_4}), (succ a).pred ≤ b ↔ succ a ≤ succ b
Tactic: obtain ⟨a, rfl⟩ | ha := mem_range_succ_or_isSuccPrelimit a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
inl : ∀ (a : Ordinal.{u_4}), (succ a).pred ≤ b ↔ succ a ≤ succ b
⊢ a.pred ≤ b ↔ a ≤ succ b
have inr : ∀ (ha : IsSuccPrelimit a), a.pred ≤ b ↔ a ≤ succ b
Tactic: obtain ⟨a, rfl⟩ | ha := mem_range_succ_or_isSuccPrelimit a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
⊢ a.pred ≤ b ↔ a ≤ succ b
have inr : a ≤ b ↔ a ≤ succ b
Tactic: rw [ha.ordinalPred_eq, ha.le_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
inr : a ≤ b ↔ a ≤ succ b
⊢ a.pred ≤ b ↔ a ≤ succ b
have inr₁ : a ≤ b ↔ a ≤ b
Tactic: rw [ha.ordinalPred_eq, ha.le_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
⊢ o.pred = o ↔ IsSuccPrelimit o
have inl : ∀ (a : Ordinal.{u_4}), (succ a).pred = succ a ↔ IsSuccPrelimit (succ a)
Tactic: obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
inl : ∀ (a : Ordinal.{u_4}), (succ a).pred = succ a ↔ IsSuccPrelimit (succ a)
⊢ o.pred = o ↔ IsSuccPrelimit o
have inr : ∀ (ho : IsSuccPrelimit o), o.pred = o ↔ IsSuccPrelimit o
Tactic: obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
ho : IsSuccPrelimit o
⊢ o.pred = o ↔ IsSuccPrelimit o
have inr : True ↔ IsSuccPrelimit o
Tactic: simp_rw [ho.ordinalPred_eq, ho]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
⊢ o.pred < o ↔ ¬IsSuccPrelimit o
have rw : o.pred ≠ o ↔ ¬IsSuccPrelimit o
Tactic: rw [(pred_le_self o).lt_iff_ne]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
⊢ succ o.pred = o ↔ ¬IsSuccPrelimit o
have rw : succ o.pred ≤ o ↔ ¬IsSuccPrelimit o
Tactic: rw [← (self_le_succ_pred o).ge_iff_eq', succ_le_iff, pred_lt_iff_not_isSuccPrelimit]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
rw : succ o.pred ≤ o ↔ ¬IsSuccPrelimit o
⊢ succ o.pred = o ↔ ¬IsSuccPrelimit o
have rw₁ : o.pred < o ↔ ¬IsSuccPrelimit o
Tactic: rw [← (self_le_succ_pred o).ge_iff_eq', succ_le_iff, pred_lt_iff_not_isSuccPrelimit]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
rw : succ o.pred ≤ o ↔ ¬IsSuccPrelimit o
rw₁ : o.pred < o ↔ ¬IsSuccPrelimit o
⊢ succ o.pred = o ↔ ¬IsSuccPrelimit o
have rw₂ : ¬IsSuccPrelimit o ↔ ¬IsSuccPrelimit o
Tactic: rw [← (self_le_succ_pred o).ge_iff_eq', succ_le_iff, pred_lt_iff_not_isSuccPrelimit]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{v}
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred
have inl : ∀ (a : Ordinal.{v}), lift.{u, v} (succ a).pred = (lift.{u, v} (succ a)).pred
Tactic: obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{v}
inl : ∀ (a : Ordinal.{v}), lift.{u, v} (succ a).pred = (lift.{u, v} (succ a)).pred
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred
have inr : ∀ (ho : IsSuccPrelimit o), lift.{u, v} o.pred = (lift.{u, v} o).pred
Tactic: obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred
have inr : lift.{u, v} o = (lift.{u, v} o).pred
Tactic: rwa [ho.ordinalPred_eq, eq_comm, pred_eq_iff_isSuccPrelimit, isSuccPrelimit_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{v}
ho : IsSuccPrelimit o
inr : lift.{u, v} o = (lift.{u, v} o).pred
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred
have inr₁ : (lift.{u, v} o).pred = lift.{u, v} o
Tactic: rwa [ho.ordinalPred_eq, eq_comm, pred_eq_iff_isSuccPrelimit, isSuccPrelimit_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{v}
ho : IsSuccPrelimit o
inr : lift.{u, v} o = (lift.{u, v} o).pred
inr₁ : (lift.{u, v} o).pred = lift.{u, v} o
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred
have inr₂ : IsSuccPrelimit (lift.{u, v} o)
Tactic: rwa [ho.ordinalPred_eq, eq_comm, pred_eq_iff_isSuccPrelimit, isSuccPrelimit_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (hypothesis)
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : Ordinal.IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
b : Ordinal.{u_4}
H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o
⊢ f b ≤ o ↔ ∀ a ∈ p, f a ≤ o
have hp : IsLUB (f '' p) (f b)
Tactic: have hp := H.map_isLUB ⟨(H₂ b).1 le_rfl, fun a ↦ (H₂ _).2⟩ p0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : Ordinal.IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
b : Ordinal.{u_4}
H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o
hp : IsLUB (f '' p) (f b)
⊢ f b ≤ o ↔ ∀ a ∈ p, f a ≤ o
have refine : ∀ (H : ∀ a ∈ p, f a ≤ o), o ∈ upperBounds (f '' p)
Tactic: refine ⟨fun hb a ha ↦ (hp.1 (mem_image_of_mem _ ha)).trans hb, fun H ↦ hp.2 ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : b ≤ a
⊢ b + (a - b) = a
have change : (b + if h : b ≤ a then Classical.choose (p := fun (x : Ordinal.{u_4}) ↦ a = b + x) sorry else 0) = a
Tactic: change b + dite _ _ _ = a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : b ≤ a
⊢ (b + if h : b ≤ a then Classical.choose (p := fun (x : Ordinal.{u_4}) ↦ a = b + x) ⋯ else 0) = a
have rw : b + Classical.choose (p := fun (x : Ordinal.{u_4}) ↦ a = b + x) sorry = a
Tactic: rw [dif_pos h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
⊢ a ≤ b + (a - b)
have inl : ∀ (h : b ≤ a), a ≤ b + (a - b)
Tactic: obtain h | h := le_or_gt b a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
inl : ∀ (h : b ≤ a), a ≤ b + (a - b)
⊢ a ≤ b + (a - b)
have inr : ∀ (h : a < b), a ≤ b + (a - b)
Tactic: obtain h | h := le_or_gt b a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
⊢ a - b ≤ c ↔ a ≤ b + c
have refine : ∀ (h : a ≤ b + c), a - b ≤ c
Tactic: refine ⟨fun h ↦ (le_add_sub a b).trans (by gcongr), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : a ≤ b + c
⊢ a - b ≤ c
have inl : ∀ (h' : b ≤ a), a - b ≤ c
Tactic: obtain h' | h' := le_or_gt b a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : a ≤ b + c
inl : ∀ (h' : b ≤ a), a - b ≤ c
⊢ a - b ≤ c
have inr : ∀ (h' : a < b), a - b ≤ c
Tactic: obtain h' | h' := le_or_gt b a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : b ≤ a
⊢ a - b ≤ c
have inl : b + (a - b) ≤ b + c
Tactic: rwa [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : b ≤ a
⊢ c ≤ a - b ↔ b + c ≤ a
have rw : b + c ≤ b + (a - b) ↔ b + c ≤ a
Tactic: rw [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : b ≤ a
rw : b + c ≤ b + (a - b) ↔ b + c ≤ a
⊢ c ≤ a - b ↔ b + c ≤ a
have rw₁ : b + c ≤ a ↔ b + c ≤ a
Tactic: rw [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c d : Ordinal.{u_4}
⊢ a - b - c ≤ d ↔ a - (b + c) ≤ d
have rw : a - b ≤ c + d ↔ a - (b + c) ≤ d
Tactic: rw [sub_le, sub_le, sub_le, add_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c d : Ordinal.{u_4}
rw : a - b ≤ c + d ↔ a - (b + c) ≤ d
⊢ a - b - c ≤ d ↔ a - (b + c) ≤ d
have rw₁ : a ≤ b + (c + d) ↔ a - (b + c) ≤ d
Tactic: rw [sub_le, sub_le, sub_le, add_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ a - b - c ≤ d ↔ a - (b + c) ≤ d
have rw₂ : a ≤ b + (c + d) ↔ a ≤ b + c + d
Tactic: rw [sub_le, sub_le, sub_le, add_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ a - b - c ≤ d ↔ a - (b + c) ≤ d
have rw₃ : a ≤ b + (c + d) ↔ a ≤ b + (c + d)
Tactic: rw [sub_le, sub_le, sub_le, add_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
⊢ a + b - (a + c) = b - c
have rw : a + b - a - c = b - c
Tactic: rw [← sub_sub, add_sub_cancel]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
rw : a + b - a - c = b - c
⊢ a + b - (a + c) = b - c
have rw₁ : b - c = b - c
Tactic: rw [← sub_sub, add_sub_cancel]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : b + c ≤ a
⊢ c ≤ a - b
have rw : b + c ≤ b + (a - b)
Tactic: rw [← add_le_add_iff_left b]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
⊢ a - b < c
have inl : ∀ (hab : a < b), a - b < c
Tactic: obtain hab | hba := lt_or_ge a b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
inl : ∀ (hab : a < b), a - b < c
⊢ a - b < c
have inr : ∀ (hba : b ≤ a), a - b < c
Tactic: obtain hab | hba := lt_or_ge a b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a < b + c ↔ ∃ d < c, a ≤ b + d
have mpr : (∃ d < c, a ≤ b + d) → a < b + c
Tactic: use fun h ↦ ⟨_, sub_lt_of_lt_add h hc.bot_lt, le_add_sub a b⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ a < b + c ↔ ∃ d < c, a < b + d
have rw : (∃ d < c, a ≤ b + d) ↔ ∃ d < c, a < b + d
Tactic: rw [lt_add_iff hc.ne_bot]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a ≤ b + d) ↔ ∃ d < c, a < b + d
have mp : (∃ d < c, a ≤ b + d) → ∃ d < c, a < b + d
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
mp : (∃ d < c, a ≤ b + d) → ∃ d < c, a < b + d
⊢ (∃ d < c, a ≤ b + d) ↔ ∃ d < c, a < b + d
have mpr : (∃ d < c, a < b + d) → ∃ d < c, a ≤ b + d
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
have mp : a < b + succ d
Tactic: refine ⟨_, hc.succ_lt hd, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ a < b + succ d
have mp : a < b + (d + 1)
Tactic: rwa [succ_eq_add_one, ← add_assoc, lt_add_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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)
⊢ a < b + succ d
have mp₁ : a < b + d + 1
Tactic: rwa [succ_eq_add_one, ← add_assoc, lt_add_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
⊢ IsNormal (β := Ordinal.{u_4}) fun (x : Ordinal.{u_4}) ↦ a + x
have 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
Tactic: rw [isNormal_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
⊢ IsSuccLimit (a - b)
have rw : b < a ∧ ∀ a_1 < a - b, succ a_1 < a - b
Tactic: rw [isSuccLimit_iff, Ordinal.sub_ne_zero_iff_lt, isSuccPrelimit_iff_succ_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
⊢ b < a ∧ ∀ a_1 < a - b, succ a_1 < a - b
have refine : ∀ (c : Ordinal.{u_4}) (hc : c < a - b), succ c < a - b
Tactic: refine ⟨h, fun c hc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : c < a - b
⊢ succ c < a - b
have rw : ∀ (hc : b + c < a), b + succ c < a
Tactic: rw [lt_sub] at hc ⊢
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + succ c < a
have rw : b + c + 1 < a
Tactic: rw [succ_eq_add_one, ← add_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
⊢ a * b = 0 ↔ a = 0 ∨ b = 0
have type : ∀ (α : Type u_4) (r : α → α → Prop) [inst : IsWellOrder α r] (β : Type u_4) (s : β → β → Prop)
  [inst_1 : IsWellOrder β s], type r * type s = 0 ↔ type r = 0 ∨ type s = 0
Tactic: induction a, b using inductionOn₂ with | _ α _ β _
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_4
r : α → α → Prop
inst : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst_1 : IsWellOrder β s
⊢ type r * type s = 0 ↔ type r = 0 ∨ type s = 0
have type : type (Prod.Lex s r) = 0 ↔ type r = 0 ∨ type s = 0
Tactic: simp_rw [← type_prod_lex, type_eq_zero_iff_isEmpty, isEmpty_prod, iff_true_intro or_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ Ordinal.type r * Ordinal.type s = 0 ↔ Ordinal.type r = 0 ∨ Ordinal.type s = 0
have type₁ : IsEmpty.{u_4 + 1} (β × α) ↔ IsEmpty α ∨ IsEmpty β
Tactic: simp_rw [← type_prod_lex, type_eq_zero_iff_isEmpty, isEmpty_prod, iff_true_intro or_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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 β
⊢ Ordinal.type r * Ordinal.type s = 0 ↔ Ordinal.type r = 0 ∨ Ordinal.type s = 0
have type₂ : IsEmpty β ∨ IsEmpty α ↔ IsEmpty α ∨ IsEmpty β
Tactic: simp_rw [← type_prod_lex, type_eq_zero_iff_isEmpty, isEmpty_prod, iff_true_intro or_comm]
-- 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
⊢ ⟦{ α := γ, 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} }⟧
have 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)
Tactic: refine
        (RelEmbedding.ofMonotone (fun a : α × γ => (f a.1, 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 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)
have 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₂))
Tactic: obtain ⟨-, -, h'⟩ | ⟨-, h'⟩ := h
Cleared hypotheses: a, b, h