awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ veblenWith f 0 = f
have rw : (if Eq.{u_1 + 2} (α := Ordinal.{u_1}) 0 0 then f
  else
    derivFamily fun (x : { x : Ordinal.{u_1} // Membership.mem (γ := Set Ordinal.{u_1}) (Iio 0) x }) ↦
      match (motive :=
        { x : Ordinal.{u_1} // Membership.mem (γ := Set Ordinal.{u_1}) (Iio 0) x } → Ordinal.{u_1} → Ordinal.{u_1})
        x with
      | ⟨x, property⟩ => veblenWith f x) =
  f
Tactic: rw [veblenWith, if_pos rfl]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
rw :
  (if Eq.{u_1 + 2} (α := Ordinal.{u_1}) 0 0 then f
    else
      derivFamily fun (x : { x : Ordinal.{u_1} // Membership.mem (γ := Set Ordinal.{u_1}) (Iio 0) x }) ↦
        match (motive :=
          { x : Ordinal.{u_1} // Membership.mem (γ := Set Ordinal.{u_1}) (Iio 0) x } → Ordinal.{u_1} → Ordinal.{u_1})
          x with
        | ⟨x, property⟩ => veblenWith f x) =
    f
⊢ veblenWith f 0 = f
have rw₁ : f = f
Tactic: rw [veblenWith, if_pos rfl]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ veblenWith f o = derivFamily fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})
have rw : (if o = 0 then f
  else
    derivFamily fun (x : { x : Ordinal.{u} // x ∈ Iio o }) ↦
      match (motive := { x : Ordinal.{u} // x ∈ Iio o } → Ordinal.{u} → Ordinal.{u}) x with
      | ⟨x, property⟩ => veblenWith f x) =
  derivFamily fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})
Tactic: rw [veblenWith, if_neg h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
rw :
  (if o = 0 then f
    else
      derivFamily fun (x : { x : Ordinal.{u} // x ∈ Iio o }) ↦
        match (motive := { x : Ordinal.{u} // x ∈ Iio o } → Ordinal.{u} → Ordinal.{u}) x with
        | ⟨x, property⟩ => veblenWith f x) =
    derivFamily fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})
⊢ veblenWith f o = derivFamily fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})
have rw₁ : (derivFamily fun (x : { x : Ordinal.{u} // x ∈ Iio o }) ↦
    match (motive := { x : Ordinal.{u} // x ∈ Iio o } → Ordinal.{u} → Ordinal.{u}) x with
    | ⟨x, property⟩ => veblenWith f x) =
  derivFamily fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})
Tactic: rw [veblenWith, if_neg h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (veblenWith f o)
have rw : IsNormal (derivFamily fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u}))
Tactic: rw [veblenWith_of_ne_zero f h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ IsNormal (veblenWith f o)
have inl : IsNormal (veblenWith f 0)
Tactic: obtain rfl | h := eq_or_ne o 0
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
inl : IsNormal (veblenWith f 0)
⊢ IsNormal (veblenWith f o)
have inr : ∀ (h : o ≠ 0), IsNormal (veblenWith f o)
Tactic: obtain rfl | h := eq_or_ne o 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
⊢ a ∈ range (veblenWith f o) ↔ ∀ b < o, veblenWith f b a = a
have rw : (∀ (i : (↑(Iio o) : Type (u + 1))), veblenWith f (↑i : Ordinal.{u}) a = a) ↔ ∀ b < o, veblenWith f b a = a
Tactic: rw [veblenWith_of_ne_zero f h, mem_range_derivFamily (fun _ ↦ isNormal_veblenWith hf _)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
a : Ordinal.{u}
⊢ veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a
have apply : veblenWith f o₂ a ∈ range (veblenWith f o₂)
Tactic: apply (mem_range_veblenWith hf h.ne_bot).1 _ _ h
-- 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₂
h' : veblenWith f o₂ a = a
⊢ veblenWith f o₁ a = a
have inl : ∀ (h : o₁ ≤ o₁) (h' : veblenWith f o₁ a = a), veblenWith f o₁ a = a
Tactic: obtain rfl | h := h.eq_or_lt
Cleared hypotheses: o₂, h, h'
-- 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₂
h' : veblenWith f o₂ a = a
inl : ∀ (h : o₁ ≤ o₁) (h' : veblenWith f o₁ a = a), veblenWith f o₁ a = a
⊢ veblenWith f o₁ a = a
have inr : ∀ (h : o₁ < o₂), veblenWith f o₁ a = a
Tactic: obtain rfl | h := h.eq_or_lt
-- 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_1 : o₁ ≤ o₂
h' : veblenWith f o₂ a = a
h : o₁ < o₂
⊢ veblenWith f o₁ a = a
have inr : veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a
Tactic: rw [← h', 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 : Ordinal.{u}
hf : IsNormal f
h_1 : o₁ ≤ o₂
h' : veblenWith f o₂ a = a
h : o₁ < o₂
inr : veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a
⊢ veblenWith f o₁ a = a
have inr₁ : veblenWith f o₂ a = veblenWith f o₂ a
Tactic: rw [← h', veblenWith_veblenWith_of_lt hf h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o a ∈ range f
have inl : veblenWith f 0 a ∈ range f
Tactic: obtain rfl | h := eq_zero_or_pos o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
inl : veblenWith f 0 a ∈ range f
⊢ veblenWith f o a ∈ range f
have inr : ∀ (h : 0 < o), veblenWith f o a ∈ range f
Tactic: obtain rfl | h := eq_zero_or_pos o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : 0 < o
⊢ veblenWith f o a ∈ range f
have inr : veblenWith f 0 (veblenWith f o a) ∈ range f
Tactic: rw [← veblenWith_veblenWith_of_lt hf h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ veblenWith f (o + 1) = deriv (veblenWith f o)
have rw : enumOrd (⋂ (i : (↑(Iio (o + 1)) : Type (u + 1))), Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))) =
  enumOrd (Function.fixedPoints (veblenWith f o))
Tactic: rw [deriv_eq_enumOrd (isNormal_veblenWith hf o),
    veblenWith_of_ne_zero f (add_pos_of_right zero_lt_one _).ne', derivFamily_eq_enumOrd]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
rw :
  enumOrd (⋂ (i : (↑(Iio (o + 1)) : Type (u + 1))), Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))) =
    enumOrd (Function.fixedPoints (veblenWith f o))
⊢ veblenWith f (o + 1) = deriv (veblenWith f o)
have rw₁ : ∀ (i : (↑(Iio (o + 1)) : Type (u + 1))), IsNormal (veblenWith f (↑i : Ordinal.{u}))
Tactic: rw [deriv_eq_enumOrd (isNormal_veblenWith hf o),
    veblenWith_of_ne_zero f (add_pos_of_right zero_lt_one _).ne', derivFamily_eq_enumOrd]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ enumOrd (⋂ (i : (↑(Iio (o + 1)) : Type (u + 1))), Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))) =
    enumOrd (Function.fixedPoints (veblenWith f o))
have h : ⋂ (i : (↑(Iio (o + 1)) : Type (u + 1))), Function.fixedPoints (veblenWith f (↑i : Ordinal.{u})) =
  Function.fixedPoints (veblenWith f o)
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ ⋂ (i : (↑(Iio (o + 1)) : Type (u + 1))), Function.fixedPoints (veblenWith f (↑i : Ordinal.{u})) =
    Function.fixedPoints (veblenWith f o)
have h : ∀ (a : Ordinal.{u}),
  Membership.mem (γ := Set Ordinal.{u})
      (⋂ (i : (↑(Iio (o + 1)) : Type (u + 1))), Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))) a ↔
    a ∈ Function.fixedPoints (veblenWith f o)
Tactic: ext a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
⊢ Membership.mem (γ := Set Ordinal.{u})
      (⋂ (i : (↑(Iio (o + 1)) : Type (u + 1))), Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))) a ↔
    a ∈ Function.fixedPoints (veblenWith f o)
have h : (∀ (i : (↑(Iio (o + 1)) : Type (u + 1))), a ∈ Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))) ↔
  a ∈ Function.fixedPoints (veblenWith f o)
Tactic: rw [mem_iInter]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
⊢ (∀ (i : (↑(Iio (o + 1)) : Type (u + 1))), a ∈ Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))) ↔
    a ∈ Function.fixedPoints (veblenWith f o)
have mpr : a ∈ Function.fixedPoints (veblenWith f o) →
  ∀ (i : (↑(Iio (o + 1)) : Type (u + 1))), a ∈ Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))
Tactic: use fun ha ↦ ha ⟨o, lt_succ o⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb : b < o + 1
⊢ a ∈
    Function.fixedPoints
      (veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (o + 1)) b hb) : Ordinal.{u}))
have mpr : ∀ (ha : veblenWith f b a = a) (hb : b < b + 1),
  a ∈
    Function.fixedPoints
      (veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (b + 1)) b hb) : Ordinal.{u}))
