awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
inl :
  ∀ (c0 : LT.lt.{u + 1} (α := Ordinal.{u}) 0 0) (ha : a < HPow.hPow (β := Ordinal.{u}) ω 0),
    a * b < HPow.hPow (β := Ordinal.{u}) ω 0
inr : ∀ (c : Ordinal.{u}) (c0 : 0 < succ c) (ha : a < ω ^ succ c), a * b < ω ^ succ c
⊢ a * b < ω ^ c
have inr₁ : ∀ (l : IsSuccLimit c), a * b < ω ^ c
Tactic: rcases zero_or_succ_or_isSuccLimit c with (rfl | ⟨c, rfl⟩ | l)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (hypothesis)
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ succ c
⊢ a * b < ω ^ succ c
have ha₁ : a < ω ^ c * ω
Tactic: rw [opow_succ] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
⊢ a * b < ω ^ succ c
have inr : ∀ (n : Ordinal.{u}) (hn : n < ω) (an : a < ω ^ c * n), a * b < ω ^ succ c
Tactic: obtain ⟨n, hn, an⟩ :=
      ((isNormal_mul_right <| opow_pos _ omega0_pos).lt_iff_exists_lt isSuccLimit_omega0).1 ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ a * b < ω ^ succ c
have inr : ω ^ c * (n * b) < ω ^ c * ω
Tactic: grw [an, opow_succ, mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ ω ^ c * (n * b) < ω ^ c * ω
have inr : 0 < ω ^ c
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
inr : 0 < ω ^ c
⊢ ω ^ c * (n * b) < ω ^ c * ω
have inr₁ : n * b < ω
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
⊢ a * b < ω ^ c
have inr : ∀ (x : Ordinal.{u}) (hx : x < c) (ax : a < ω ^ x), a * b < ω ^ c
Tactic: rcases ((isNormal_opow one_lt_omega0).lt_iff_exists_lt l).1 ha with ⟨x, hx, ax⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ a * b < ω ^ c
have inr : ω ^ x * ω < ω ^ c
Tactic: refine (mul_le_mul' (le_of_lt ax) (le_of_lt hb)).trans_lt ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ ω ^ x * ω < ω ^ c
have inr : succ x < c
Tactic: rw [← opow_succ, opow_lt_opow_iff_right one_lt_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
have inl : ∀ (h : a < ω ^ HPow.hPow (β := Ordinal.{u}) ω 0),
  a * ω ^ HPow.hPow (β := Ordinal.{u}) ω 0 = ω ^ HPow.hPow (β := Ordinal.{u}) ω 0
Tactic: obtain rfl | b0 := eq_or_ne b 0
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
inl :
  ∀ (h : a < ω ^ HPow.hPow (β := Ordinal.{u}) ω 0),
    a * ω ^ HPow.hPow (β := Ordinal.{u}) ω 0 = ω ^ HPow.hPow (β := Ordinal.{u}) ω 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
have inr : ∀ (b0 : b ≠ 0), a * ω ^ ω ^ b = ω ^ ω ^ b
Tactic: obtain rfl | b0 := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ HPow.hPow (β := Ordinal.{u}) ω 0
⊢ a * ω ^ HPow.hPow (β := Ordinal.{u}) ω 0 = ω ^ HPow.hPow (β := Ordinal.{u}) ω 0
have inl : ∀ (h : a < ω), a * ω = ω
Tactic: rw [opow_zero, opow_one] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
have inr : a * ω ^ ω ^ b ≤ ω ^ ω ^ b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
inr : a * ω ^ ω ^ b ≤ ω ^ ω ^ b
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
have inr₁ : ω ^ ω ^ b ≤ a * ω ^ ω ^ b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b
have inr : ∀ (x : Ordinal.{u}) (xb : x < ω ^ b) (ax : a < ω ^ x), a * ω ^ ω ^ b ≤ ω ^ ω ^ b
Tactic: obtain ⟨x, xb, ax⟩ :=
        (lt_opow_of_isSuccLimit omega0_ne_zero (isSuccLimit_opow_left isSuccLimit_omega0 b0)).1 h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
x : Ordinal.{u}
xb : x < ω ^ b
ax : a < ω ^ x
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b
have inr : ω ^ x * ω ^ ω ^ b ≤ ω ^ ω ^ b
Tactic: grw [ax, ← opow_add, add_omega0_opow xb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
x : Ordinal.{u}
xb : x < ω ^ b
ax : a < ω ^ x
inr : ω ^ x * ω ^ ω ^ b ≤ ω ^ ω ^ b
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b
have inr₁ : ω ^ (x + ω ^ b) ≤ ω ^ ω ^ b
Tactic: grw [ax, ← opow_add, add_omega0_opow xb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
x : Ordinal.{u}
xb : x < ω ^ b
ax : a < ω ^ x
inr : ω ^ x * ω ^ ω ^ b ≤ ω ^ ω ^ b
inr₁ : ω ^ (x + ω ^ b) ≤ ω ^ ω ^ b
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b
have inr₂ : ω ^ ω ^ b ≤ ω ^ ω ^ b
Tactic: grw [ax, ← opow_add, add_omega0_opow xb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
| ω ^ ω ^ b
have rw : 1 * ω ^ ω ^ b
Tactic: rw [← one_mul (ω ^ _)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ ω ^ ω ^ b ≤ a * ω ^ ω ^ b
have inr : 1 * ω ^ ω ^ b ≤ a * ω ^ ω ^ b
Tactic: conv_lhs => rw [← one_mul (ω ^ _)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ 1 * ω ^ ω ^ b ≤ a * ω ^ ω ^ b
have inr : a * ω ^ ω ^ b ≤ a * ω ^ ω ^ b
Tactic: grw [one_le_iff_pos.2 a0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (hypothesis)
Goal:
b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) x y < o
have this : (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) (b ^ x) (b ^ y) < b ^ o
Tactic: have := ho ((opow_lt_opow_iff_right hb).2 hx) ((opow_lt_opow_iff_right hb).2 hy)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : b ^ x * b ^ y < b ^ o
⊢ x + y < o
have rwa : ∀ (this : b ^ (x + y) < b ^ o), x + y < o
Tactic: rwa [← opow_add, opow_lt_opow_iff_right hb] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : b ^ x * b ^ y < b ^ o
rwa : ∀ (this : b ^ (x + y) < b ^ o), x + y < o
⊢ x + y < o
have rwa₁ : ∀ (this : x + y < o), x + y < o
Tactic: rwa [← opow_add, opow_lt_opow_iff_right hb] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o ↔
    o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
have refine_1 : ∀ (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o),
  o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
Tactic: refine ⟨fun ho => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
refine_1 :
  ∀ (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o),
    o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o ↔
    o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
have refine_2 : o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o →
  IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
Tactic: refine ⟨fun ho => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
⊢ o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
have refine_1 : ∀ (ho₂ : o ≤ 2), o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
Tactic: rcases le_or_gt o 2 with ho₂ | ho₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
refine_1 :
  ∀ (ho₂ : o ≤ 2), o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
⊢ o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
have refine_1₁ : ∀ (ho₂ : 2 < o), o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
Tactic: rcases le_or_gt o 2 with ho₂ | ho₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
have refine_1 : ∀ (ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0) (ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 0),
  LE.le.{u + 1} (α := Ordinal.{u}) 0 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) 0
Tactic: rcases isPrincipal_add_iff_zero_or_omega0_opow.1
        (isPrincipal_add_of_isPrincipal_mul ho ho₂.ne') with (rfl | ⟨a, rfl⟩)
Cleared hypotheses: o, ho, ho₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂ : 2 < o
refine_1 :
  ∀ (ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0) (ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 0),
    LE.le.{u + 1} (α := Ordinal.{u}) 0 2 ∨
      Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) 0
⊢ o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
have refine_1₁ : ∀ (a : Ordinal.{u}) (ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) ((fun (x : Ordinal.{u}) ↦ ω ^ x) a))
  (ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)),
  LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) a) 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
      ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)
Tactic: rcases isPrincipal_add_iff_zero_or_omega0_opow.1
        (isPrincipal_add_of_isPrincipal_mul ho ho₂.ne') with (rfl | ⟨a, rfl⟩)
Cleared hypotheses: o, ho, ho₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a : Ordinal.{u}
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)
ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)
⊢ LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) a) 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
      ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)
