awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a x : Ordinal.{u}
rw : veblen x.invVeblen₁ a < veblen x.invVeblen₁ x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x
rw₁ rw₂ : veblen x.invVeblen₁ a < ω ^ x ↔ veblen x.invVeblen₁ a < ω ^ x
⊢ a < x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x

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₁ a ≤ veblen x.invVeblen₁ x.invVeblen₂ ↔ veblen x.invVeblen₁ a ≤ ω ^ x
rw₁ rw₂ : veblen x.invVeblen₁ a ≤ ω ^ x ↔ veblen x.invVeblen₁ a ≤ ω ^ x
⊢ a ≤ x.invVeblen₂ ↔ veblen x.invVeblen₁ a ≤ ω ^ x

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
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u_1}
rw : x < veblen x.invVeblen₁ x
⊢ x.invVeblen₂ < ω ^ x

Tactic:
rw [invVeblen₂_lt_iff, opow_lt_veblen_opow_iff]

Premises used: Ordinal.opow_lt_veblen_opow_iff, Ordinal.invVeblen₂_lt_iff
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u_1}
⊢ x < veblen x.invVeblen₁ x

Tactic:
lt_veblen_invVeblen₁ x

Premises used: Ordinal.lt_veblen_invVeblen₁
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u_1}
⊢ x < veblen x.invVeblen₁ x

Tactic:
exact lt_veblen_invVeblen₁ x

Premises used: Ordinal.lt_veblen_invVeblen₁
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u_1}
inl : ∀ (h : x.invVeblen₁ = 0), x.invVeblen₂ ≤ x
inr : ∀ (h : 0 < x.invVeblen₁), x.invVeblen₂ ≤ x
⊢ x.invVeblen₂ ≤ x

Tactic:
obtain h | h := eq_zero_or_pos (invVeblen₁ x)

Premises used: eq_zero_or_pos, Ordinal.invVeblen₁
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u_1}
h : x.invVeblen₁ = 0
inl : ω ^ x ≤ veblen x.invVeblen₁ x
inl₁ : ω ^ x ≤ veblen 0 x
inl₂ inl₃ : ω ^ x ≤ ω ^ x
⊢ x.invVeblen₂ ≤ x

Tactic:
rw [invVeblen₂_le_iff, h, veblen_zero]

Premises used: Ordinal.invVeblen₂_le_iff, Ordinal.veblen_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u_1}
h : 0 < x.invVeblen₁
⊢ x.invVeblen₂ ≤ ω ^ x

Tactic:
(invVeblen₂_lt x).le

Premises used: LT.lt.le, Ordinal.invVeblen₂_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u_1}
h : 0 < x.invVeblen₁
h₁ : x = ω ^ x
⊢ x.invVeblen₂ ≤ x

Tactic:
convert! (invVeblen₂_lt x).le

Premises used: LT.lt.le, Ordinal.invVeblen₂_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
x : Ordinal.{u_1}
h : 0 < x.invVeblen₁
h₁ : x = veblen 0 x
h₂ h₃ : x = x
⊢ x = ω ^ x

Tactic:
rw [← veblen_zero_apply, veblen_eq_of_lt_invVeblen₁ h]

Premises used: Ordinal.veblen_eq_of_lt_invVeblen₁, Ordinal.veblen_zero_apply
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a : Ordinal.{u}
h : a < ω ^ a
rw : ω ^ a = veblen a.invVeblen₁ a
rw₁ : ω ^ a = veblen 0 a
rw₂ rw₃ : ω ^ a = ω ^ a
⊢ a.invVeblen₂ = a

Tactic:
rw [invVeblen₂_eq_iff, invVeblen₁_of_lt_opow h, veblen_zero_apply]

Premises used: Ordinal.invVeblen₂_eq_iff, Ordinal.invVeblen₁_of_lt_opow, Ordinal.veblen_zero_apply
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
h : 0 < HPow.hPow (β := Ordinal.{u_1}) ω 0
⊢ invVeblen₂ 0 = 0

Tactic:
apply invVeblen₂_of_lt_opow

Premises used: Ordinal.invVeblen₂_of_lt_opow
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
h₁ : 0 < o
⊢ (veblen o a).invVeblen₂ = a

Tactic:
rw [invVeblen₂_eq_iff, invVeblen₁_veblen h, ← veblen_zero_apply, veblen_veblen_of_lt]

Premises used: Ordinal.invVeblen₂_eq_iff, Ordinal.veblen_veblen_of_lt, Ordinal.veblen_zero_apply, Ordinal.invVeblen₁_veblen
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ 0 < o

Tactic:
ho.bot_lt

Premises used: Ne.bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ 0 < o

Tactic:
exact ho.bot_lt

Premises used: Ne.bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a x : Ordinal.{u}
h : a < veblen o a
⊢ veblen o a = ω ^ x ↔ x.invVeblen₁ = o ∧ x.invVeblen₂ = a

Tactic:
⟨?_, fun ⟨hx, ha⟩ ↦ ?_⟩

Premises used: Ordinal.veblen, Ordinal.omega0, HPow.hPow, _private.0.Ordinal.veblen_eq_opow_iff.match_1, Iff.intro, Eq
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a x : Ordinal.{u}
h : a < veblen o a
refine_1 : veblen o a = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
refine_2 : x.invVeblen₁ = o ∧ x.invVeblen₂ = a → ∀ (hx : x.invVeblen₁ = o) (ha : x.invVeblen₂ = a), veblen o a = ω ^ x
⊢ veblen o a = ω ^ x ↔ x.invVeblen₁ = o ∧ x.invVeblen₂ = a

Tactic:
refine ⟨?_, fun ⟨hx, ha⟩ ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
refine_1₁ : ∀ (ho : 0 < o), veblen o a = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
⊢ veblen o a = ω ^ x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a

Tactic:
obtain rfl | ho := eq_zero_or_pos o

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

Tactic:
rw [veblen_zero] at h

Premises used: Ordinal.veblen_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a x : Ordinal.{u}
h : a < (fun (a : Ordinal.{u}) ↦ ω ^ a) a
⊢ a.invVeblen₁ = 0

Tactic:
have := invVeblen₁_of_lt_opow h
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a x : Ordinal.{u}
h : a < (fun (a : Ordinal.{u}) ↦ ω ^ a) a
this : a.invVeblen₁ = 0
⊢ a.invVeblen₂ = a

Tactic:
have := invVeblen₂_of_lt_opow h
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a x : Ordinal.{u}
h : a < (fun (a : Ordinal.{u}) ↦ ω ^ a) a
this_1 : a.invVeblen₁ = 0
this : a.invVeblen₂ = a
⊢ veblen 0 a = ω ^ x → x.invVeblen₁ = 0 ∧ x.invVeblen₂ = a

Tactic:
aesop
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a x : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
refine_1 : veblen o a = x → x.invVeblen₁ = o ∧ x.invVeblen₂ = a
⊢ 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]

Premises used: Ordinal.veblen_veblen_of_lt, Ordinal.veblen_zero_apply, Ordinal.opow_right_inj, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ (veblen o a).invVeblen₁ = o ∧ (veblen o a).invVeblen₂ = a

Tactic:
simp [invVeblen₁_veblen h, invVeblen₂_veblen ho.ne' h]

Premises used: LT.lt.ne', Ordinal.invVeblen₁_veblen, Ordinal.invVeblen₂_veblen
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a x : Ordinal.{u}
h : a < veblen o a
h_1 : x.invVeblen₁ = o ∧ x.invVeblen₂ = a
hx : x.invVeblen₁ = o
ha : x.invVeblen₂ = a
⊢ veblen x.invVeblen₁ x.invVeblen₂ = ω ^ x

Tactic:
veblen_invVeblen₁_invVeblen₂ x

Premises used: Ordinal.veblen_invVeblen₁_invVeblen₂
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o a x : Ordinal.{u}
h : a < veblen o a
h_1 : x.invVeblen₁ = o ∧ x.invVeblen₂ = a
hx : x.invVeblen₁ = o
ha : x.invVeblen₂ = a
⊢ veblen o a = ω ^ x

Tactic:
convert! ← veblen_invVeblen₁_invVeblen₂ x

Premises used: Ordinal.veblen_invVeblen₁_invVeblen₂
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ ε_ o = deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o

Tactic:
simpa [epsilon] using congrFun (veblen_add_one 0) o

Premises used: Ordinal.veblen_add_one, congrFun, Ordinal.epsilon, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
rw : deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0 = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0
rw₁ rw₂ : nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0 = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0
⊢ ε_ 0 = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0

Tactic:
rw [epsilon_eq_deriv, deriv_zero_right]

Premises used: Ordinal.epsilon_eq_deriv, Ordinal.deriv_zero_right
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
rw : deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ o) = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (ε_ o))
rw₁ :
  deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ o) =
    nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o))
rw₂ rw₃ :
  nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o)) =
    nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o))
⊢ ε_ (succ o) = nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) (succ (ε_ o))

Tactic:
rw [epsilon_eq_deriv, epsilon_eq_deriv, deriv_succ]

Premises used: Ordinal.epsilon_eq_deriv, Ordinal.deriv_succ
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : ω ^ o ≤ o
rw : nfp (fun (a : Ordinal.{u}) ↦ ω ^ a) 0 ≤ o
⊢ ε_ 0 ≤ o

Tactic:
rw [epsilon_zero_eq_nfp]

Premises used: Ordinal.epsilon_zero_eq_nfp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : ω ^ o ≤ o
⊢ nfp (fun (a : Ordinal.{u}) ↦ ω ^ a) 0 ≤ o

Tactic:
nfp_le_fp (fun _ _ ↦ (opow_le_opow_iff_right one_lt_omega0).2) zero_le h

Premises used: Iff.mpr, zero_le, Ordinal.nfp_le_fp, Ordinal.opow_le_opow_iff_right, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : ω ^ o ≤ o
⊢ nfp (fun (a : Ordinal.{u}) ↦ ω ^ a) 0 ≤ o

Tactic:
exact nfp_le_fp (fun _ _ ↦ (opow_le_opow_iff_right one_lt_omega0).2) zero_le h

Premises used: Iff.mpr, zero_le, Ordinal.nfp_le_fp, Ordinal.opow_le_opow_iff_right, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
rw : ω ^ deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o = deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o
rw₁ rw₂ : deriv (fun (x : Ordinal.{u_1}) ↦ ω ^ x) o = deriv (fun (a : Ordinal.{u_1}) ↦ ω ^ a) o
⊢ ω ^ ε_ o = ε_ o

Tactic:
rw [epsilon_eq_deriv, deriv_fp (isNormal_opow one_lt_omega0)]

Premises used: Ordinal.epsilon_eq_deriv, Ordinal.deriv_fp, Ordinal.isNormal_opow, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
rw : o < nfp (fun (a : Ordinal.{u}) ↦ ω ^ a) 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ ω ^ a)^[n] 0
rw₁ rw₂ : (∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ ω ^ a)^[n] 0) ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ ω ^ a)^[n] 0
⊢ o < ε_ 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ ω ^ a)^[n] 0

Tactic:
rw [epsilon_zero_eq_nfp, lt_nfp_iff]

Premises used: Ordinal.epsilon_zero_eq_nfp, Ordinal.lt_nfp_iff
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
n : ℕ
rw : (fun (a : Ordinal.{u_1}) ↦ ω ^ a)^[n] 0 < nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0
⊢ (fun (a : Ordinal.{u_1}) ↦ ω ^ a)^[n] 0 < ε_ 0

Tactic:
rw [epsilon_zero_eq_nfp]

Premises used: Ordinal.epsilon_zero_eq_nfp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
n : ℕ
h : 0 < HPow.hPow (β := Ordinal.{u_1}) ω 0
⊢ (fun (a : Ordinal.{u_1}) ↦ ω ^ a)^[n] 0 < nfp (fun (a : Ordinal.{u_1}) ↦ ω ^ a) 0

Tactic:
apply iterate_lt_nfp (isNormal_opow one_lt_omega0).strictMono