Tactic: obtain rfl | hb := lt_succ_iff_eq_or_lt.1 hb
Cleared hypotheses: o, ha, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb : b < o + 1
mpr :
  ∀ (ha : veblenWith f b a = a) (hb : b < b + 1),
    a ∈
      Function.fixedPoints
        (veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (b + 1)) b hb) : Ordinal.{u}))
⊢ a ∈
    Function.fixedPoints
      (veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (o + 1)) b hb) : Ordinal.{u}))
have mpr₁ : ∀ (hb_1 : b < o),
  a ∈
    Function.fixedPoints
      (veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (o + 1)) b hb) : Ordinal.{u}))
Tactic: obtain rfl | hb := lt_succ_iff_eq_or_lt.1 hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a b : Ordinal.{u}
ha : veblenWith f b a = a
hb : b < b + 1
⊢ a ∈
    Function.fixedPoints
      (veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (b + 1)) b hb) : Ordinal.{u}))
have mpr : veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (b + 1)) b hb) : Ordinal.{u}) a = a
Tactic: rw [Function.mem_fixedPoints_iff, ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a b : Ordinal.{u}
ha : veblenWith f b a = a
hb : b < b + 1
mpr : veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (b + 1)) b hb) : Ordinal.{u}) a = a
⊢ a ∈
    Function.fixedPoints
      (veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (b + 1)) b hb) : Ordinal.{u}))
