awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o a = veblenWith f o b ↔ a = b

Tactic:
(veblenWith_injective hf o).eq_iff

Premises used: Function.Injective.eq_iff, Ordinal.veblenWith_injective
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
⊢ a ≤ veblenWith f o a

Tactic:
(veblenWith_right_strictMono hf o).le_apply

Premises used: StrictMono.le_apply, Ordinal.veblenWith_right_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a : Ordinal.{u}
rw : ∀ ⦃a_1 b : Ordinal.{u}⦄, a_1 < b → veblenWith f a_1 a ≤ veblenWith f b a
⊢ Monotone (β := Ordinal.{u}) fun (x : Ordinal.{u}) ↦ veblenWith f x a

Tactic:
rw [monotone_iff_forall_lt]

Premises used: monotone_iff_forall_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
rw : veblenWith f o₁ a ≤ veblenWith f o₁ (veblenWith f o₂ a)
⊢ veblenWith f o₁ a ≤ veblenWith f o₂ a

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h]

Premises used: Ordinal.veblenWith_veblenWith_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ a ≤ veblenWith f o₁ (veblenWith f o₂ a)

Tactic:
(veblenWith_right_strictMono hf o₁).monotone (right_le_veblenWith hf o₂ a)

Premises used: StrictMono.monotone, Ordinal.veblenWith_right_strictMono, Ordinal.right_le_veblenWith
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ a ≤ veblenWith f o₁ (veblenWith f o₂ a)

Tactic:
exact (veblenWith_right_strictMono hf o₁).monotone (right_le_veblenWith hf o₂ a)

Premises used: StrictMono.monotone, Ordinal.veblenWith_right_strictMono, Ordinal.right_le_veblenWith
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
b : Ordinal.{u}
rw : 0 < f b
⊢ 0 < veblenWith f 0 b

Tactic:
rw [veblenWith_zero]

Premises used: Ordinal.veblenWith_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
b : Ordinal.{u}
⊢ 0 < f b

Tactic:
hp.trans_le (hf.monotone zero_le)

Premises used: zero_le, Order.IsNormal.monotone, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
b : Ordinal.{u}
⊢ 0 < f b

Tactic:
exact hp.trans_le (hf.monotone zero_le)

Premises used: zero_le, Order.IsNormal.monotone, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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

Tactic:
have H (b) : 0 < veblenWith f 0 b := by
    rw [veblenWith_zero]
    exact hp.trans_le (hf.monotone zero_le)
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
inr : ∀ (h : 0 < o), 0 < veblenWith f o a
⊢ 0 < veblenWith f o a

Tactic:
obtain rfl | h := eq_zero_or_pos o

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
⊢ 0 < veblenWith f 0 a

Tactic:
H a
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
⊢ 0 < veblenWith f 0 a

Tactic:
exact H a
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
inr : 0 < veblenWith f 0 (veblenWith f o a)
⊢ 0 < veblenWith f o a

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h]

Premises used: Ordinal.veblenWith_veblenWith_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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 0 (veblenWith f o a)

Tactic:
H _
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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 0 (veblenWith f o a)

Tactic:
exact H _
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
rw : 0 < veblenWith f o₂ 0
⊢ veblenWith f o₁ 0 < veblenWith f o₂ 0

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h, veblenWith_lt_veblenWith_iff_right hf]

Premises used: Ordinal.veblenWith_veblenWith_of_lt, Ordinal.veblenWith_lt_veblenWith_iff_right
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ 0 < veblenWith f o₂ 0

Tactic:
veblenWith_pos hf hp

Premises used: Ordinal.veblenWith_pos
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ 0 < veblenWith f o₂ 0

Tactic:
exact veblenWith_pos hf hp

Premises used: Ordinal.veblenWith_pos
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ veblenWith f o₁ 0 < veblenWith f o₂ 0 ↔ o₁ < o₂

Tactic:
(veblenWith_zero_strictMono hf hp).lt_iff_lt

Premises used: Ordinal.veblenWith_zero_strictMono, StrictMono.lt_iff_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ veblenWith f o₁ 0 ≤ veblenWith f o₂ 0 ↔ o₁ ≤ o₂

Tactic:
(veblenWith_zero_strictMono hf hp).le_iff_le

Premises used: Ordinal.veblenWith_zero_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ veblenWith f o₁ 0 = veblenWith f o₂ 0 ↔ o₁ = o₂

Tactic:
(veblenWith_zero_strictMono hf hp).injective.eq_iff

Premises used: Ordinal.veblenWith_zero_strictMono, Function.Injective.eq_iff, StrictMono.injective
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o a : Ordinal.{u}
⊢ o ≤ veblenWith f o a

Tactic:
(veblenWith_zero_strictMono hf hp).le_apply.trans <|
    (veblenWith_right_strictMono hf _).monotone zero_le

Premises used: StrictMono.le_apply, zero_le, StrictMono.monotone, Ordinal.veblenWith_right_strictMono, Ordinal.veblenWith_zero_strictMono, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
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
⊢ IsNormal (β := Ordinal.{u}) fun (x : Ordinal.{u}) ↦ veblenWith f x 0

Tactic:
rw [isNormal_iff]

Premises used: Order.isNormal_iff
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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

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

Premises used: Ordinal.veblenWith_zero_strictMono, And.intro
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
refine :
  ∀ (o : Ordinal.{u}) (ho : IsSuccLimit o) (a : Ordinal.{u}) (IH : ∀ b < o, veblenWith f b 0 ≤ a), veblenWith f o 0 ≤ a