Premises used: Ordinal.isNormal_opow, Order.IsNormal.strictMono, Ordinal.one_lt_omega0, Ordinal.iterate_lt_nfp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
n : ℕ
⊢ 0 < HPow.hPow (β := Ordinal.{u_1}) ω 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
apply : ω < veblen 1 0
⊢ ω < ε_ o

Tactic:
apply lt_of_lt_of_le _ <| (veblen_right_strictMono _).monotone zero_le

Premises used: zero_le, StrictMono.monotone, Ordinal.veblen_right_strictMono, lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ ω < veblen 1 0

Tactic:
simpa using iterate_omega0_opow_lt_epsilon_zero 2

Premises used: OfNat.ofNat, Ordinal.iterate_omega0_opow_lt_epsilon_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
n : ℕ
o : Ordinal.{u_1}
⊢ (↑n : Ordinal.{u_1}) < ε_ o

Tactic:
(natCast_lt_omega0 n).trans <| omega0_lt_epsilon o

Premises used: Ordinal.omega0_lt_epsilon, Ordinal.natCast_lt_omega0, LT.lt.trans
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ 0 < ε_ o

Tactic:
veblen_pos

Premises used: Ordinal.veblen_pos
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : o < ε_ o
⊢ (ε_ o).invVeblen₁ = 1

Tactic:
invVeblen₁_veblen h

Premises used: Ordinal.invVeblen₁_veblen
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : o < ε_ o
⊢ (ε_ o).invVeblen₂ = o

Tactic:
invVeblen₂_veblen one_ne_zero h

Premises used: one_ne_zero, Ordinal.invVeblen₂_veblen
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
⊢ IsNormal Γ_

Tactic:
isNormal_deriv _

Premises used: Ordinal.isNormal_deriv, Ordinal.gamma
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
⊢ o ∈ range Γ_ ↔ veblen o 0 = o

Tactic:
mem_range_deriv isNormal_veblen_zero

Premises used: Set.Mem, Ordinal.isNormal_veblen_zero, Ordinal.mem_range_deriv, Ordinal.gamma
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
⊢ StrictMono Γ_

Tactic:
isNormal_gamma.strictMono

Premises used: Ordinal.isNormal_gamma, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
⊢ Monotone Γ_

Tactic:
isNormal_gamma.monotone

Premises used: Order.IsNormal.monotone, Ordinal.isNormal_gamma
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a b : Ordinal.{u}
⊢ Γ_ a < Γ_ b ↔ a < b

Tactic:
strictMono_gamma.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Ordinal.strictMono_gamma
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a b : Ordinal.{u}
⊢ Γ_ a ≤ Γ_ b ↔ a ≤ b

Tactic:
strictMono_gamma.le_iff_le

Premises used: Ordinal.strictMono_gamma, StrictMono.le_iff_le
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
a b : Ordinal.{u}
⊢ Γ_ a = Γ_ b ↔ a = b

Tactic:
strictMono_gamma.injective.eq_iff

Premises used: Function.Injective.eq_iff, StrictMono.injective, Ordinal.strictMono_gamma
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ veblen (Γ_ o) 0 = Γ_ o

Tactic:
deriv_fp isNormal_veblen_zero o

Premises used: Ordinal.deriv_fp, Ordinal.isNormal_veblen_zero, Ordinal.gamma
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
⊢ Γ_ 0 = nfp (fun (x : Ordinal.{u_1}) ↦ veblen x 0) 0

Tactic:
deriv_zero_right _

Premises used: Ordinal.gamma, Ordinal.deriv_zero_right
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ Γ_ (succ o) = nfp (fun (x : Ordinal.{u_1}) ↦ veblen x 0) (succ (Γ_ o))

Tactic:
deriv_succ _ _

Premises used: Ordinal.deriv_succ, Ordinal.gamma
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : veblen o 0 ≤ o
rw : nfp (fun (x : Ordinal.{u}) ↦ veblen x 0) 0 ≤ o
⊢ Γ_ 0 ≤ o

Tactic:
rw [gamma_zero_eq_nfp]

