mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: a : Ordinal.{u}
s : Set Ordinal.{u}
⊢ [a ∈ closure s, a ∈ closure (s ∩ Iic a), (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a,
      ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a, ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
b₁ b₂ : Ordinal.{0}
bb : b₁ ≤ b₂
h : o.NFBelow b₁
⊢ o.NFBelow b₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ a ∈ closure s ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' : Ordinal.{0}
h : (e.oadd n a).NFBelow b'
⊢ (e.oadd n a).NFBelow b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ NF 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
⊢ a ∈ s ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ e.oadd n₁ o₁ < e.oadd n₂ o₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ e.oadd n a₁ < e.oadd n a₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
ι : Type u
w✝ : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ type WellOrderingRel ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s
⊢ Nonempty o.ToType

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ a ∈ closure s ↔ ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hb : ∀ (e' : Ordinal.{u_1}), f e' < b
he : ∀ e' ∈ f.support, e' < e
⊢ eval b f < b ^ e

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
⊢ a ∈ s ↔ ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
⊢ IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ eval b (coeff b o) = o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
⊢ IsClosed s ↔
    ∀ {o : Ordinal.{u}},
      o ≠ 0 →
        ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i ↦ (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
this : enumOrd s (⨆ i, g i) = ⨆ i, f i
⊢ ⨆ i, f i ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i ↦ (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
⊢ enumOrd s (⨆ i, g i) = ⨆ i, f i

Tactic:
rw [h.map_iSup bddAbove_of_small]

Goal state after:
case refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i ↦ (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
⊢ ⨆ i, enumOrd s (g i) = ⨆ i, f i
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
e' : Ordinal.{u_1}
⊢ f e' < b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ IsNormal (enumOrd s) ↔ IsClosed s

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ o.IsAcc S ↔ o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
apply SuccOrder.accPt_principal.trans

Goal state after:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ (¬IsMin o ∧ ∀ b < o, (S ∩ Ioo b o).Nonempty) ↔ o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ o.IsAcc S ↔ o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
⊢ AccPt p (𝓟 S) ↔ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsClosedBelow S o ↔ ∀ p < o, p.IsAcc S → p ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
⊢ IsClosedBelow (⋂₀ S) o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
⊢ coeff b (eval b (single e x + f)) = single e x + f

Tactic:
have IH' (e') : f e' < b := by
      by_cases he' : e' ∈ f.support
      · apply (hf e').trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        exact (hf' _ he').ne
      · rw [notMem_support_iff.1 he']
        exact hb.pos
    rw [eval_single_add' _ hf', coeff_opow_mul_add hb hx, IH IH']
    · apply (hf e).trans_eq'
      rw [add_apply, single_eq_same, notMem_support_iff.1, add_zero]
      exact fun h ↦ (hf' _ h).false
    · exact eval_lt IH' hf'

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b : Ordinal.{u_1}
hb : 1 < b
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ (e : Ordinal.{u_1}), f e < b
⊢ coeff b (eval b f) = f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: x : PSet.{u_1}
y : PSet.{u_2}
inst✝¹ : IsEmpty x.Type
inst✝ : IsEmpty y.Type
⊢ (∀ (i : x.Type), ∃ j, (x.Func i).Equiv (y.Func j)) ∧ ∀ (j : y.Type), ∃ i, (x.Func i).Equiv (y.Func j)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: x y z : PSet.{?u.3}
hxy : x ⊆ y
hyz : y ⊆ z
a : x.Type
⊢ ∃ b, (x.Func a).Equiv (z.Func b)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : (mk α A).Equiv (mk β B)
⊢ ∀ y ∈ mk β B, Acc (fun x1 x2 ↦ x1 ∈ x2) y

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: ⊢ ∅ = mk PEmpty PEmpty.elim

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: ⊢ ∅.toSet = ∅

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: ⊢ ¬∅.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: x y z : PSet.{u_1}
⊢ x ∈ {y, z} ↔ x.Equiv y ∨ x.Equiv z

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: α : Type u
A : α → PSet.{u}
y : PSet.{u}
x✝ : y ∈ ⋃₀ mk α A
a : (mk α A).Type
c : ((mk α A).Func a).Type
e : y.Equiv ((A a).Func c)
this : (A a).Func c ∈ mk (A a).Type (A a).Func
⊢ (A a).Func c ∈ A (?m.126 α A y x✝ a c e this)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: α : Type u
A : α → PSet.{u}
y : PSet.{u}
x✝ : ∃ z ∈ mk α A, y ∈ z
β : Type u
B : β → PSet.{u}
a : (mk α A).Type
e : (mk β B).Equiv (A a)
b : (mk β B).Type
yb : y.Equiv ((mk β B).Func b)
⊢ y ∈ ⋃₀ mk α A

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: x : PSet.{u}
⊢ (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
⊢ FormallySmooth R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
R' : Type u_3
S' : Type u_4
inst✝¹ : CommRing R'
inst✝ : CommRing S'
f : R →+* S
flat : f.Flat
qR : R →+* R'
qS : S →+* S'
g : R' →+* S'
surjR : Function.Surjective ⇑qR
surjS : Function.Surjective ⇑qS
comm : qS.comp f = g.comp qR
sq0 : ker qR ^ 2 = ⊥
eqmap : ker qS = Ideal.map f (ker qR)
smoothq : g.FormallySmooth
⊢ f.FormallySmooth

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
⊢ ((namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).cmp (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)).Compares
    (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹) (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h✝ : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
h : e.oadd n a = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ ω ∣ (e.oadd n a).repr → e.repr ≠ 0 ∧ ω ∣ a.repr

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: 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
⊢ out f xs ≈ out f ys

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x : ZFSet.{u}
⊢ #↥x = lift.{u + 1, u} x.card

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x y : ZFSet.{u}
h : x ⊆ y
⊢ x.card ≤ y.card

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: ⊢ ∅.card = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x y : ZFSet.{u}
⊢ (insert x y).card ≤ y.card + 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x y : ZFSet.{u}
h : x ∉ y
⊢ (insert x y).card = y.card + 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x : ZFSet.{u}
⊢ {x}.card = 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x y : ZFSet.{u}
h : x ≠ y
⊢ {x, y}.card = 2

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x y : ZFSet.{u}
⊢ (x ∪ y).card ≤ x.card + y.card

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ DecidableRel TopBelow

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x : ZFSet.{u}
⊢ x.powerset.card = 2 ^ x.card

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ veblenWith f 0 = f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
⊢ Decidable (e.oadd n a).NF

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x : ZFSet.{u}
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
⊢ (image f x).card ≤ x.card

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ veblenWith f o = derivFamily fun x ↦ veblenWith f ↑x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x✝ y✝ z x y : ZFSet.{u}
hxy : x.toSet = y.toSet
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (veblenWith f o)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x✝ y z x : ZFSet.{u}
a : PSet.{u}
f : a.Type → ↥(mk a) := fun i ↦ ⟨mk (a.Func i), ⋯⟩
this : Function.Surjective f
⊢ Small.{u, u + 1} ↥(⟦a⟧)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{u, v} (range f).card ≤ lift.{v, u} #α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ ⨆ i, (f i).card ≤ (⋃ (i : α), f i).card

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ IsNormal (veblenWith f o)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x✝ y z x : ZFSet.{u}
a : PSet.{u}
⊢ Small.{u, u + 1} ↥(⟦a⟧)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: ⊢ ↑∅ = ∅

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: ⊢ ¬∅.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : PSet.{u_1}
⊢ (mk x).Nonempty ↔ x.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : ZFSet.{u}
⊢ x = ∅ ↔ ∀ (y : ZFSet.{u}), y ∉ x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{u, v} (⋃ (i : α), f i).card ≤ sum fun i ↦ (f i).card

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
⊢ a ∈ range (veblenWith f o) ↔ ∀ b < o, veblenWith f b a = a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: u : ZFSet.{u_1}
⊢ u = ∅ ∨ u.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u_1}
⊢ ↑(insert x y) = insert x ↑y

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
a : Ordinal.{u}
⊢ veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : ZFSet.{u_1}
⊢ ↑{x} = {x}

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y z : ZFSet.{u}
⊢ x ∈ {y, z} ↔ x = y ∨ x = z

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : ZFSet.{u_1}
⊢ {x, x} = {x}

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y z : ZFSet.{u_1}
⊢ {x, y} = {z} ↔ x = z ∧ y = z

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y z : ZFSet.{u_1}
⊢ {x} = {y, z} ↔ x = y ∧ x = z

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h : o₁ ≤ o₂
h' : veblenWith f o₂ a = a
⊢ veblenWith f o₁ a = a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o a ∈ range f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y z : ZFSet.{u}
p : ZFSet.{?u.28} → Prop
x✝³ x✝² : PSet.{?u.28}
α : Type ?u.28
A : α → PSet.{?u.28}
β : Type ?u.28
B : β → PSet.{?u.28}
x✝¹ : PSet.mk α A ≈ PSet.mk β B
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
βα : ∀ (b : β), ∃ a, (A a).Equiv (B b)
x✝ : { a // (fun y ↦ p (mk y)) ((PSet.mk α A).Func a) }
a : (PSet.mk α A).Type
pa : (fun y ↦ p (mk y)) ((PSet.mk α A).Func a)
b : β
hb : (A a).Equiv (B b)
⊢ (fun y ↦ p (mk y)) ((PSet.mk β B).Func b)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y z : ZFSet.{u}
p : ZFSet.{?u.28} → Prop
x✝³ x✝² : PSet.{?u.28}
α : Type ?u.28
A : α → PSet.{?u.28}
β : Type ?u.28
B : β → PSet.{?u.28}
x✝¹ : PSet.mk α A ≈ PSet.mk β B
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
βα : ∀ (b : β), ∃ a, (A a).Equiv (B b)
x✝ : { a // (fun y ↦ p (mk y)) ((PSet.mk β B).Func a) }
b : (PSet.mk β B).Type
pb : (fun y ↦ p (mk y)) ((PSet.mk β B).Func b)
a : α
ha : (A a).Equiv (B b)
⊢ (fun y ↦ p (mk y)) ((PSet.mk α A).Func a)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
⊢ ↑(ZFSet.sep p a) = {x | x ∈ a ∧ p x}

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ (e.oadd n a + o).NFBelow b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
x✝¹ : NF 0
x✝ : o.NF
⊢ (0 + o).repr = repr 0 + o.repr

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ veblenWith f (o + 1) = deriv (veblenWith f o)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f 1 = deriv f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a : Ordinal.{u}
⊢ Monotone fun x ↦ veblenWith f x a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ 0 < veblenWith f o a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: case mk.mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : (A a).Equiv (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
rw [ea, eb] at hb

Goal state after:
case mk.mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
hb : (PSet.mk γ Γ).Equiv (PSet.mk δ Δ)
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ StrictMono fun x ↦ veblenWith f x 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c✝ : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
c : (A a).Type := c✝
⊢ γ

Tactic:
by

Goal state after: