awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂ (veblenWith f o₁ a)) (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₁
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
⊢ 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₂ (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 [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
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
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
⊢ 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

Tactic:
rw [← cmp_eq_lt_iff, cmp_veblenWith hf]

Premises used: Ordinal.cmp_veblenWith, cmp_eq_lt_iff
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (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:
aesop (add simp lt_asymm)

Premises used: lt_asymm
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
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
⊢ 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

Tactic:
rw [← not_lt, ← cmp_eq_gt_iff, cmp_veblenWith hf]

Premises used: not_lt, Ordinal.cmp_veblenWith, cmp_eq_gt_iff
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ ¬(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:
aesop (add simp [not_lt_of_ge, lt_asymm])

Premises used: lt_asymm, not_lt_of_ge
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
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
⊢ 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

Tactic:
rw [← cmp_eq_eq_iff, cmp_veblenWith hf]

Premises used: cmp_eq_eq_iff, Ordinal.cmp_veblenWith
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (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:
aesop (add simp lt_asymm)

Premises used: lt_asymm
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
rw : veblenWith (fun (x : Ordinal.{u_1}) ↦ ω ^ x) 0 = fun (a : Ordinal.{u_1}) ↦ ω ^ a
rw₁ rw₂ :
  Eq.{u_1 + 2} (α := Ordinal.{u_1} → Ordinal.{u_1}) (fun (x : Ordinal.{u_1}) ↦ ω ^ x) fun (a : Ordinal.{u_1}) ↦ ω ^ a
⊢ veblen 0 = fun (a : Ordinal.{u_1}) ↦ ω ^ a

Tactic:
rw [veblen, veblenWith_zero]

Premises used: Ordinal.veblen, Ordinal.veblenWith_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a : Ordinal.{u_1}
rw rw₁ : (fun (a : Ordinal.{u_1}) ↦ ω ^ a) a = ω ^ a
⊢ veblen 0 a = ω ^ a

Tactic:
rw [veblen_zero]

Premises used: Ordinal.veblen_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : o ≠ 0
⊢ veblen o = derivFamily fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblen (↑x : Ordinal.{u})

Tactic:
veblenWith_of_ne_zero _ h

Premises used: Ordinal.veblen, Ordinal.veblenWith_of_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ IsNormal (veblen o)

Tactic:
isNormal_veblenWith (isNormal_opow one_lt_omega0) o

Premises used: Ordinal.veblen, Ordinal.isNormal_veblenWith, Ordinal.isNormal_opow, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
h : o ≠ 0
⊢ a ∈ range (veblen o) ↔ ∀ b < o, veblen b a = a

Tactic:
mem_range_veblenWith (isNormal_opow one_lt_omega0) h

Premises used: Ordinal.veblen, Set.Mem, Ordinal.isNormal_opow, Ordinal.mem_range_veblenWith, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
a : Ordinal.{u}
⊢ veblen o₁ (veblen o₂ a) = veblen o₂ a

Tactic:
veblenWith_veblenWith_of_lt (isNormal_opow one_lt_omega0) h a

Premises used: Ordinal.veblen, Ordinal.veblenWith_veblenWith_of_lt, Ordinal.isNormal_opow, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o₁ o₂ a : Ordinal.{u}
h : o₁ ≤ o₂
h' : veblen o₂ a = a
⊢ veblen o₁ a = a

Tactic:
veblenWith_eq_self_of_le (isNormal_opow one_lt_omega0) h h'

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.veblenWith_eq_self_of_le, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u_1}
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (range fun (x : Ordinal.{u_1}) ↦ ω ^ x) (veblen o a)

Tactic:
veblenWith_mem_range (isNormal_opow one_lt_omega0)

Premises used: Ordinal.veblen, Set.Mem, Ordinal.isNormal_opow, Ordinal.one_lt_omega0, Ordinal.veblenWith_mem_range
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ veblen (o + 1) = deriv (veblen o)

Tactic:
veblenWith_add_one (isNormal_opow one_lt_omega0) o

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.veblenWith_add_one, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ veblen (succ o) = deriv (veblen o)

Tactic:
veblen_add_one o

Premises used: Order.succ, Ordinal.veblen_add_one
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ StrictMono (veblen o)

Tactic:
veblenWith_right_strictMono (isNormal_opow one_lt_omega0) o

Premises used: Ordinal.veblen, Ordinal.veblenWith_right_strictMono, Ordinal.isNormal_opow, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a b : Ordinal.{u}
⊢ veblen o a < veblen o b ↔ a < b

Tactic:
veblenWith_lt_veblenWith_iff_right (isNormal_opow one_lt_omega0)

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.veblenWith_lt_veblenWith_iff_right, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a b : Ordinal.{u}
⊢ veblen o a ≤ veblen o b ↔ a ≤ b

Tactic:
veblenWith_le_veblenWith_iff_right (isNormal_opow one_lt_omega0)

Premises used: Ordinal.veblenWith_le_veblenWith_iff_right, Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ Function.Injective (veblen o)

Tactic:
veblenWith_injective (isNormal_opow one_lt_omega0) o

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.veblenWith_injective, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a b : Ordinal.{u}
⊢ veblen o a = veblen o b ↔ a = b

Tactic:
(veblen_injective o).eq_iff

Premises used: Function.Injective.eq_iff, Ordinal.veblen_injective
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u_1}
⊢ a ≤ veblen o a

Tactic:
right_le_veblenWith (isNormal_opow one_lt_omega0) o a

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.one_lt_omega0, Ordinal.right_le_veblenWith
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ Monotone (β := Ordinal.{u_1}) fun (x : Ordinal.{u_1}) ↦ veblen x o

Tactic:
veblenWith_left_monotone (isNormal_opow one_lt_omega0) o

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.one_lt_omega0, Ordinal.veblenWith_left_monotone
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
⊢ 0 < HPow.hPow (β := Ordinal.{u}) ω 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
⊢ 0 < HPow.hPow (β := Ordinal.{u_1}) ω 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o₁ o₂ : Ordinal.{u}
⊢ veblen o₁ 0 < veblen o₂ 0 ↔ o₁ < o₂

Tactic:
veblen_zero_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Ordinal.veblen_zero_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o₁ o₂ : Ordinal.{u}
⊢ veblen o₁ 0 ≤ veblen o₂ 0 ↔ o₁ ≤ o₂

Tactic:
veblen_zero_strictMono.le_iff_le

Premises used: StrictMono.le_iff_le, Ordinal.veblen_zero_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o₁ o₂ : Ordinal.{u}
⊢ veblen o₁ 0 = veblen o₂ 0 ↔ o₁ = o₂

Tactic:
veblen_zero_strictMono.injective.eq_iff

Premises used: Function.Injective.eq_iff, StrictMono.injective, Ordinal.veblen_zero_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u_1}
⊢ 0 < HPow.hPow (β := Ordinal.{u_1}) ω 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o₁ o₂ a : Ordinal.{u}
h : o₂ ≤ o₁
⊢ veblen o₁ (veblen o₂ a) = veblen o₂ a ↔ veblen o₁ a = a

Tactic:
veblenWith_veblenWith_eq_veblenWith_iff (isNormal_opow one_lt_omega0) h

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.veblenWith_veblenWith_eq_veblenWith_iff, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o₁ o₂ a : Ordinal.{u}
h : o₂ ≤ o₁
⊢ veblen o₂ a < veblen o₁ (veblen o₂ a) ↔ a < veblen o₁ a

Tactic:
veblenWith_lt_veblenWith_veblenWith_iff (isNormal_opow one_lt_omega0) h

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.veblenWith_lt_veblenWith_veblenWith_iff, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
⊢ veblen o (ω ^ a) = ω ^ a ↔ veblen o a = a

Tactic:
veblenWith_apply_eq_apply_iff (isNormal_opow one_lt_omega0)

Premises used: Ordinal.veblen, Ordinal.veblenWith_apply_eq_apply_iff, Ordinal.isNormal_opow, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
⊢ ω ^ a < veblen o (ω ^ a) ↔ a < veblen o a

Tactic:
apply_lt_veblenWith_apply_iff (isNormal_opow one_lt_omega0)

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.one_lt_omega0, Ordinal.apply_lt_veblenWith_apply_iff
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a : Ordinal.{u_1}
inl : 0 < veblen 0 0
inr : ∀ (h : 0 < a), a < veblen a a
⊢ a < veblen a a

Tactic:
obtain rfl | h := eq_zero_or_pos a

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
⊢ 0 < veblen 0 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a : Ordinal.{u_1}
h : 0 < a
inr : veblen a 0 < veblen a a
⊢ a < veblen a a

Tactic:
apply (left_le_veblen a 0).trans_lt

Premises used: Ordinal.left_le_veblen, OfNat.ofNat, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a : Ordinal.{u_1}
h : 0 < a
⊢ veblen a 0 < veblen a a

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o₁ o₂ a b : Ordinal.{u}
⊢ cmp (veblen o₁ a) (veblen o₂ b) =
    match (motive := Ordering → Ordering) cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblen o₂ b)
    | Ordering.gt => cmp (veblen o₁ a) b

Tactic:
cmp_veblenWith (isNormal_opow one_lt_omega0)

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.cmp_veblenWith, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o₁ o₂ a b : Ordinal.{u}
⊢ veblen o₁ a < veblen o₂ b ↔ o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a < b

Tactic:
veblenWith_lt_veblenWith_iff (isNormal_opow one_lt_omega0)

Premises used: Ordinal.veblen, Ordinal.veblenWith_lt_veblenWith_iff, Ordinal.isNormal_opow, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o₁ o₂ a b : Ordinal.{u}
⊢ veblen o₁ a ≤ veblen o₂ b ↔ o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a ≤ b

Tactic:
veblenWith_le_veblenWith_iff (isNormal_opow one_lt_omega0)

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.veblenWith_le_veblenWith_iff, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o₁ o₂ a b : Ordinal.{u}
⊢ veblen o₁ a = veblen o₂ b ↔ o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a = b

Tactic:
veblenWith_eq_veblenWith_iff (isNormal_opow one_lt_omega0)

Premises used: Ordinal.veblen, Ordinal.isNormal_opow, Ordinal.veblenWith_eq_veblenWith_iff, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o x : Ordinal.{u}
h : o < x.invVeblen₁
⊢ veblen o x = x

Tactic:
simpa using notMem_of_lt_csInf' h

Premises used: notMem_of_lt_csInf'
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u_1}
⊢ x.invVeblen₁ ≤ x

Tactic:
csInf_le' (lt_veblen x).ne'

Premises used: csInf_le', LT.lt.ne', Ordinal.invVeblen₁, Ordinal.lt_veblen
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u_1}
⊢ x < veblen x.invVeblen₁ x