Premises used: Ordinal.gamma_zero_eq_nfp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : veblen o 0 ≤ o
⊢ nfp (fun (x : Ordinal.{u}) ↦ veblen x 0) 0 ≤ o

Tactic:
nfp_le_fp (veblen_left_monotone 0) zero_le h

Premises used: zero_le, Ordinal.nfp_le_fp, OfNat.ofNat, Ordinal.veblen_left_monotone
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : veblen o 0 ≤ o
⊢ nfp (fun (x : Ordinal.{u}) ↦ veblen x 0) 0 ≤ o

Tactic:
exact nfp_le_fp (veblen_left_monotone 0) zero_le h

Premises used: zero_le, Ordinal.nfp_le_fp, OfNat.ofNat, Ordinal.veblen_left_monotone
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
rw : o < nfp (fun (x : Ordinal.{u}) ↦ veblen x 0) 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ veblen a 0)^[n] 0
rw₁ rw₂ :
  (∃ (n : ℕ), o < (fun (x : Ordinal.{u}) ↦ veblen x 0)^[n] 0) ↔
    ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ veblen a 0)^[n] 0
⊢ o < Γ_ 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) ↦ veblen a 0)^[n] 0

Tactic:
rw [gamma_zero_eq_nfp, lt_nfp_iff]

Premises used: Ordinal.gamma_zero_eq_nfp, Ordinal.lt_nfp_iff
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
n : ℕ
rw : (fun (a : Ordinal.{u_1}) ↦ veblen a 0)^[n] 0 < nfp (fun (x : Ordinal.{u_1}) ↦ veblen x 0) 0
⊢ (fun (a : Ordinal.{u_1}) ↦ veblen a 0)^[n] 0 < Γ_ 0

Tactic:
rw [gamma_zero_eq_nfp]

Premises used: Ordinal.gamma_zero_eq_nfp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
n : ℕ
h : 0 < veblen 0 0
⊢ (fun (a : Ordinal.{u_1}) ↦ veblen a 0)^[n] 0 < nfp (fun (x : Ordinal.{u_1}) ↦ veblen x 0) 0

Tactic:
apply iterate_lt_nfp veblen_zero_strictMono

Premises used: Ordinal.veblen_zero_strictMono, Ordinal.iterate_lt_nfp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
n : ℕ
⊢ 0 < veblen 0 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
apply : ε_ 0 < Γ_ 0
⊢ ε_ 0 < Γ_ o

Tactic:
apply (gamma_le_gamma.2 zero_le).trans_lt'

Premises used: Iff.mpr, zero_le, Ordinal.gamma_le_gamma, LE.le.trans_lt'
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ ε_ 0 < Γ_ 0

Tactic:
simpa using iterate_veblen_lt_gamma_zero 2

Premises used: Ordinal.iterate_veblen_lt_gamma_zero, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
⊢ ω < Γ_ o

Tactic:
(omega0_lt_epsilon 0).trans (epsilon_zero_lt_gamma o)

Premises used: Ordinal.epsilon_zero_lt_gamma, Ordinal.omega0_lt_epsilon, LT.lt.trans, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
n : ℕ
⊢ (↑n : Ordinal.{u}) < Γ_ o

Tactic:
(natCast_lt_omega0 n).trans (omega0_lt_gamma o)

Premises used: Ordinal.natCast_lt_omega0, Ordinal.omega0_lt_gamma, LT.lt.trans
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
⊢ 0 < Γ_ o

Tactic:
natCast_lt_gamma 0

Premises used: OfNat.ofNat, Ordinal.natCast_lt_gamma
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
⊢ Γ_ o ≠ 0

Tactic:
gamma_pos.ne'

Premises used: Ordinal.gamma_pos, LT.lt.ne'
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
rw : (veblen (Γ_ o) 0).invVeblen₁ = veblen (Γ_ o) 0
rw₁ : Γ_ o = veblen (Γ_ o) 0
rw₂ rw₃ : Γ_ o = Γ_ o
⊢ (Γ_ o).invVeblen₁ = Γ_ o