have refine_1 : ∀ (ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0))
  (ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0)),
  LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0) 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
      ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0)
Tactic: rcases isPrincipal_add_iff_zero_or_omega0_opow.1
          (isPrincipal_add_of_isPrincipal_mul_opow one_lt_omega0 ho) with (rfl | ⟨b, rfl⟩)
Cleared hypotheses: a, ho, ho₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a : Ordinal.{u}
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)
ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)
refine_1 :
  ∀ (ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0))
    (ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0)),
    LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0) 2 ∨
      Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
        ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0)
⊢ LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) a) 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
      ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)
have refine_1₁ : ∀ (b : Ordinal.{u})
  (ho :
    IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2)
      ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b)))
  (ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b))),
  LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b)) 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
      ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b))
Tactic: rcases isPrincipal_add_iff_zero_or_omega0_opow.1
          (isPrincipal_add_of_isPrincipal_mul_opow one_lt_omega0 ho) with (rfl | ⟨b, rfl⟩)
Cleared hypotheses: a, ho, ho₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a : Ordinal.{u}
a0 : 0 < a
ha : a < ω
b : Ordinal.{u}
⊢ a * (ω * b) = ω * b
have rw : a * ω * b = ω * b
Tactic: rw [← mul_assoc, mul_omega0 a0 ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a : Ordinal.{u}
a0 : 0 < a
ha : a < ω
b : Ordinal.{u}
rw : a * ω * b = ω * b
⊢ a * (ω * b) = ω * b
have rw₁ : ω * b = ω * b
Tactic: rw [← mul_assoc, mul_omega0 a0 ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
⊢ a * b = b ^ succ (log b a)
have a₁ : a * b ≤ b ^ succ (log b a)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
a₁ : a * b ≤ b ^ succ (log b a)
⊢ a * b = b ^ succ (log b a)
have a₂ : b ^ succ (log b a) ≤ a * b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (hypothesis)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
⊢ a * b ≤ b ^ succ (log b a)
have hbl : IsSuccLimit b
Tactic: have hbl := isSuccLimit_of_isPrincipal_mul hb₂ hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
⊢ a * b ≤ b ^ succ (log b a)
have a₁ : ∀ (i : (↑(Set.Iio b) : Type (u + 1))), a * (↑i : Ordinal.{u}) ≤ b ^ succ (log b a)
Tactic: rw [(isNormal_mul_right (pos_iff_ne_zero.2 ha)).apply_of_isSuccLimit hbl,
      Ordinal.iSup_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (hypothesis)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
⊢ a * (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio b) c hcb) : Ordinal.{u}) ≤ b ^ succ (log b a)
have hb₁ : 1 < b
Tactic: have hb₁ : 1 < b := one_lt_two.trans hb₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (hypothesis)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
⊢ a * (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio b) c hcb) : Ordinal.{u}) ≤ b ^ succ (log b a)
have hbo₀ : b ^ log b a ≠ 0
Tactic: have hbo₀ : b ^ log b a ≠ 0 := pos_iff_ne_zero.1 (opow_pos _ (zero_lt_one.trans hb₁))
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a * (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio b) c hcb) : Ordinal.{u}) ≤ b ^ succ (log b a)
have a₁ : b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)
Tactic: apply (mul_le_mul_left (le_of_lt (lt_mul_succ_div a hbo₀)) c).trans
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)
have a₁ : b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ log b a * b
Tactic: rw [mul_assoc, opow_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ log b a * b
have a₁ : succ (a / b ^ log b a) * c ≤ b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ succ (a / b ^ log b a) * c ≤ b
have a₁ : a / b ^ log b a < b
Tactic: refine (hb (hbl.succ_lt ?_) hcb).le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a / b ^ log b a < b
have a₁ : a < b ^ succ (log b a)
Tactic: rw [← lt_mul_iff_div_lt hbo₀, ← opow_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
⊢ b ^ succ (log b a) ≤ a * b
have a₁ : b ^ log b a * b ≤ a * b
Tactic: grw [opow_succ, opow_log_le_self b ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
a₁ : b ^ log b a * b ≤ a * b
⊢ b ^ succ (log b a) ≤ a * b
have a₂ : a * b ≤ a * b
Tactic: grw [opow_succ, opow_log_le_self b ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (goal)
Goal:
α : Type u
a b : α
r : α → α → Prop
hb : Acc r b
h : r a b
⊢ Order.succ (⋯.rank (r := r)) ≤ hb.rank (r := r)
have rw : Order.succ (sorry.rank (r := r)) ≤ ⨆ (b_1 : { b_1 : α // r b_1 b }), Order.succ (sorry.rank (r := r))
Tactic: rw [hb.rank_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (goal)
Goal:
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho : o ≤ ha.rank (r := r)
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
have inl : ∀ (ho : ha.rank (r := r) ≤ ha.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = ha.rank (r := r)
Tactic: obtain rfl | ho := ho.eq_or_lt
Cleared hypotheses: o, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (goal)
Goal:
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho : o ≤ ha.rank (r := r)
inl : ∀ (ho : ha.rank (r := r) ≤ ha.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = ha.rank (r := r)
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
have inr : ∀ (ho : o < ha.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
Tactic: obtain rfl | ho := ho.eq_or_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (goal)
Goal:
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho_1 : o ≤ ha.rank (r := r)
ho : o < ha.rank (r := r)
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
have inr : ∀ (ho : o < ha.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
Tactic: revert ho
Cleared hypotheses: ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (goal)
Goal:
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho : o ≤ ha.rank (r := r)
⊢ ∀ (ho : o < ha.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
have inr : ∀ (a : α) (ha : ∀ (y : α), r y a → Acc r y)
  (IH : ∀ (y : α) (a : r y a) (ho : o < sorry.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o)
  (ho : o < sorry.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
Tactic: refine ha.recOn fun a ha IH ho ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (hypothesis)
Goal:
α : Type u
a_1 : α
r : α → α → Prop
o : Ordinal.{u}
ha_1 : Acc r a_1
ho_1 : o ≤ ha_1.rank (r := r)
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a) (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
ho : o < ⋯.rank (r := r)
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
have ho₁ : ∃ (i : { b : α // r b a }), o < Order.succ (sorry.rank (r := r))
Tactic: rw [rank_eq, Ordinal.lt_iSup_iff] at ho
Cleared hypotheses: ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (goal)
Goal:
α : Type u
a_1 : α
r : α → α → Prop
o : Ordinal.{u}
ha_1 : Acc r a_1
ho_1 : o ≤ ha_1.rank (r := r)
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a) (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
ho : ∃ (i : { b : α // r b a }), o < Order.succ (⋯.rank (r := r))
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
have inr : ∀ (b : α) (hb : r b a)
  (ho : o < Order.succ (rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) sorry)),
  ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
Tactic: obtain ⟨⟨b, hb⟩, ho⟩ := ho
Cleared hypotheses: ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Rank (hypothesis)
Goal:
α : Type u
a_1 : α
r : α → α → Prop
o : Ordinal.{u}
ha_1 : Acc r a_1
ho_1 : o ≤ ha_1.rank (r := r)
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a) (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
b : α
hb : r b a
ho : o < Order.succ (rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯)
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
have ho₁ : o ≤ rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) sorry
Tactic: rw [Order.lt_succ_iff] at ho
Cleared hypotheses: ho