have mpr₁ : a = a
Tactic: rw [Function.mem_fixedPoints_iff, ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb_1 : b < o + 1
hb : b < o
⊢ a ∈
    Function.fixedPoints
      (veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (o + 1)) b hb_1) : Ordinal.{u}))
have mpr : veblenWith f o a ∈
  Function.fixedPoints
    (veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (o + 1)) b hb_1) : Ordinal.{u}))
Tactic: rw [← ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a : Ordinal.{u}
⊢ Monotone (β := Ordinal.{u}) fun (x : Ordinal.{u}) ↦ veblenWith f x a
have rw : ∀ ⦃a_1 b : Ordinal.{u}⦄, a_1 < b → veblenWith f a_1 a ≤ veblenWith f b a
Tactic: rw [monotone_iff_forall_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ a ≤ veblenWith f o₂ a
have rw : veblenWith f o₁ a ≤ veblenWith f o₁ (veblenWith f o₂ a)
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 a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
b : Ordinal.{u}
⊢ 0 < veblenWith f 0 b
have rw : 0 < f b
Tactic: rw [veblenWith_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (hypothesis)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ 0 < veblenWith f o a
have H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
Tactic: have H (b) : 0 < veblenWith f 0 b := by
    rw [veblenWith_zero]
    exact hp.trans_le (hf.monotone zero_le)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
⊢ 0 < veblenWith f o a
have inl : 0 < veblenWith f 0 a
Tactic: obtain rfl | h := eq_zero_or_pos o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
inl : 0 < veblenWith f 0 a
⊢ 0 < veblenWith f o a
have inr : ∀ (h : 0 < o), 0 < veblenWith f o a
Tactic: obtain rfl | h := eq_zero_or_pos o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f o a
have inr : 0 < veblenWith f 0 (veblenWith f o a)
Tactic: rw [← veblenWith_veblenWith_of_lt hf h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ 0 < veblenWith f o₂ 0
have rw : 0 < veblenWith f o₂ 0
Tactic: rw [← veblenWith_veblenWith_of_lt hf h, veblenWith_lt_veblenWith_iff_right hf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ IsNormal (β := Ordinal.{u}) fun (x : Ordinal.{u}) ↦ veblenWith f x 0
have rw : (StrictMono (β := Ordinal.{u}) fun (x : Ordinal.{u}) ↦ veblenWith f x 0) ∧
  ∀ (o : Ordinal.{u}), IsSuccLimit o → ∀ (a : Ordinal.{u}), (∀ b < o, veblenWith f b 0 ≤ a) → veblenWith f o 0 ≤ a
Tactic: rw [isNormal_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ (StrictMono (β := Ordinal.{u}) fun (x : Ordinal.{u}) ↦ veblenWith f x 0) ∧
    ∀ (o : Ordinal.{u}), IsSuccLimit o → ∀ (a : Ordinal.{u}), (∀ b < o, veblenWith f b 0 ≤ a) → veblenWith f o 0 ≤ a
have refine : ∀ (o : Ordinal.{u}) (ho : IsSuccLimit o) (a : Ordinal.{u}) (IH : ∀ b < o, veblenWith f b 0 ≤ a), veblenWith f o 0 ≤ a
Tactic: refine ⟨veblenWith_zero_strictMono hf hp, fun o ho a IH ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ veblenWith f o 0 ≤ a
have rw : nfpFamily (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 ≤ a
Tactic: rw [veblenWith_of_ne_zero f ho.ne_bot, derivFamily_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ nfpFamily (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 ≤ a
have apply : ∀ (l : List (↑(Iio o) : Type (u + 1))),
  List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ a
Tactic: apply nfpFamily_le fun l ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List (↑(Iio o) : Type (u + 1))
this :
  ∃ b < o, List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ veblenWith f b 0
⊢ List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ a
have obtain : ∀ (b : Ordinal.{u}) (hb : b < o)
  (hb' : List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ veblenWith f b 0),
  List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ a
Tactic: obtain ⟨b, hb, hb'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List (↑(Iio o) : Type (u + 1))
⊢ List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ a
have suffices : ∃ b < o, List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ veblenWith f b 0
Tactic: suffices ∃ b < o, List.foldr _ 0 l ≤ veblenWith f b 0 by
    obtain ⟨b, hb, hb'⟩ := this
    exact hb'.trans (IH b hb)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ ∃ b < o, List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 [] ≤ veblenWith f b 0
have h : 0 < o ∧ List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 [] ≤ veblenWith f 0 0
Tactic: use 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a_1 : Ordinal.{u}
IH_1 : ∀ b < o, veblenWith f b 0 ≤ a_1
a : (↑(Iio o) : Type (u + 1))
l : List (↑(Iio o) : Type (u + 1))
IH : ∃ b < o, List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ veblenWith f b 0
⊢ ∃ b < o,
    List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 (a :: l) ≤ veblenWith f b 0
have cons : ∀ (b : Ordinal.{u}) (hb : b < o)
  (hb' : List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ veblenWith f b 0),
  ∃ b < o,
    List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 (a :: l) ≤ veblenWith f b 0
Tactic: obtain ⟨b, hb, hb'⟩ := IH
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a_1 : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a_1
a : (↑(Iio o) : Type (u + 1))
l : List (↑(Iio o) : Type (u + 1))
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ veblenWith f b 0
⊢ ∃ b < o,
    List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 (a :: l) ≤ veblenWith f b 0
have cons : veblenWith f (↑a : Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ veblenWith f x 0) (succ (max (↑a : Ordinal.{u}) b))) ≤
  veblenWith f (succ (max (↑a : Ordinal.{u}) b)) 0
Tactic: refine ⟨_, ho.succ_lt (max_lt a.2 hb), ((veblenWith_right_strictMono hf _).monotone <|
      hb'.trans <| veblenWith_left_monotone hf _ <|
        (le_max_right a.1 b).trans (le_succ _)).trans ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a_1 : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a_1
a : (↑(Iio o) : Type (u + 1))
l : List (↑(Iio o) : Type (u + 1))
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ veblenWith f b 0
⊢ veblenWith f (↑a : Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ veblenWith f x 0) (succ (max (↑a : Ordinal.{u}) b))) ≤
    veblenWith f (succ (max (↑a : Ordinal.{u}) b)) 0
have cons : (↑a : Ordinal.{u}) < succ (max (↑a : Ordinal.{u}) b)
Tactic: rw [veblenWith_veblenWith_of_lt hf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a_1 : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a_1
a : (↑(Iio o) : Type (u + 1))
l : List (↑(Iio o) : Type (u + 1))
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ veblenWith f b 0
⊢ (↑a : Ordinal.{u}) < succ (max (↑a : Ordinal.{u}) b)
have cons : (↑a : Ordinal.{u}) ≤ max (↑a : Ordinal.{u}) b
Tactic: rw [lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List (↑(Iio o) : Type (u + 1))
⊢ ∃ b < o, List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ veblenWith f b 0
have nil : ∃ b < o, List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 [] ≤ veblenWith f b 0
Tactic: induction l with
  | nil => use 0; simpa using ho.bot_lt
  | cons a l IH =>
    obtain ⟨b, hb, hb'⟩ := IH
    refine ⟨_, ho.succ_lt (max_lt a.2 hb), ((veblenWith_right_strictMono hf _).monotone <|
      hb'.trans <| veblenWith_left_monotone hf _ <|
        (le_max_right a.1 b).trans (le_succ _)).trans ?_⟩
    rw [veblenWith_veblenWith_of_lt hf]
    rw [lt_succ_iff]
    exact le_max_left _ b
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Veblen (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List (↑(Iio o) : Type (u + 1))
nil :
  ∃ b < o, List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 [] ≤ veblenWith f b 0
⊢ ∃ b < o, List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ veblenWith f b 0
have cons : ∀ (a : (↑(Iio o) : Type (u + 1))) (l : List (↑(Iio o) : Type (u + 1)))
  (IH :
    ∃ b < o, List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ veblenWith f b 0),
  ∃ b < o,
    List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 (a :: l) ≤ veblenWith f b 0
Tactic: induction l with
  | nil => use 0; simpa using ho.bot_lt
  | cons a l IH =>
    obtain ⟨b, hb, hb'⟩ := IH
    refine ⟨_, ho.succ_lt (max_lt a.2 hb), ((veblenWith_right_strictMono hf _).monotone <|
      hb'.trans <| veblenWith_left_monotone hf _ <|
        (le_max_right a.1 b).trans (le_succ _)).trans ?_⟩
    rw [veblenWith_veblenWith_of_lt hf]
    rw [lt_succ_iff]
    exact le_max_left _ b
Cleared hypotheses: l
-- 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₁
⊢ 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]