awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ o <
    Ordinal.liftPrincipalSeg.top (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
      fun (x1 x2 : Ordinal.{max (u + 1) v}) ↦ x1 < x2)

Tactic:
simpa using h
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (u + 1) v}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    o

Tactic:
have := Ordinal.liftPrincipalSeg.mem_range_of_rel_top (by simpa using h)
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
this :
  Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (u + 1) v}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    o
rcases :
  ∀ (o_1 : Ordinal.{u})
    (h' :
      (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
              fun (x1 x2 : Ordinal.{max (u + 1) v}) ↦ x1 < x2) :
            (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
          o_1 =
        o),
    o.card < univ.{u, v}
⊢ o.card < univ.{u, v}

Tactic:
rcases this with ⟨o, h'⟩
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
o_1 : Ordinal.{max (u + 1) v}
h : o_1 < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' :
  (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (u + 1) v}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      o =
    o_1
rw : lift.{max (u + 1) v, u} o.card < univ.{u, v}
⊢ o_1.card < univ.{u, v}

Tactic:
rw [← h', Ordinal.liftPrincipalSeg_coe, ← Ordinal.lift_card]

Premises used: Ordinal.liftPrincipalSeg_coe, Ordinal.lift_card
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
o_1 : Ordinal.{max (u + 1) v}
h : o_1 < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' :
  (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (u + 1) v}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      o =
    o_1
⊢ lift.{max (u + 1) v, u} o.card < univ.{u, v}

Tactic:
apply lift_lt_univ'

Premises used: Cardinal.lift_lt_univ'
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
⊢ c.ord < univ.{u, u + 1}.ord

Tactic:
have := ord_lt_ord.2 h
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < univ.{u, u + 1}.ord
⊢ c.ord < Ordinal.univ.{u, u + 1}

Tactic:
rw [ord_univ] at this

Premises used: Cardinal.ord_univ
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
⊢ c.ord <
    Ordinal.liftPrincipalSeg.top (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦
      x1 < x2)

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
obtain :
  ∀ (o : Ordinal.{u})
    (e :
      (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
              fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) :
            (a : Ordinal.{u}) → Ordinal.{u + 1})
          o =
        c.ord),
    ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'
⊢ ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'

Tactic:
obtain ⟨o, e⟩ := Ordinal.liftPrincipalSeg.mem_range_of_rel_top (by simpa)

Premises used: PrincipalSeg.mem_range_of_rel_top, Ordinal.liftPrincipalSeg
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e :
  (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    c.ord
⊢ c.ord.card = c

Tactic:
have := card_ord c
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this_1 : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e :
  (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    c.ord
this : c.ord.card = c
⊢ lift.{u + 1, u} o.card = c

Tactic:
rw [← e, Ordinal.liftPrincipalSeg_coe, ← Ordinal.lift_card] at this

Premises used: Ordinal.liftPrincipalSeg_coe, Ordinal.lift_card
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this_1 : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e :
  (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    c.ord
this : lift.{u + 1, u} o.card = c
⊢ ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'

Tactic:
⟨_, this.symm⟩

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this_1 : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e :
  (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    c.ord
this : lift.{u + 1, u} o.card = c
⊢ ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'

Tactic:
exact ⟨_, this.symm⟩
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
let :
  ∀ (a : Cardinal.{u + 1}) (h' : a < #Ordinal.{u}) (e : lift.{v, u + 1} a = c),
    ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'
⊢ ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'

Tactic:
let ⟨a, h', e⟩ := lt_lift_iff.1 h
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < #Ordinal.{u}
e : lift.{v, u + 1} a = c
⊢ a < univ.{u, u + 1}

Tactic:
rw [mk_ordinal] at h'

Premises used: Cardinal.mk_ordinal
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < #Ordinal.{u}
e : lift.{v, u + 1} a = c
h'₁ : a < univ.{u, u + 1}
⊢ lift.{v, u + 1} a = c

Tactic:
rw [mk_ordinal] at h'

Premises used: Cardinal.mk_ordinal
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < univ.{u, u + 1}
e : lift.{v, u + 1} a = c
rcases :
  ∀ (c' : Cardinal.{u}) (h' : lift.{u + 1, u} c' < univ.{u, u + 1}) (e : lift.{v, u + 1} (lift.{u + 1, u} c') = c),
    ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'
⊢ ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'

Tactic:
rcases lt_univ.{u}.1 h' with ⟨c', rfl⟩

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
c' : Cardinal.{u}
h' : lift.{u + 1, u} c' < univ.{u, u + 1}
e : lift.{v, u + 1} (lift.{u + 1, u} c') = c
⊢ c = lift.{max (u + 1) v, u} c'

Tactic:
simp only [e.symm, lift_lift]

Premises used: Cardinal.lift_lift, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
c' : Cardinal.{u}
h' : lift.{u + 1, u} c' < univ.{u, u + 1}
e : lift.{v, u + 1} (lift.{u + 1, u} c') = c
⊢ ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'

Tactic:
exact ⟨c', by simp only [e.symm, lift_lift]⟩
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{max (u + 1) v}
h_1 : c < Cardinal.univ.{u, v}
w : Cardinal.{u}
h : c = lift.{max (u + 1) v, u} w
⊢ HPow.hPow (α := Cardinal.{max (u + 1) v}) 2 c = lift.{max (u + 1) v, u} (HPow.hPow (α := Cardinal.{u}) 2 w)

Tactic:
simp [h]
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
α : Type u
rw : Small.{v, u} α ↔ ∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
⊢ Small.{v, u} α ↔ lift.{v + 1, u} #α < univ.{v, max u (v + 1)}

Tactic:
rw [lt_univ']

Premises used: Cardinal.lt_univ'
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
α : Type u
mp : Small.{v, u} α → ∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
mpr : (∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c') → Small.{v, u} α
⊢ Small.{v, u} α ↔ ∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
α : Type u
β : Type v
e : Nonempty (α ≃ β)
⊢ ∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Tactic:
⟨#β, lift_mk_eq.{u, _, v + 1}.2 e⟩

Premises used: Iff.mpr, Cardinal.mk, Cardinal.lift_mk_eq, Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
α : Type u
β : Type v
e : Nonempty (α ≃ β)
⊢ ∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Tactic:
exact ⟨#β, lift_mk_eq.{u, _, v + 1}.2 e⟩
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
α : Type u
c : Cardinal.{v}
hc : lift.{v + 1, u} #α = lift.{max u (v + 1), v} c
⊢ Small.{v, u} α

Tactic:
⟨⟨c.out, lift_mk_eq.{u, _, v + 1}.1 (hc.trans (congr rfl c.mk_out.symm))⟩⟩

Premises used: Cardinal.mk_out, Quotient.out, Small.mk, Cardinal.lift_mk_eq, congr, Exists.intro, Iff.mp, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
α : Type u
c : Cardinal.{v}
hc : lift.{v + 1, u} #α = lift.{max u (v + 1), v} c
⊢ Small.{v, u} α

Tactic:
exact ⟨⟨c.out, lift_mk_eq.{u, _, v + 1}.1 (hc.trans (congr rfl c.mk_out.symm))⟩⟩
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
rw₁ rw₂ : f = f
⊢ veblenWith f 0 = f

Tactic:
rw [veblenWith, if_pos rfl]

Premises used: if_pos, Ordinal.veblenWith, rfl
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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})
rw₁ 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})
⊢ veblenWith f o = derivFamily fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u})

Tactic:
rw [veblenWith, if_neg h]

Premises used: Ordinal.veblenWith, if_neg
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
rw : IsNormal (derivFamily fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u}))
⊢ IsNormal (veblenWith f o)

Tactic:
rw [veblenWith_of_ne_zero f h]

Premises used: Ordinal.veblenWith_of_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (derivFamily fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u}))

Tactic:
isNormal_derivFamily _

Premises used: Ordinal.isNormal_derivFamily
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (derivFamily fun (x : (↑(Iio o) : Type (u + 1))) ↦ veblenWith f (↑x : Ordinal.{u}))

Tactic:
exact isNormal_derivFamily _

Premises used: Ordinal.isNormal_derivFamily
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
inl : IsNormal (veblenWith f 0)
inr : ∀ (h : o ≠ 0), IsNormal (veblenWith f o)
⊢ IsNormal (veblenWith f o)

Tactic:
obtain rfl | h := eq_or_ne o 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf inl inl₁ inl₂ inl₃ : IsNormal f
⊢ IsNormal (veblenWith f 0)

Tactic:
rwa [veblenWith_zero]

Premises used: Ordinal.veblenWith_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (veblenWith f o)

Tactic:
isNormal_veblenWith' f h

Premises used: Ordinal.isNormal_veblenWith'
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (veblenWith f o)

Tactic:
exact isNormal_veblenWith' f h

Premises used: Ordinal.isNormal_veblenWith'
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
rw : (∀ (i : (↑(Iio o) : Type (u + 1))), veblenWith f (↑i : Ordinal.{u}) a = a) ↔ ∀ b < o, veblenWith f b a = a
⊢ a ∈ range (veblenWith f o) ↔ ∀ b < o, veblenWith f b a = a