Tactic:
(right_le_veblen ..).lt_of_ne' (csInf_mem (s := {y | veblen y x ≠ x}) ⟨x, (lt_veblen x).ne'⟩)

Premises used: csInf_mem, LT.lt.ne', Exists.intro, Ordinal.lt_veblen, LE.le.lt_of_ne', Ordinal.right_le_veblen
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
inl : ∀ (h : o < a.invVeblen₁), a < veblen o a ↔ a.invVeblen₁ ≤ o
inr : ∀ (h : a.invVeblen₁ ≤ o), a < veblen o a ↔ a.invVeblen₁ ≤ o
⊢ a < veblen o a ↔ a.invVeblen₁ ≤ o

Tactic:
obtain h | h := lt_or_ge o (invVeblen₁ a)

Premises used: Ordinal.invVeblen₁, lt_or_ge
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
h : o < a.invVeblen₁
inl : a < a ↔ a.invVeblen₁ ≤ o
⊢ a < veblen o a ↔ a.invVeblen₁ ≤ o

Tactic:
rw [veblen_eq_of_lt_invVeblen₁ h]

Premises used: Ordinal.veblen_eq_of_lt_invVeblen₁
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
h : o < a.invVeblen₁
⊢ a < a ↔ a.invVeblen₁ ≤ o

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
h : a.invVeblen₁ ≤ o
⊢ a < veblen o a ↔ a.invVeblen₁ ≤ o