Tactic:
rw [← veblen_gamma_zero, invVeblen₁_veblen veblen_pos, veblen_gamma_zero]

Premises used: Ordinal.veblen_gamma_zero, Ordinal.invVeblen₁_veblen, Ordinal.veblen_pos
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u_1}
rw : (veblen (Γ_ o) 0).invVeblen₂ = 0
rw₁ rw₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 0 0
⊢ (Γ_ o).invVeblen₂ = 0

Tactic:
rw [← veblen_gamma_zero, invVeblen₂_veblen gamma_ne_zero veblen_pos]

Premises used: Ordinal.gamma_ne_zero, Ordinal.veblen_gamma_zero, Ordinal.veblen_pos, Ordinal.invVeblen₂_veblen
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
mp : o.invVeblen₁ = o → o = 0 ∨ o ∈ range Γ_
mpr : o = 0 ∨ o ∈ range Γ_ → o.invVeblen₁ = o
⊢ o.invVeblen₁ = o ↔ o = 0 ∨ o ∈ range Γ_

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
mp : o.invVeblen₁ = o → ¬o = 0 → veblen o 0 = o
⊢ o.invVeblen₁ = o → o = 0 ∨ o ∈ range Γ_

Tactic:
rw [mem_range_gamma, or_iff_not_imp_left]

Premises used: Ordinal.mem_range_gamma, Classical.or_iff_not_imp_left
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
⊢ o.invVeblen₁ = o → ¬o = 0 → veblen o 0 = o

Tactic:
fun h ho ↦ (left_le_veblen ..).antisymm' ?_

Premises used: LE.le.antisymm', Ordinal.left_le_veblen, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
mp : ∀ (h : o.invVeblen₁ = o) (ho : ¬o = 0), veblen o 0 ≤ o
⊢ o.invVeblen₁ = o → ¬o = 0 → veblen o 0 = o

Tactic:
refine fun h ho ↦ (left_le_veblen ..).antisymm' ?_

Premises used: LE.le.antisymm', Ordinal.left_le_veblen
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
rw : veblen o o.invVeblen₂
| o

Tactic:
rw [← veblen_eq_of_lt_invVeblen₁ (h.trans_ne ho).bot_lt, bot_eq_zero,
      veblen_zero_apply, ← veblen_invVeblen₁_invVeblen₂, h]

Premises used: Ordinal.veblen_eq_of_lt_invVeblen₁, Ordinal.bot_eq_zero, Ordinal.veblen_invVeblen₁_invVeblen₂, Eq.trans_ne, Ordinal.veblen_zero_apply, Ne.bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
mp : veblen o 0 ≤ veblen o o.invVeblen₂
⊢ veblen o 0 ≤ o

Tactic:
conv_rhs => rw [← veblen_eq_of_lt_invVeblen₁ (h.trans_ne ho).bot_lt, bot_eq_zero,
      veblen_zero_apply, ← veblen_invVeblen₁_invVeblen₂, h]

Premises used: Ordinal.veblen_eq_of_lt_invVeblen₁, Ordinal.bot_eq_zero, Ordinal.veblen_invVeblen₁_invVeblen₂, Eq.trans_ne, Ordinal.veblen_zero_apply, Ne.bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
⊢ veblen o 0 ≤ veblen o o.invVeblen₂

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
⊢ o = 0 ∨ o ∈ range Γ_ → o.invVeblen₁ = o

Tactic:
aesop
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
rw : o.invVeblen₁ ≠ o ↔ o ≠ 0 ∧ o ∉ range Γ_
rw₁ : ¬o.invVeblen₁ = o ↔ o ≠ 0 ∧ o ∉ range Γ_
rw₂ : ¬(o = 0 ∨ o ∈ range Γ_ ) ↔ o ≠ 0 ∧ o ∉ range Γ_
rw₃ rw₄ : ¬o = 0 ∧ o ∉ range Γ_ ↔ o ≠ 0 ∧ o ∉ range Γ_
⊢ o.invVeblen₁ < o ↔ o ≠ 0 ∧ o ∉ range Γ_