Tactic:
rw [veblenWith_of_ne_zero f h, mem_range_derivFamily (fun _ ↦ isNormal_veblenWith hf _)]

Premises used: Ordinal.isNormal_veblenWith, Ordinal.mem_range_derivFamily, Ordinal.veblenWith_of_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
⊢ (∀ (i : (↑(Iio o) : Type (u + 1))), veblenWith f (↑i : Ordinal.{u}) a = a) ↔ ∀ b < o, veblenWith f b a = a

Tactic:
Subtype.forall

Premises used: Set.Mem, setOf, Subtype.forall, Set.Iio
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
⊢ (∀ (i : (↑(Iio o) : Type (u + 1))), veblenWith f (↑i : Ordinal.{u}) a = a) ↔ ∀ b < o, veblenWith f b a = a

Tactic:
exact Subtype.forall

Premises used: Subtype.forall
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
a : Ordinal.{u}
apply : veblenWith f o₂ a ∈ range (veblenWith f o₂)
⊢ veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a

Tactic:
apply (mem_range_veblenWith hf h.ne_bot).1 _ _ h

Premises used: Iff.mp, Ordinal.mem_range_veblenWith, LT.lt.ne_bot
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
a : Ordinal.{u}
⊢ veblenWith f o₂ a ∈ range (veblenWith f o₂)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
inr : ∀ (h : o₁ < o₂), veblenWith f o₁ a = a
⊢ veblenWith f o₁ a = a

Tactic:
obtain rfl | h := h.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o₁ a : Ordinal.{u}
hf : IsNormal f
h : o₁ ≤ o₁
h' : veblenWith f o₁ a = a
⊢ veblenWith f o₁ a = a

Tactic:
assumption
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
inr₁ inr₂ : veblenWith f o₂ a = veblenWith f o₂ a
⊢ veblenWith f o₁ a = a

Tactic:
rw [← h', 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
inl : veblenWith f 0 a ∈ range f
inr : ∀ (h : 0 < o), veblenWith f o a ∈ range f
⊢ veblenWith f o a ∈ range f

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
⊢ veblenWith f 0 a ∈ range f

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : 0 < o
inr : veblenWith f 0 (veblenWith f o a) ∈ range f
⊢ veblenWith f o a ∈ range f

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
h : 0 < o
⊢ veblenWith f 0 (veblenWith f o a) ∈ range f

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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))
rw₁ : ∀ (i : (↑(Iio (o + 1)) : Type (u + 1))), IsNormal (veblenWith f (↑i : Ordinal.{u}))
⊢ veblenWith f (o + 1) = deriv (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]

