-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem IsNormal.veblenWith_zero (hp : 0 < f 0) : IsNormal (veblenWith f · 0)

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ veblenWith f o 0 ≤ a

Tactic:
rw [veblenWith_of_ne_zero f ho.pos.ne', derivFamily_zero]

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ nfpFamily (fun x => veblenWith f ↑x) 0 ≤ a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Set.Iio o)
⊢ List.foldr (fun x => veblenWith f ↑x) 0 l ≤ a

Tactic:
suffices ∃ b < o, List.foldr _ 0 l ≤ veblenWith f b 0 by
  obtain ⟨b, hb, hb'⟩ := this
  exact hb'.trans (IH b hb)

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Set.Iio o)
⊢ ∃ b < o, List.foldr (fun x => veblenWith f ↑x) 0 l ≤ veblenWith f b 0

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Set.Iio o)
this : ∃ b < o, List.foldr (?m.12381 b) 0 l ≤ veblenWith f b 0
⊢ List.foldr (fun x => veblenWith f ↑x) 0 l ≤ a

Tactic:
obtain ⟨b, hb, hb'⟩ := this

Result:
case intro.intro
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Set.Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (?m.12381 b) 0 l ≤ veblenWith f b 0
⊢ List.foldr (fun x => veblenWith f ↑x) 0 l ≤ a

Proof state:
case cons.intro.intro.h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Set.Iio o)
l : List ↑(Set.Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x => veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ↑a ≤ ↑a ⊔ b

Tactic:
exact le_max_left _ b

Result:
no goals

Proof state:
case cons.intro.intro.h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Set.Iio o)
l : List ↑(Set.Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x => veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ↑a < Order.succ (↑a ⊔ b)

Tactic:
rw [Order.lt_succ_iff]

Result:
case cons.intro.intro.h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Set.Iio o)
l : List ↑(Set.Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x => veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ↑a ≤ ↑a ⊔ b

Proof state:
case cons.intro.intro
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Set.Iio o)
l : List ↑(Set.Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x => veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ∃ b < o, List.foldr (fun x => veblenWith f ↑x) 0 (a :: l) ≤ veblenWith f 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 (Order.le_succ _)).trans ?_⟩

Result:
case cons.intro.intro
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Set.Iio o)
l : List ↑(Set.Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x => veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ veblenWith f (↑a) ((fun x => veblenWith f x 0) (Order.succ (↑a ⊔ b))) ≤ veblenWith f (Order.succ (↑a ⊔ b)) 0

Proof state:
case intro.intro
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Set.Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (?m.12381 b) 0 l ≤ veblenWith f b 0
⊢ List.foldr (fun x => veblenWith f ↑x) 0 l ≤ a

Tactic:
exact hb'.trans (IH b hb)

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Set.Iio o)
⊢ ∃ b < o, List.foldr (fun x => veblenWith f ↑x) 0 l ≤ veblenWith f b 0

Tactic:
induction l with
| nil => use 0; simp [ho.pos]
| 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 (Order.le_succ _)).trans ?_⟩
  rw [veblenWith_veblenWith_of_lt hf]
  rw [Order.lt_succ_iff]
  exact le_max_left _ b

Result:
no goals

Proof state:
case cons.intro.intro
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Set.Iio o)
l : List ↑(Set.Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x => veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ veblenWith f (↑a) ((fun x => veblenWith f x 0) (Order.succ (↑a ⊔ b))) ≤ veblenWith f (Order.succ (↑a ⊔ b)) 0

Tactic:
rw [veblenWith_veblenWith_of_lt hf]

Result:
case cons.intro.intro.h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Set.Iio o)
l : List ↑(Set.Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x => veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ↑a < Order.succ (↑a ⊔ b)

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ IsNormal fun x => veblenWith f x 0

Tactic:
rw [isNormal_iff_strictMono_limit]

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ (StrictMono fun x => veblenWith f x 0) ∧
    ∀ (o : Ordinal.{u}), o.IsLimit → ∀ (a : Ordinal.{u}), (∀ b < o, veblenWith f b 0 ≤ a) → veblenWith f o 0 ≤ a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ (StrictMono fun x => veblenWith f x 0) ∧
    ∀ (o : Ordinal.{u}), o.IsLimit → ∀ (a : Ordinal.{u}), (∀ b < o, veblenWith f b 0 ≤ a) → veblenWith f o 0 ≤ a

Tactic:
refine ⟨veblenWith_zero_strictMono hf hp, fun o ho a IH ↦ ?_⟩

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ veblenWith f o 0 ≤ a

Proof state:
case cons
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a✝ : Ordinal.{u}
IH✝ : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Set.Iio o)
l : List ↑(Set.Iio o)
IH : ∃ b < o, List.foldr (fun x => veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ∃ b < o, List.foldr (fun x => veblenWith f ↑x) 0 (a :: l) ≤ veblenWith f b 0

Tactic:
obtain ⟨b, hb, hb'⟩ := IH

Result:
case cons.intro.intro
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Set.Iio o)
l : List ↑(Set.Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x => veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ∃ b < o, List.foldr (fun x => veblenWith f ↑x) 0 (a :: l) ≤ veblenWith f b 0

Proof state:
case h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ 0 < o ∧ List.foldr (fun x => veblenWith f ↑x) 0 [] ≤ veblenWith f 0 0

Tactic:
simp [ho.pos]

Result:
no goals