Tactic:
rw [(invVeblen₁_le o).lt_iff_ne, ne_eq, invVeblen₁_eq_iff, not_or]

Premises used: Ordinal.invVeblen₁_le, ne_eq, not_or, LE.le.lt_iff_ne, Ordinal.invVeblen₁_eq_iff
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : PSet.{u_1}
⊢ ⟦x⟧ = mk x

Tactic:
rfl

Premises used: ZFSet.mk, rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
⊢ ∀ (x : ZFSet.{u_1}), mk (Quotient.out x) = x

Tactic:
Quotient.out_eq

Premises used: ZFSet, ZFSet.mk, Quotient.out_eq
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x : PSet.{u}
⊢ ZFSet.mk (out f x) = f (ZFSet.mk x)

Tactic:
Definable.mk_out ![x]

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Matrix.vecEmpty, Fin.cases, ZFSet.Definable.mk_out, Matrix.vecCons
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}
inst : Definable₂ f
x y : PSet.{u}
⊢ ZFSet.mk (out f x y) = f (ZFSet.mk x) (ZFSet.mk y)

Tactic:
Definable.mk_out ![x, y]

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Matrix.vecEmpty, Fin.cases, ZFSet.Definable.mk_out, Matrix.vecCons
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
rw : (f fun (x : Fin n) ↦ ZFSet.mk (xs x)) = f fun (x : Fin n) ↦ ZFSet.mk (ys x)
⊢ out f xs ≈ out f ys

Tactic:
rw [← Quotient.eq_iff_equiv, mk_eq, mk_eq, mk_out, mk_out]

Premises used: ZFSet.mk_eq, Quotient.eq_iff_equiv, ZFSet.Definable.mk_out
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ (f fun (x : Fin n) ↦ ZFSet.mk (xs x)) = f fun (x : Fin n) ↦ ZFSet.mk (ys x)

Tactic:
congrArg _ (funext fun i ↦ Quotient.sound (h i))

Premises used: congrArg, funext, Quotient.sound
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ (f fun (x : Fin n) ↦ ZFSet.mk (xs x)) = f fun (x : Fin n) ↦ ZFSet.mk (ys x)

Tactic:
exact congrArg _ (funext fun i ↦ Quotient.sound (h i))

Premises used: congrArg, funext, Quotient.sound
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : PSet.{u}
h : x ≈ y
⊢ ∀ (i : Fin (Nat.succ 0)), ![x] i ≈ ![y] i

Tactic:
simp [h]
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}
inst : Definable₂ f
x₁ y₁ x₂ y₂ : PSet.{u}
h₁ : x₁ ≈ y₁
h₂ : x₂ ≈ y₂
⊢ ∀ (i : Fin (Nat.succ 0).succ), ![x₁, x₂] i ≈ ![y₁, y₂] i

Tactic:
simp [Fin.forall_fin_succ, h₁, h₂]

Premises used: Fin.forall_fin_succ
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : PSet.{u_1}
⊢ mk x = mk y ↔ x.Equiv y

Tactic:
Quotient.eq

Premises used: ZFSet, ZFSet.mk, Quotient.eq
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : PSet.{u_1}
h : x.Equiv y
⊢ mk x = mk y

Tactic:
Quotient.sound h

Premises used: ZFSet, ZFSet.mk, Quotient.sound
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : PSet.{u_1}
⊢ mk x = mk y → x.Equiv y

Tactic:
Quotient.exact

Premises used: ZFSet, ZFSet.mk, Quotient.exact
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ (∀ (z : ZFSet.{u}), z ∈ x.toSet ↔ z ∈ y.toSet) → x = y

Tactic:
Quotient.inductionOn₂ x y fun _ _ h => Quotient.sound (Mem.ext fun w => h ⟦w⟧)

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y_1 z x y : ZFSet.{u}
hxy : x.toSet = y.toSet
a : ∀ (z : ZFSet.{u}), z ∈ x.toSet ↔ z ∈ y.toSet
⊢ x = y

Tactic:
apply ext_aux

Premises used: _private.0.ZFSet.ext_aux