Tactic:
simpa [(lt_veblen_invVeblen₁ a).trans_le (veblen_left_monotone _ h)]

Premises used: LT.lt.trans_le, Ordinal.lt_veblen_invVeblen₁, Ordinal.veblen_left_monotone
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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₁
inr₁ : ∀ (h : x.invVeblen₁ < o), ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁

Tactic:
obtain h | rfl | h := lt_trichotomy o (invVeblen₁ x)

Premises used: Ordinal.invVeblen₁, rfl, lt_trichotomy
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o x : Ordinal.{u}
h : o < x.invVeblen₁
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁

Tactic:
iff_of_true ⟨_, veblen_opow_eq_opow_iff.2 <| veblen_eq_of_lt_invVeblen₁ h⟩ h.le

Premises used: Iff.mpr, Ordinal.veblen_eq_of_lt_invVeblen₁, Ordinal.veblen_opow_eq_opow_iff, LT.lt.le, iff_of_true, Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o x : Ordinal.{u}
h : o < x.invVeblen₁
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁

Tactic:
exact iff_of_true ⟨_, veblen_opow_eq_opow_iff.2 <| veblen_eq_of_lt_invVeblen₁ h⟩ h.le

Premises used: LT.lt.le, iff_of_true
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u}
apply : ω ^ x ∈ range (veblen x.invVeblen₁)
⊢ ω ^ x ∈ range (veblen x.invVeblen₁) ↔ x.invVeblen₁ ≤ x.invVeblen₁