Premises used: Ordinal.isNormal_veblenWith, add_pos_of_right, LT.lt.ne', zero_lt_one, Ordinal.deriv_eq_enumOrd, Ordinal.veblenWith_of_ne_zero, Ordinal.derivFamily_eq_enumOrd
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
h :
  ⋂ (i : (↑(Iio (o + 1)) : Type (u + 1))), Function.fixedPoints (veblenWith f (↑i : Ordinal.{u})) =
    Function.fixedPoints (veblenWith f o)
⊢ enumOrd (⋂ (i : (↑(Iio (o + 1)) : Type (u + 1))), Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))) =
    enumOrd (Function.fixedPoints (veblenWith f o))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
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)
⊢ ⋂ (i : (↑(Iio (o + 1)) : Type (u + 1))), Function.fixedPoints (veblenWith f (↑i : Ordinal.{u})) =
    Function.fixedPoints (veblenWith f o)

Tactic:
ext a
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
h :
  (∀ (i : (↑(Iio (o + 1)) : Type (u + 1))), a ∈ Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))) ↔
    a ∈ Function.fixedPoints (veblenWith f o)
⊢ 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:
rw [mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
mpr :
  a ∈ Function.fixedPoints (veblenWith f o) →
    ∀ (i : (↑(Iio (o + 1)) : Type (u + 1))), a ∈ Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))
⊢ (∀ (i : (↑(Iio (o + 1)) : Type (u + 1))), a ∈ Function.fixedPoints (veblenWith f (↑i : Ordinal.{u}))) ↔
    a ∈ Function.fixedPoints (veblenWith f o)

Tactic:
use fun ha ↦ ha ⟨o, lt_succ o⟩
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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}))
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}))
⊢ 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

Premises used: Order.lt_succ_iff_eq_or_lt, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
mpr₁ mpr₂ : a = a
⊢ a ∈
    Function.fixedPoints
      (veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (b + 1)) b hb) : Ordinal.{u}))

Tactic:
rw [Function.mem_fixedPoints_iff, ha]

Premises used: Function.mem_fixedPoints_iff
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
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}))
⊢ a ∈
    Function.fixedPoints
      (veblenWith f (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (o + 1)) b hb_1) : Ordinal.{u}))

Tactic:
rw [← ha]
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
⊢ 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:
veblenWith_veblenWith_of_lt hf hb _

Premises used: Set.Mem, setOf, Function.fixedPoints, Ordinal.veblenWith_veblenWith_of_lt, Function.IsFixedPt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
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
⊢ 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:
exact veblenWith_veblenWith_of_lt hf hb _

Premises used: Ordinal.veblenWith_veblenWith_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ ∀ (i : (↑(Iio (o + 1)) : Type (u + 1))), IsNormal (veblenWith f (↑i : Ordinal.{u}))

Tactic:
fun o ↦ isNormal_veblenWith hf o.1

Premises used: Ordinal.isNormal_veblenWith, Subtype.val
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ ∀ (i : (↑(Iio (o + 1)) : Type (u + 1))), IsNormal (veblenWith f (↑i : Ordinal.{u}))

Tactic:
exact fun o ↦ isNormal_veblenWith hf o.1

Premises used: Ordinal.isNormal_veblenWith
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f 1 = deriv f

Tactic:
simpa using veblenWith_add_one hf 0

Premises used: Ordinal.veblenWith_add_one, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ veblenWith f (succ o) = deriv (veblenWith f o)

Tactic:
veblenWith_add_one hf o

Premises used: Order.succ, Ordinal.veblenWith_add_one
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ StrictMono (veblenWith f o)

Tactic:
(isNormal_veblenWith hf o).strictMono

Premises used: Ordinal.isNormal_veblenWith, Order.IsNormal.strictMono
-- 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_right_strictMono hf o).lt_iff_lt

Premises used: Ordinal.veblenWith_right_strictMono, StrictMono.lt_iff_lt
-- 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_right_strictMono hf o).le_iff_le

Premises used: Ordinal.veblenWith_right_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.SetTheory.Ordinal.Veblen
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ Function.Injective (veblenWith f o)

Tactic:
(veblenWith_right_strictMono hf o).injective

Premises used: Ordinal.veblenWith_right_strictMono, StrictMono.injective