⊢ (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:
refine ⟨veblenWith_zero_strictMono hf hp, fun o ho a IH ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
rw : nfpFamily (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 ≤ a
⊢ veblenWith f o 0 ≤ a

Tactic:
rw [veblenWith_of_ne_zero f ho.ne_bot, derivFamily_zero]

Premises used: Order.IsSuccLimit.ne_bot, Ordinal.derivFamily_zero, Ordinal.veblenWith_of_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
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
⊢ nfpFamily (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 ≤ a

Tactic:
apply nfpFamily_le fun l ↦ ?_

Premises used: Ordinal.nfpFamily_le
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
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
⊢ List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 l ≤ a

Tactic:
obtain ⟨b, hb, hb'⟩ := this
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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 : 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:
hb'.trans (IH b hb)

Premises used: LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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 : 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:
exact hb'.trans (IH b hb)

Premises used: LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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))
suffices :
  ∃ 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

Tactic:
suffices ∃ b < o, List.foldr _ 0 l ≤ veblenWith f b 0 by
    obtain ⟨b, hb, hb'⟩ := this
    exact hb'.trans (IH b hb)
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
h : 0 < o ∧ List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 [] ≤ veblenWith f 0 0
⊢ ∃ b < o, List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 [] ≤ veblenWith f b 0

Tactic:
use 0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
⊢ 0 < o ∧ List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 [] ≤ veblenWith f 0 0

Tactic:
simpa using ho.bot_lt

Premises used: Order.IsSuccLimit.bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
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
⊢ ∃ 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
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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

Tactic:
⟨_, 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 ?_⟩

Premises used: le_max_right, StrictMono.monotone, Ordinal.veblenWith_right_strictMono, Order.IsSuccLimit.succ_lt, max_lt, And.intro, Exists.intro, Order.le_succ, LE.le.trans, Subtype.val, Subtype.property, Ordinal.veblenWith_left_monotone
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
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
⊢ ∃ b < o,
    List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 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 (le_succ _)).trans ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
cons : (↑a : Ordinal.{u}) < succ (max (↑a : Ordinal.{u}) b)
⊢ 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:
rw [veblenWith_veblenWith_of_lt hf]

Premises used: Ordinal.veblenWith_veblenWith_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
cons : (↑a : Ordinal.{u}) ≤ max (↑a : Ordinal.{u}) b
⊢ (↑a : Ordinal.{u}) < succ (max (↑a : Ordinal.{u}) b)

Tactic:
rw [lt_succ_iff]

Premises used: Order.lt_succ_iff
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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}) ≤ max (↑a : Ordinal.{u}) b

Tactic:
le_max_left _ b

Premises used: le_max_left
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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}) ≤ max (↑a : Ordinal.{u}) b

Tactic:
exact le_max_left _ b

Premises used: le_max_left
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
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
⊢ ∃ b < o, List.foldr (fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})) 0 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

Premises used: Ordinal.veblenWith_veblenWith_of_lt, Order.lt_succ_iff, Order.IsSuccLimit.bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h : o₂ ≤ o₁
⊢ veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a ↔ veblenWith f o₁ a = a

Tactic:
grind [veblenWith_inj, → veblenWith_eq_self_of_le]

Premises used: Ordinal.veblenWith_inj, Ordinal.veblenWith_eq_self_of_le
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
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

Tactic:
simp_rw [(right_le_veblenWith hf ..).lt_iff_ne', ne_eq,
    veblenWith_veblenWith_eq_veblenWith_iff hf h]

Premises used: Ordinal.veblenWith_veblenWith_eq_veblenWith_iff, ne_eq, LE.le.lt_iff_ne', Ordinal.right_le_veblenWith
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o (f a) = f a ↔ veblenWith f o a = a

Tactic:
simpa using veblenWith_veblenWith_eq_veblenWith_iff hf zero_le

Premises used: zero_le, Ordinal.veblenWith_veblenWith_eq_veblenWith_iff
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ f a < veblenWith f o (f a) ↔ a < veblenWith f o a

Tactic:
simpa using veblenWith_lt_veblenWith_veblenWith_iff hf zero_le

Premises used: zero_le, Ordinal.veblenWith_lt_veblenWith_veblenWith_iff
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
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
⊢ 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₂

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
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

Tactic:
simp [(veblenWith_right_strictMono hf _).cmp_map_eq]

Premises used: Ordinal.veblenWith_right_strictMono, StrictMono.cmp_map_eq
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
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

Tactic:
on_goal 2 => simp [(veblenWith_right_strictMono hf _).cmp_map_eq]

Premises used: Ordinal.veblenWith_right_strictMono, StrictMono.cmp_map_eq
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
rw : cmp (veblenWith f o₁ a) (veblenWith f o₁ (veblenWith f o₂ b))
| cmp (veblenWith f o₁ a) (veblenWith f o₂ b)

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h]

Premises used: Ordinal.veblenWith_veblenWith_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
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
⊢ 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:
conv_lhs => rw [← veblenWith_veblenWith_of_lt hf h]

Premises used: Ordinal.veblenWith_veblenWith_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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₁ (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:
simp [h.cmp_eq_lt, h.cmp_eq_gt, (veblenWith_right_strictMono hf _).cmp_map_eq]

Premises used: Ordinal.veblenWith_right_strictMono, LT.lt.cmp_eq_gt, LT.lt.cmp_eq_lt, StrictMono.cmp_map_eq