awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h : o₂ ≤ o₁
simp_rw : veblenWith f o₁ (veblenWith f o₂ a) ≠ veblenWith f o₂ a ↔ veblenWith f o₁ a ≠ a
⊢ veblenWith f o₂ a < veblenWith f o₁ (veblenWith f o₂ a) ↔ a < veblenWith f o₁ a
have simp_rw₁ : ¬veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a ↔ ¬veblenWith f o₁ a = a
Tactic: simp_rw [(right_le_veblenWith hf ..).lt_iff_ne', ne_eq,
    veblenWith_veblenWith_eq_veblenWith_iff hf h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match (motive := Ordering → Ordering) cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b
have inl : ∀ (h : o₁ < o₂),
  cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match (motive := Ordering → Ordering) cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b
Tactic: obtain h | rfl | h := lt_trichotomy o₁ o₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
inl :
  ∀ (h : o₁ < o₂),
    cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
      match (motive := Ordering → Ordering) cmp o₁ o₂ with
      | Ordering.eq => cmp a b
      | Ordering.lt => cmp a (veblenWith f o₂ b)
      | Ordering.gt => cmp (veblenWith f o₁ a) b
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match (motive := Ordering → Ordering) cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b
have inr : cmp (veblenWith f o₁ a) (veblenWith f o₁ b) =
  match (motive := Ordering → Ordering) cmp o₁ o₁ with
  | Ordering.eq => cmp a b
  | Ordering.lt => cmp a (veblenWith f o₁ b)
  | Ordering.gt => cmp (veblenWith f o₁ a) b
Tactic: obtain h | rfl | h := lt_trichotomy o₁ o₂
Cleared hypotheses: o₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
inl :
  ∀ (h : o₁ < o₂),
    cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
      match (motive := Ordering → Ordering) cmp o₁ o₂ with
      | Ordering.eq => cmp a b
      | Ordering.lt => cmp a (veblenWith f o₂ b)
      | Ordering.gt => cmp (veblenWith f o₁ a) b
inr :
  cmp (veblenWith f o₁ a) (veblenWith f o₁ b) =
    match (motive := Ordering → Ordering) cmp o₁ o₁ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₁ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match (motive := Ordering → Ordering) cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b
have inr₁ : ∀ (h : o₂ < o₁),
  cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match (motive := Ordering → Ordering) cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b
Tactic: obtain h | rfl | h := lt_trichotomy o₁ o₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
| cmp (veblenWith f o₁ a) (veblenWith f o₂ b)
have rw : cmp (veblenWith f o₁ a) (veblenWith f o₁ (veblenWith f o₂ b))
Tactic: rw [← veblenWith_veblenWith_of_lt hf h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match (motive := Ordering → Ordering) cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b
have inl : cmp (veblenWith f o₁ a) (veblenWith f o₁ (veblenWith f o₂ b)) =
  match (motive := Ordering → Ordering) cmp o₁ o₂ with
  | Ordering.eq => cmp a b
  | Ordering.lt => cmp a (veblenWith f o₂ b)
  | Ordering.gt => cmp (veblenWith f o₁ a) b
Tactic: conv_lhs => rw [← veblenWith_veblenWith_of_lt hf h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
| cmp (veblenWith f o₁ a) (veblenWith f o₂ b)
have rw : cmp (veblenWith f o₂ (veblenWith f o₁ a)) (veblenWith f o₂ b)
Tactic: rw [← veblenWith_veblenWith_of_lt hf h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match (motive := Ordering → Ordering) cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b
have inr : cmp (veblenWith f o₂ (veblenWith f o₁ a)) (veblenWith f o₂ b) =
  match (motive := Ordering → Ordering) cmp o₁ o₂ with
  | Ordering.eq => cmp a b
  | Ordering.lt => cmp a (veblenWith f o₂ b)
  | Ordering.gt => cmp (veblenWith f o₁ a) b
Tactic: conv_lhs => rw [← veblenWith_veblenWith_of_lt hf h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a < veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b
have rw : (match (motive := Ordering → Ordering) cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b) =
    Ordering.lt ↔
  o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b
Tactic: rw [← cmp_eq_lt_iff, cmp_veblenWith hf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a ≤ veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b
have rw : ¬(match (motive := Ordering → Ordering) cmp o₁ o₂ with
      | Ordering.eq => cmp a b
      | Ordering.lt => cmp a (veblenWith f o₂ b)
      | Ordering.gt => cmp (veblenWith f o₁ a) b) =
      Ordering.gt ↔
  o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b
Tactic: rw [← not_lt, ← cmp_eq_gt_iff, cmp_veblenWith hf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a = veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b
have rw : (match (motive := Ordering → Ordering) cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b) =
    Ordering.eq ↔
  o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b
Tactic: rw [← cmp_eq_eq_iff, cmp_veblenWith hf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
⊢ veblen 0 = fun (a : Ordinal.{u_1}) ↦ ω ^ a
have rw : veblenWith (fun (x : Ordinal.{u_1}) ↦ ω ^ x) 0 = fun (a : Ordinal.{u_1}) ↦ ω ^ a
Tactic: rw [veblen, veblenWith_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
rw : veblenWith (fun (x : Ordinal.{u_1}) ↦ ω ^ x) 0 = fun (a : Ordinal.{u_1}) ↦ ω ^ a
⊢ veblen 0 = fun (a : Ordinal.{u_1}) ↦ ω ^ a
have rw₁ : Eq.{u_1 + 2} (α := Ordinal.{u_1} → Ordinal.{u_1}) (fun (x : Ordinal.{u_1}) ↦ ω ^ x) fun (a : Ordinal.{u_1}) ↦ ω ^ a
Tactic: rw [veblen, veblenWith_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a : Ordinal.{u_1}
⊢ veblen 0 a = ω ^ a
have rw : (fun (a : Ordinal.{u_1}) ↦ ω ^ a) a = ω ^ a
Tactic: rw [veblen_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a : Ordinal.{u_1}
⊢ a < veblen a a
have inl : 0 < veblen 0 0
Tactic: obtain rfl | h := eq_zero_or_pos a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a : Ordinal.{u_1}
inl : 0 < veblen 0 0
⊢ a < veblen a a
have inr : ∀ (h : 0 < a), a < veblen a a
Tactic: obtain rfl | h := eq_zero_or_pos a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a : Ordinal.{u_1}
h : 0 < a
⊢ a < veblen a a
have inr : veblen a 0 < veblen a a
Tactic: apply (left_le_veblen a 0).trans_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a : Ordinal.{u}
⊢ a < veblen o a ↔ a.invVeblen₁ ≤ o
have inl : ∀ (h : o < a.invVeblen₁), a < veblen o a ↔ a.invVeblen₁ ≤ o
Tactic: obtain h | h := lt_or_ge o (invVeblen₁ a)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a : Ordinal.{u}
inl : ∀ (h : o < a.invVeblen₁), a < veblen o a ↔ a.invVeblen₁ ≤ o
⊢ a < veblen o a ↔ a.invVeblen₁ ≤ o
have inr : ∀ (h : a.invVeblen₁ ≤ o), a < veblen o a ↔ a.invVeblen₁ ≤ o
Tactic: obtain h | h := lt_or_ge o (invVeblen₁ a)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a : Ordinal.{u}
h : o < a.invVeblen₁
⊢ a < veblen o a ↔ a.invVeblen₁ ≤ o
have inl : a < a ↔ a.invVeblen₁ ≤ o
Tactic: rw [veblen_eq_of_lt_invVeblen₁ h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o x : Ordinal.{u}
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁
have inl : ∀ (h : o < x.invVeblen₁), ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁
Tactic: obtain h | rfl | h := lt_trichotomy o (invVeblen₁ x)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o x : Ordinal.{u}
inl : ∀ (h : o < x.invVeblen₁), ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁
have inr : ω ^ x ∈ range (veblen x.invVeblen₁) ↔ x.invVeblen₁ ≤ x.invVeblen₁
Tactic: obtain h | rfl | h := lt_trichotomy o (invVeblen₁ x)
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o x : Ordinal.{u}
inl : ∀ (h : o < x.invVeblen₁), ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁
inr : ω ^ x ∈ range (veblen x.invVeblen₁) ↔ x.invVeblen₁ ≤ x.invVeblen₁
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁
have inr₁ : ∀ (h : x.invVeblen₁ < o), ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁
Tactic: obtain h | rfl | h := lt_trichotomy o (invVeblen₁ x)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u}
⊢ ω ^ x ∈ range (veblen x.invVeblen₁) ↔ x.invVeblen₁ ≤ x.invVeblen₁
have apply : ω ^ x ∈ range (veblen x.invVeblen₁)
Tactic: apply iff_of_true _ le_rfl
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u}
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)
have pos : ∀ (h : x.invVeblen₁ = 0), ω ^ x ∈ range (veblen x.invVeblen₁)
Tactic: by_cases h : invVeblen₁ x = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u}
pos : ∀ (h : x.invVeblen₁ = 0), ω ^ x ∈ range (veblen x.invVeblen₁)
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)
have neg : ∀ (h : ¬x.invVeblen₁ = 0), ω ^ x ∈ range (veblen x.invVeblen₁)
Tactic: by_cases h : invVeblen₁ x = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u}
h : ¬x.invVeblen₁ = 0
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)
have neg : ∀ b < x.invVeblen₁, veblen b x = x
Tactic: simp_rw [mem_range_veblen h, veblen_opow_eq_opow_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁
have apply : ω ^ x ∉ range (veblen o)
Tactic: apply iff_of_false _ h.not_ge
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (hypothesis)
Goal:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz hz' : veblen o z = ω ^ x
⊢ False
have hz₁ : veblen x.invVeblen₁ x = x
Tactic: rw [← veblen_veblen_of_lt h, hz', veblen_opow_eq_opow_iff] at hz
Cleared hypotheses: hz, hz'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a : Ordinal.{u}
h : a < veblen o a
⊢ (veblen o a).invVeblen₁ = o
have a₁ : (veblen o a).invVeblen₁ ≤ o
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a : Ordinal.{u}
h : a < veblen o a
a₁ : (veblen o a).invVeblen₁ ≤ o
⊢ (veblen o a).invVeblen₁ = o
have a₂ : o ≤ (veblen o a).invVeblen₁
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a : Ordinal.{u}
h : a < veblen o a
⊢ (veblen o a).invVeblen₁ ≤ o
have a₁ : veblen o a < veblen o (veblen o a)
Tactic: rwa [← lt_veblen_iff_invVeblen₁_le, veblen_lt_veblen_iff_right]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a : Ordinal.{u}
h : a < veblen o a
⊢ o ≤ (veblen o a).invVeblen₁
have a₁ : ω ^ veblen o a ∈ range (veblen o)
Tactic: rw [← mem_range_veblen_iff_le_invVeblen₁]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a : Ordinal.{u}
h : a < veblen o a
⊢ ω ^ veblen o a ∈ range (veblen o)
have a₁ : ∀ (h : a < veblen 0 a), ω ^ veblen 0 a ∈ range (veblen 0)
Tactic: obtain rfl | ho := eq_zero_or_pos o
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a : Ordinal.{u}
h : a < veblen o a
a₁ : ∀ (h : a < veblen 0 a), ω ^ veblen 0 a ∈ range (veblen 0)
⊢ ω ^ veblen o a ∈ range (veblen o)
have a₂ : ∀ (ho : 0 < o), ω ^ veblen o a ∈ range (veblen o)
Tactic: obtain rfl | ho := eq_zero_or_pos o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ ω ^ veblen o a ∈ range (veblen o)
have a₁ : veblen o a ∈ range (veblen o)
Tactic: rw [← veblen_zero_apply, veblen_veblen_of_lt ho]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a : Ordinal.{u}
h : a < ω ^ a
⊢ a.invVeblen₁ = 0
have rwa : a.invVeblen₁ ≤ 0
Tactic: rwa [← nonpos_iff_eq_zero, ← lt_veblen_iff_invVeblen₁_le, veblen_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a : Ordinal.{u}
h : a < ω ^ a
rwa : a.invVeblen₁ ≤ 0
⊢ a.invVeblen₁ = 0
have rwa₁ : a < veblen 0 a
Tactic: rwa [← nonpos_iff_eq_zero, ← lt_veblen_iff_invVeblen₁_le, veblen_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a x : Ordinal.{u}
⊢ x.invVeblen₂ = a ↔ ω ^ x = veblen x.invVeblen₁ a
have rw : veblen x.invVeblen₁ x.invVeblen₂ = veblen x.invVeblen₁ a ↔ ω ^ x = veblen x.invVeblen₁ a
Tactic: rw [← veblen_inj (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a x : Ordinal.{u}
rw : veblen x.invVeblen₁ x.invVeblen₂ = veblen x.invVeblen₁ a ↔ ω ^ x = veblen x.invVeblen₁ a
⊢ x.invVeblen₂ = a ↔ ω ^ x = veblen x.invVeblen₁ a
have rw₁ : ω ^ x = veblen x.invVeblen₁ a ↔ ω ^ x = veblen x.invVeblen₁ a
Tactic: rw [← veblen_inj (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a x : Ordinal.{u}
⊢ x.invVeblen₂ < a ↔ ω ^ x < veblen x.invVeblen₁ a
have rw : veblen x.invVeblen₁ x.invVeblen₂ < veblen x.invVeblen₁ a ↔ ω ^ x < veblen x.invVeblen₁ a
Tactic: rw [← veblen_lt_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a x : Ordinal.{u}
rw : veblen x.invVeblen₁ x.invVeblen₂ < veblen x.invVeblen₁ a ↔ ω ^ x < veblen x.invVeblen₁ a
⊢ x.invVeblen₂ < a ↔ ω ^ x < veblen x.invVeblen₁ a
have rw₁ : ω ^ x < veblen x.invVeblen₁ a ↔ ω ^ x < veblen x.invVeblen₁ a
Tactic: rw [← veblen_lt_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a x : Ordinal.{u}
⊢ x.invVeblen₂ ≤ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a
have rw : veblen x.invVeblen₁ x.invVeblen₂ ≤ veblen x.invVeblen₁ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a
Tactic: rw [← veblen_le_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a x : Ordinal.{u}
rw : veblen x.invVeblen₁ x.invVeblen₂ ≤ veblen x.invVeblen₁ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a
⊢ x.invVeblen₂ ≤ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a
have rw₁ : ω ^ x ≤ veblen x.invVeblen₁ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a
Tactic: rw [← veblen_le_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a x : Ordinal.{u}
⊢ a < x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x
have rw : veblen x.invVeblen₁ a < veblen x.invVeblen₁ x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x
Tactic: rw [← veblen_lt_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a x : Ordinal.{u}
rw : veblen x.invVeblen₁ a < veblen x.invVeblen₁ x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x
⊢ a < x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x
have rw₁ : veblen x.invVeblen₁ a < ω ^ x ↔ veblen x.invVeblen₁ a < ω ^ x
Tactic: rw [← veblen_lt_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a x : Ordinal.{u}
⊢ a ≤ x.invVeblen₂ ↔ veblen x.invVeblen₁ a ≤ ω ^ x
have rw : veblen x.invVeblen₁ a ≤ veblen x.invVeblen₁ x.invVeblen₂ ↔ veblen x.invVeblen₁ a ≤ ω ^ x
Tactic: rw [← veblen_le_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a x : Ordinal.{u}
rw : veblen x.invVeblen₁ a ≤ veblen x.invVeblen₁ x.invVeblen₂ ↔ veblen x.invVeblen₁ a ≤ ω ^ x
⊢ a ≤ x.invVeblen₂ ↔ veblen x.invVeblen₁ a ≤ ω ^ x
have rw₁ : veblen x.invVeblen₁ a ≤ ω ^ x ↔ veblen x.invVeblen₁ a ≤ ω ^ x
Tactic: rw [← veblen_le_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u_1}
⊢ x.invVeblen₂ < ω ^ x
have rw : x < veblen x.invVeblen₁ x
Tactic: rw [invVeblen₂_lt_iff, opow_lt_veblen_opow_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u_1}
⊢ x.invVeblen₂ ≤ x
have inl : ∀ (h : x.invVeblen₁ = 0), x.invVeblen₂ ≤ x
Tactic: obtain h | h := eq_zero_or_pos (invVeblen₁ x)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u_1}
inl : ∀ (h : x.invVeblen₁ = 0), x.invVeblen₂ ≤ x
⊢ x.invVeblen₂ ≤ x
have inr : ∀ (h : 0 < x.invVeblen₁), x.invVeblen₂ ≤ x
Tactic: obtain h | h := eq_zero_or_pos (invVeblen₁ x)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u_1}
h : x.invVeblen₁ = 0
⊢ x.invVeblen₂ ≤ x
have inl : ω ^ x ≤ veblen x.invVeblen₁ x
Tactic: rw [invVeblen₂_le_iff, h, veblen_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u_1}
h : x.invVeblen₁ = 0
inl : ω ^ x ≤ veblen x.invVeblen₁ x
⊢ x.invVeblen₂ ≤ x
have inl₁ : ω ^ x ≤ veblen 0 x
Tactic: rw [invVeblen₂_le_iff, h, veblen_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u_1}
h : x.invVeblen₁ = 0
inl : ω ^ x ≤ veblen x.invVeblen₁ x
inl₁ : ω ^ x ≤ veblen 0 x
⊢ x.invVeblen₂ ≤ x
have inl₂ : ω ^ x ≤ ω ^ x
Tactic: rw [invVeblen₂_le_iff, h, veblen_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u_1}
h : 0 < x.invVeblen₁
⊢ x.invVeblen₂ ≤ x
have h₁ : x = ω ^ x
Tactic: convert! (invVeblen₂_lt x).le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u_1}
h : 0 < x.invVeblen₁
⊢ x = ω ^ x
have h₁ : x = veblen 0 x
Tactic: rw [← veblen_zero_apply, veblen_eq_of_lt_invVeblen₁ h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
x : Ordinal.{u_1}
h : 0 < x.invVeblen₁
h₁ : x = veblen 0 x
⊢ x = ω ^ x
have h₂ : x = x
Tactic: rw [← veblen_zero_apply, veblen_eq_of_lt_invVeblen₁ h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a : Ordinal.{u}
h : a < ω ^ a
⊢ a.invVeblen₂ = a
have rw : ω ^ a = veblen a.invVeblen₁ a
Tactic: rw [invVeblen₂_eq_iff, invVeblen₁_of_lt_opow h, veblen_zero_apply]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a : Ordinal.{u}
h : a < ω ^ a
rw : ω ^ a = veblen a.invVeblen₁ a
⊢ a.invVeblen₂ = a
have rw₁ : ω ^ a = veblen 0 a
Tactic: rw [invVeblen₂_eq_iff, invVeblen₁_of_lt_opow h, veblen_zero_apply]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
a : Ordinal.{u}
h : a < ω ^ a
rw : ω ^ a = veblen a.invVeblen₁ a
rw₁ : ω ^ a = veblen 0 a
⊢ a.invVeblen₂ = a
have rw₂ : ω ^ a = ω ^ a
Tactic: rw [invVeblen₂_eq_iff, invVeblen₁_of_lt_opow h, veblen_zero_apply]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
⊢ invVeblen₂ 0 = 0
have h : 0 < HPow.hPow (β := Ordinal.{u_1}) ω 0
Tactic: apply invVeblen₂_of_lt_opow
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ (veblen o a).invVeblen₂ = a
have h₁ : 0 < o
Tactic: rw [invVeblen₂_eq_iff, invVeblen₁_veblen h, ← veblen_zero_apply, veblen_veblen_of_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a x : Ordinal.{u}
h : a < veblen o a
⊢ veblen o a = ω ^ x ↔ x.invVeblen₁ = o ∧ x.invVeblen₂ = a
have refine_1 : veblen o a = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
Tactic: refine ⟨?_, fun ⟨hx, ha⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a x : Ordinal.{u}
h : a < veblen o a
refine_1 : veblen o a = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
⊢ veblen o a = ω ^ x ↔ x.invVeblen₁ = o ∧ x.invVeblen₂ = a
have refine_2 : x.invVeblen₁ = o ∧ x.invVeblen₂ = a → ∀ (hx : x.invVeblen₁ = o) (ha : x.invVeblen₂ = a), veblen o a = ω ^ x
Tactic: refine ⟨?_, fun ⟨hx, ha⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a x : Ordinal.{u}
h : a < veblen o a
⊢ veblen o a = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
have refine_1 : ∀ (h : a < veblen 0 a), veblen 0 a = ω ^ x → x.invVeblen₁ = 0 ∧ x.invVeblen₂ = a
Tactic: obtain rfl | ho := eq_zero_or_pos o
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a x : Ordinal.{u}
h : a < veblen o a
refine_1 : ∀ (h : a < veblen 0 a), veblen 0 a = ω ^ x → x.invVeblen₁ = 0 ∧ x.invVeblen₂ = a
⊢ veblen o a = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
have refine_1₁ : ∀ (ho : 0 < o), veblen o a = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
Tactic: obtain rfl | ho := eq_zero_or_pos o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (hypothesis)
Goal:
a x : Ordinal.{u}
h : a < veblen 0 a
⊢ veblen 0 a = ω ^ x → x.invVeblen₁ = 0 ∧ x.invVeblen₂ = a
have h₁ : a < (fun (a : Ordinal.{u}) ↦ ω ^ a) a
Tactic: rw [veblen_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (hypothesis)
Goal:
a x : Ordinal.{u}
h : a < (fun (a : Ordinal.{u}) ↦ ω ^ a) a
⊢ veblen 0 a = ω ^ x → x.invVeblen₁ = 0 ∧ x.invVeblen₂ = a
have this : a.invVeblen₁ = 0
Tactic: have := invVeblen₁_of_lt_opow h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (hypothesis)
Goal:
a x : Ordinal.{u}
h : a < (fun (a : Ordinal.{u}) ↦ ω ^ a) a
this : a.invVeblen₁ = 0
⊢ veblen 0 a = ω ^ x → x.invVeblen₁ = 0 ∧ x.invVeblen₂ = a
have this₁ : a.invVeblen₂ = a
Tactic: have := invVeblen₂_of_lt_opow h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o a x : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ veblen o a = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
have refine_1 : veblen o a = x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
Tactic: rw [← veblen_veblen_of_lt ho, veblen_zero_apply, opow_right_inj one_lt_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
⊢ ε_ 0 = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0
have rw : deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0 = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0
Tactic: rw [epsilon_eq_deriv, deriv_zero_right]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
rw : deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0 = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0
⊢ ε_ 0 = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0
have rw₁ : nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0 = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0
Tactic: rw [epsilon_eq_deriv, deriv_zero_right]