Tactic:
apply iff_of_true _ le_rfl

Premises used: le_rfl, iff_of_true
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u}
pos : ∀ (h : x.invVeblen₁ = 0), ω ^ x ∈ range (veblen x.invVeblen₁)
neg : ∀ (h : ¬x.invVeblen₁ = 0), ω ^ x ∈ range (veblen x.invVeblen₁)
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)

Tactic:
by_cases h : invVeblen₁ x = 0

Premises used: Ordinal.invVeblen₁
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u}
h : x.invVeblen₁ = 0
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)

Tactic:
simp [h]
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u}
h : ¬x.invVeblen₁ = 0
neg : ∀ b < x.invVeblen₁, veblen b x = x
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)

Tactic:
simp_rw [mem_range_veblen h, veblen_opow_eq_opow_iff]

Premises used: Ordinal.veblen_opow_eq_opow_iff, Ordinal.mem_range_veblen
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u}
h : ¬x.invVeblen₁ = 0
⊢ ∀ b < x.invVeblen₁, veblen b x = x

Tactic:
fun o ↦ veblen_eq_of_lt_invVeblen₁

Premises used: Ordinal.veblen_eq_of_lt_invVeblen₁
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u}
h : ¬x.invVeblen₁ = 0
⊢ ∀ b < x.invVeblen₁, veblen b x = x

Tactic:
exact fun o ↦ veblen_eq_of_lt_invVeblen₁

Premises used: Ordinal.veblen_eq_of_lt_invVeblen₁
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
apply : ω ^ x ∉ range (veblen o)
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁

Tactic:
apply iff_of_false _ h.not_ge

Premises used: iff_of_false, LT.lt.not_ge
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz : veblen o z = ω ^ x
⊢ veblen o z = ω ^ x

Tactic:
have hz' := hz
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz hz' : veblen o z = ω ^ x
⊢ veblen x.invVeblen₁ x = x

Tactic:
rw [← veblen_veblen_of_lt h, hz', veblen_opow_eq_opow_iff] at hz

Premises used: Ordinal.veblen_opow_eq_opow_iff, Ordinal.veblen_veblen_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz hz' : veblen o z = ω ^ x
hz₁ : veblen x.invVeblen₁ x = x
⊢ veblen o z = ω ^ x

Tactic:
rw [← veblen_veblen_of_lt h, hz', veblen_opow_eq_opow_iff] at hz

Premises used: Ordinal.veblen_opow_eq_opow_iff, Ordinal.veblen_veblen_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz : veblen x.invVeblen₁ x = x
hz' : veblen o z = ω ^ x
⊢ False

Tactic:
(lt_veblen_invVeblen₁ x).ne' hz

Premises used: LT.lt.ne', Ordinal.lt_veblen_invVeblen₁
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz : veblen x.invVeblen₁ x = x
hz' : veblen o z = ω ^ x
⊢ False

Tactic:
exact (lt_veblen_invVeblen₁ x).ne' hz

Premises used: LT.lt.ne', Ordinal.lt_veblen_invVeblen₁
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
h : a < veblen o a
a₁ : (veblen o a).invVeblen₁ ≤ o
a₂ : o ≤ (veblen o a).invVeblen₁
⊢ (veblen o a).invVeblen₁ = o

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
h : a < veblen o a
a₁ : veblen o a < veblen o (veblen o a)
a₂ a₃ a₄ a₅ : a < veblen o a
⊢ (veblen o a).invVeblen₁ ≤ o

Tactic:
rwa [← lt_veblen_iff_invVeblen₁_le, veblen_lt_veblen_iff_right]

Premises used: Ordinal.lt_veblen_iff_invVeblen₁_le, Ordinal.veblen_lt_veblen_iff_right
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
h : a < veblen o a
a₁ : ω ^ veblen o a ∈ range (veblen o)
⊢ o ≤ (veblen o a).invVeblen₁

Tactic:
rw [← mem_range_veblen_iff_le_invVeblen₁]

Premises used: Ordinal.mem_range_veblen_iff_le_invVeblen₁
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
h : a < veblen o a
a₁ : ∀ (h : a < veblen 0 a), ω ^ veblen 0 a ∈ range (veblen 0)
a₂ : ∀ (ho : 0 < o), ω ^ veblen o a ∈ range (veblen o)
⊢ ω ^ veblen o a ∈ range (veblen o)

Tactic:
obtain rfl | ho := eq_zero_or_pos o

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a : Ordinal.{u}
h : a < veblen 0 a
⊢ ω ^ veblen 0 a ∈ range (veblen 0)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
a₁ : veblen o a ∈ range (veblen o)
⊢ ω ^ veblen o a ∈ range (veblen o)

Tactic:
rw [← veblen_zero_apply, veblen_veblen_of_lt ho]

Premises used: Ordinal.veblen_veblen_of_lt, Ordinal.veblen_zero_apply
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ veblen o a ∈ range (veblen o)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a : Ordinal.{u}
h : a < ω ^ a
rwa : a.invVeblen₁ ≤ 0
rwa₁ : a < veblen 0 a
rwa₂ rwa₃ rwa₄ rwa₅ : a < (fun (a : Ordinal.{u}) ↦ ω ^ a) a
⊢ a.invVeblen₁ = 0

Tactic:
rwa [← nonpos_iff_eq_zero, ← lt_veblen_iff_invVeblen₁_le, veblen_zero]

Premises used: Ordinal.veblen_zero, Ordinal.lt_veblen_iff_invVeblen₁_le, nonpos_iff_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u_1}
⊢ veblen x.invVeblen₁ x.invVeblen₂ = ω ^ x

Tactic:
Classical.choose_spec (mem_range_veblen_iff_le_invVeblen₁.2 le_rfl)

Premises used: Iff.mpr, le_rfl, Classical.choose_spec, Ordinal.mem_range_veblen_iff_le_invVeblen₁, Ordinal.invVeblen₂
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a x : Ordinal.{u}
rw : veblen x.invVeblen₁ x.invVeblen₂ = veblen x.invVeblen₁ a ↔ ω ^ x = veblen x.invVeblen₁ a
rw₁ rw₂ : ω ^ x = veblen x.invVeblen₁ a ↔ ω ^ x = veblen x.invVeblen₁ a
⊢ x.invVeblen₂ = a ↔ ω ^ x = veblen x.invVeblen₁ a

Tactic:
rw [← veblen_inj (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

Premises used: Ordinal.veblen_inj, Ordinal.veblen_invVeblen₁_invVeblen₂
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a x : Ordinal.{u}
rw : veblen x.invVeblen₁ x.invVeblen₂ < veblen x.invVeblen₁ a ↔ ω ^ x < veblen x.invVeblen₁ a
rw₁ rw₂ : ω ^ x < veblen x.invVeblen₁ a ↔ ω ^ x < veblen x.invVeblen₁ a
⊢ x.invVeblen₂ < a ↔ ω ^ x < veblen x.invVeblen₁ a

Tactic:
rw [← veblen_lt_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

Premises used: Ordinal.veblen_invVeblen₁_invVeblen₂, Ordinal.veblen_lt_veblen_iff_right
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a x : Ordinal.{u}
rw : veblen x.invVeblen₁ x.invVeblen₂ ≤ veblen x.invVeblen₁ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a
rw₁ rw₂ : ω ^ x ≤ veblen x.invVeblen₁ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a
⊢ x.invVeblen₂ ≤ a ↔ ω ^ x ≤ veblen x.invVeblen₁ a

Tactic:
rw [← veblen_le_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

Premises used: Ordinal.veblen_invVeblen₁_invVeblen₂, Ordinal.veblen_le_veblen_iff_right