awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
h : a < b
⊢ ∃ a_1 < b, a_1.toZFSet = a.toZFSet

Tactic:
⟨a, h, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
h : a < b
⊢ ∃ a_1 < b, a_1.toZFSet = a.toZFSet

Tactic:
exact ⟨a, h, rfl⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
h : a ≤ b
x : ZFSet.{u_1}
hx : x ∈ a.toZFSet
obtain : ∀ (c : Ordinal.{u_1}) (hc : c < a) (hx : c.toZFSet ∈ a.toZFSet), c.toZFSet ∈ b.toZFSet
⊢ x ∈ b.toZFSet

Tactic:
obtain ⟨c, hc, rfl⟩ := mem_toZFSet_iff.1 hx

Premises used: Ordinal.mem_toZFSet_iff, Iff.mp, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
h : a ≤ b
c : Ordinal.{u_1}
hc : c < a
hx : c.toZFSet ∈ a.toZFSet
⊢ c.toZFSet ∈ b.toZFSet

Tactic:
toZFSet_mem_toZFSet_of_lt (hc.trans_le h)

Premises used: _private.0.Ordinal.toZFSet_mem_toZFSet_of_lt, LT.lt.trans_le
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
h : a ≤ b
c : Ordinal.{u_1}
hc : c < a
hx : c.toZFSet ∈ a.toZFSet
⊢ c.toZFSet ∈ b.toZFSet

Tactic:
exact toZFSet_mem_toZFSet_of_lt (hc.trans_le h)

Premises used: _private.0.Ordinal.toZFSet_mem_toZFSet_of_lt, LT.lt.trans_le
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
⊢ a.toZFSet ∈ b.toZFSet ↔ a < b

Tactic:
⟨?_, toZFSet_mem_toZFSet_of_lt⟩

Premises used: _private.0.Ordinal.toZFSet_mem_toZFSet_of_lt, Iff.intro
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
refine : a.toZFSet ∈ b.toZFSet → a < b
⊢ a.toZFSet ∈ b.toZFSet ↔ a < b

Tactic:
refine ⟨?_, toZFSet_mem_toZFSet_of_lt⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
contrapose! : b ≤ a → a.toZFSet ∉ b.toZFSet
⊢ a.toZFSet ∈ b.toZFSet → a < b

Tactic:
contrapose!
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
⊢ b ≤ a → a.toZFSet ∉ b.toZFSet

Tactic:
fun h ↦ notMem_of_subset (toZFSet_monotone h)

Premises used: ZFSet.notMem_of_subset, Ordinal.toZFSet_monotone
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
⊢ b ≤ a → a.toZFSet ∉ b.toZFSet

Tactic:
exact fun h ↦ notMem_of_subset (toZFSet_monotone h)

Premises used: ZFSet.notMem_of_subset, Ordinal.toZFSet_monotone
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
⊢ a.toZFSet ⊆ b.toZFSet ↔ a ≤ b

Tactic:
⟨?_, fun h ↦ toZFSet_monotone h⟩

Premises used: Iff.intro, Ordinal.toZFSet_monotone
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
refine : a.toZFSet ⊆ b.toZFSet → a ≤ b
⊢ a.toZFSet ⊆ b.toZFSet ↔ a ≤ b

Tactic:
refine ⟨?_, fun h ↦ toZFSet_monotone h⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
contrapose! : b < a → ¬a.toZFSet ⊆ b.toZFSet
⊢ a.toZFSet ⊆ b.toZFSet → a ≤ b

Tactic:
contrapose!
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
⊢ b < a → ¬a.toZFSet ⊆ b.toZFSet

Tactic:
fun h ↦ not_subset_of_mem (toZFSet_mem_toZFSet_of_lt h)

Premises used: ZFSet.not_subset_of_mem, _private.0.Ordinal.toZFSet_mem_toZFSet_of_lt
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a b : Ordinal.{u_1}
⊢ b < a → ¬a.toZFSet ⊆ b.toZFSet

Tactic:
exact fun h ↦ not_subset_of_mem (toZFSet_mem_toZFSet_of_lt h)

Premises used: ZFSet.not_subset_of_mem, _private.0.Ordinal.toZFSet_mem_toZFSet_of_lt
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x x_1 : Ordinal.{u_1}
h : x < x_1
⊢ x.toZFSet < x_1.toZFSet

Tactic:
simpa [ssubset_iff_subset_not_subset] using ⟨h.le, h⟩

Premises used: ssubset_iff_subset_not_subset
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
⊢ Function.Injective toZFSet

Tactic:
toZFSet_strictMono.injective

Premises used: Ordinal.toZFSet_strictMono, StrictMono.injective
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a : ∀ (z : ZFSet.{u_1}), z ∈ toZFSet 0 ↔ Membership.mem (γ := ZFSet.{u_1}) ∅ z
⊢ toZFSet 0 = ∅

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
z : ZFSet.{u_1}
⊢ z ∈ toZFSet 0 ↔ Membership.mem (γ := ZFSet.{u_1}) ∅ z

Tactic:
simp [mem_toZFSet_iff]

Premises used: Ordinal.mem_toZFSet_iff
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ (o + 1).toZFSet = insert o.toZFSet o.toZFSet

Tactic:
aesop (add simp [mem_toZFSet_iff, le_iff_eq_or_lt])

Premises used: le_iff_eq_or_lt, Ordinal.mem_toZFSet_iff
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ (Order.succ o).toZFSet = insert o.toZFSet o.toZFSet

Tactic:
toZFSet_add_one o

Premises used: Order.succ, Ordinal.toZFSet_add_one
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ o.toZFSet.card = o.card

Tactic:
simpa [← coe_toZFSet, cardinalMk_coe_sort, Cardinal.mk_Iio_ordinal, ← lift_card] using
    Cardinal.mk_image_eq (s := Iio o) toZFSet_injective

Premises used: Ordinal.coe_toZFSet, Cardinal.mk_Iio_ordinal, Cardinal.mk_image_eq, Ordinal.toZFSet_injective, ZFSet.cardinalMk_coe_sort, Ordinal.lift_card
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
⊢ IsOrdinal.{u_1} o.toZFSet

Tactic:
⟨fun x hx y hy ↦ ?_, fun {z y x} hz hy hx ↦ ?_⟩

Premises used: ZFSet.IsOrdinal.mk
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
refine_1 : ∀ (x : ZFSet.{u_1}) (hx : x ∈ o.toZFSet) (y : ZFSet.{u_1}) (hy : y ∈ x), y ∈ o.toZFSet
refine_2 : ∀ {z y x : ZFSet.{u_1}} (hz : z ∈ y) (hy : y ∈ x) (hx : x ∈ o.toZFSet), z ∈ x
⊢ IsOrdinal.{u_1} o.toZFSet

Tactic:
refine ⟨fun x hx y hy ↦ ?_, fun {z y x} hz hy hx ↦ ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ∈ o.toZFSet
y : ZFSet.{u_1}
hy : y ∈ x
refine_1 : ∀ (a : Ordinal.{u_1}) (ha : a < o) (hx : a.toZFSet ∈ o.toZFSet) (hy : y ∈ a.toZFSet), y ∈ o.toZFSet
⊢ y ∈ o.toZFSet

Tactic:
obtain ⟨a, ha, rfl⟩ := mem_toZFSet_iff.1 hx

Premises used: Ordinal.mem_toZFSet_iff, Iff.mp, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
y : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
hy : y ∈ a.toZFSet
refine_1 : ∀ (b : Ordinal.{u_1}) (hb : b < a) (hy : b.toZFSet ∈ a.toZFSet), b.toZFSet ∈ o.toZFSet
⊢ y ∈ o.toZFSet

Tactic:
obtain ⟨b, hb, rfl⟩ := mem_toZFSet_iff.1 hy

Premises used: Ordinal.mem_toZFSet_iff, Iff.mp, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
z y x : ZFSet.{u_1}
hz : z ∈ y
hy : y ∈ x
hx : x ∈ o.toZFSet
refine_2 : ∀ (a : Ordinal.{u_1}) (ha : a < o) (hy : y ∈ a.toZFSet) (hx : a.toZFSet ∈ o.toZFSet), z ∈ a.toZFSet
⊢ z ∈ x

Tactic:
obtain ⟨a, ha, rfl⟩ := mem_toZFSet_iff.1 hx

Premises used: Ordinal.mem_toZFSet_iff, Iff.mp, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
z y : ZFSet.{u_1}
hz : z ∈ y
a : Ordinal.{u_1}
ha : a < o
hy : y ∈ a.toZFSet
hx : a.toZFSet ∈ o.toZFSet
refine_2 : ∀ (b : Ordinal.{u_1}) (hb : b < a) (hz : z ∈ b.toZFSet) (hy : b.toZFSet ∈ a.toZFSet), z ∈ a.toZFSet
⊢ z ∈ a.toZFSet

Tactic:
obtain ⟨b, hb, rfl⟩ := mem_toZFSet_iff.1 hy

Premises used: Ordinal.mem_toZFSet_iff, Iff.mp, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hy : b.toZFSet ∈ a.toZFSet
⊢ b.toZFSet ∈ o.toZFSet

Tactic:
toZFSet_mem_toZFSet_iff.2 (hb.trans ha)

Premises used: Iff.mpr, LT.lt.trans, Ordinal.toZFSet_mem_toZFSet_iff
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hy : b.toZFSet ∈ a.toZFSet
⊢ b.toZFSet ∈ o.toZFSet

Tactic:
exact toZFSet_mem_toZFSet_iff.2 (hb.trans ha)

Premises used: Iff.mpr, LT.lt.trans, Ordinal.toZFSet_mem_toZFSet_iff
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o : Ordinal.{u_1}
z : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hz : z ∈ b.toZFSet
hy : b.toZFSet ∈ a.toZFSet
refine_2 : ∀ (c : Ordinal.{u_1}) (hc : c < b) (hz : c.toZFSet ∈ b.toZFSet), c.toZFSet ∈ a.toZFSet
⊢ z ∈ a.toZFSet

Tactic:
obtain ⟨c, hc, rfl⟩ := mem_toZFSet_iff.1 hz

Premises used: Ordinal.mem_toZFSet_iff, Iff.mp, rfl
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hy : b.toZFSet ∈ a.toZFSet
c : Ordinal.{u_1}
hc : c < b
hz : c.toZFSet ∈ b.toZFSet
⊢ c.toZFSet ∈ a.toZFSet

Tactic:
toZFSet_mem_toZFSet_iff.2 (hc.trans hb)

Premises used: Iff.mpr, LT.lt.trans, Ordinal.toZFSet_mem_toZFSet_iff
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
o a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hy : b.toZFSet ∈ a.toZFSet
c : Ordinal.{u_1}
hc : c < b
hz : c.toZFSet ∈ b.toZFSet
⊢ c.toZFSet ∈ a.toZFSet

Tactic:
exact toZFSet_mem_toZFSet_iff.2 (hc.trans hb)

Premises used: Iff.mpr, LT.lt.trans, Ordinal.toZFSet_mem_toZFSet_iff
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u_1}
hx : x.IsOrdinal
⊢ x.rank.toZFSet = x

Tactic:
(IsOrdinal.rank_inj (isOrdinal_toZFSet _) hx).1 (rank_toZFSet _)

Premises used: ZFSet.isOrdinal_toZFSet, Ordinal.rank_toZFSet, Iff.mp, ZFSet.IsOrdinal.rank_inj
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
⊢ x.IsOrdinal ↔ x ∈ Set.range toZFSet

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
refine_1 : ∀ (h : x.IsOrdinal), x ∈ Set.range toZFSet
refine_2 : x ∈ Set.range toZFSet → x.IsOrdinal
⊢ x.IsOrdinal ↔ x ∈ Set.range toZFSet

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsOrdinal
refine_1 : x.rank.toZFSet ∈ Set.range toZFSet
⊢ x ∈ Set.range toZFSet

Tactic:
rw [← h.toZFSet_rank_eq]

Premises used: ZFSet.IsOrdinal.toZFSet_rank_eq
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsOrdinal
⊢ x.rank.toZFSet ∈ Set.range toZFSet

Tactic:
Set.mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x : ZFSet.{u}
h : x.IsOrdinal
⊢ x.rank.toZFSet ∈ Set.range toZFSet

Tactic:
exact Set.mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a : Ordinal.{u}
⊢ IsOrdinal.{u} a.toZFSet

Tactic:
isOrdinal_toZFSet a

Premises used: ZFSet.isOrdinal_toZFSet
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
a : Ordinal.{u}
⊢ IsOrdinal.{u} a.toZFSet

Tactic:
exact isOrdinal_toZFSet a

Premises used: ZFSet.isOrdinal_toZFSet
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x_1 y z w : ZFSet.{u}
x_2 : { x : ZFSet.{u_1} // x.IsOrdinal }
x : ZFSet.{u_1}
hx : x.IsOrdinal
⊢ (fun (o : Ordinal.{u_1}) ↦ Subtype.mk (p := fun (x : ZFSet.{u_1}) ↦ x.IsOrdinal) o.toZFSet ⋯)
      ((fun (x : { x : ZFSet.{u_1} // x.IsOrdinal }) ↦ rank.{u_1} (↑x : ZFSet.{u_1}))
        (Subtype.mk (p := fun (x : ZFSet.{u_1}) ↦ x.IsOrdinal) x hx)) =
    Subtype.mk (p := fun (x : ZFSet.{u_1}) ↦ x.IsOrdinal) x hx

Tactic:
simpa using hx.toZFSet_rank_eq

Premises used: ZFSet.IsOrdinal.toZFSet_rank_eq
-- Module: Mathlib.SetTheory.ZFC.Ordinal
Goal:
x y z w : ZFSet.{u}
a b : Ordinal.{u_1}
⊢ LE.le (α := { x : ZFSet.{u_1} // x.IsOrdinal })
      (({ toFun := fun (o : Ordinal.{u_1}) ↦ Subtype.mk (p := fun (x : ZFSet.{u_1}) ↦ x.IsOrdinal) o.toZFSet ⋯,
              invFun := fun (x : { x : ZFSet.{u_1} // x.IsOrdinal }) ↦ (↑x : ZFSet.{u_1}).rank, left_inv := ⋯,
              right_inv := ⋯ } :
            (a : Ordinal.{u_1}) → { x : ZFSet.{u_1} // x.IsOrdinal })
          a :
        { x : ZFSet.{u_1} // x.IsOrdinal })
      (({ toFun := fun (o : Ordinal.{u_1}) ↦ Subtype.mk (p := fun (x : ZFSet.{u_1}) ↦ x.IsOrdinal) o.toZFSet ⋯,
              invFun := fun (x : { x : ZFSet.{u_1} // x.IsOrdinal }) ↦ (↑x : ZFSet.{u_1}).rank, left_inv := ⋯,
              right_inv := ⋯ } :
            (a : Ordinal.{u_1}) → { x : ZFSet.{u_1} // x.IsOrdinal })
          b :
        { x : ZFSet.{u_1} // x.IsOrdinal }) ↔
    a ≤ b

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
α : Type u_1
A : α → PSet.{u_1}
⊢ (mk α A).Type = α

Tactic:
rfl

Premises used: rfl, PSet.Type
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
α : Type u_1
A : α → PSet.{u_1}
⊢ (mk α A).Func = A

Tactic:
rfl

Premises used: PSet.Func, rfl
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
y : PSet.{u_2}
h : x.Equiv y
⊢ ∀ (i : x.Type), ∃ (j : y.Type), Equiv.{u_1, u_2} (x.Func i) (y.Func j)

Tactic:
(equiv_iff.1 h).1

Premises used: PSet.equiv_iff, And.left, Iff.mp
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
y : PSet.{u_2}
h : x.Equiv y
⊢ ∀ (j : y.Type), ∃ (i : x.Type), Equiv.{u_1, u_2} (x.Func i) (y.Func j)

Tactic:
(equiv_iff.1 h).2

Premises used: PSet.equiv_iff, And.right, Iff.mp
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
⊢ x.Equiv x

Tactic:
Equiv.refl x

Premises used: PSet.Equiv.refl
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
y : PSet.{u_2}
⊢ x.Equiv y → y.Equiv x

Tactic:
(Equiv.refl y).euc

Premises used: PSet.Equiv.euc, PSet.Equiv.refl
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
y : PSet.{u_2}
⊢ x.Equiv y ↔ y.Equiv x

Tactic:
⟨Equiv.symm, Equiv.symm⟩

Premises used: PSet.Equiv.symm, Iff.intro
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
y : PSet.{u_2}
z : PSet.{u_3}
h1 : x.Equiv y
h2 : y.Equiv z
⊢ x.Equiv z

Tactic:
h1.euc h2.symm

Premises used: PSet.Equiv.euc, PSet.Equiv.symm
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
y : PSet.{u_2}
inst : IsEmpty.{u_1 + 1} x.Type
inst_1 : IsEmpty.{u_2 + 1} y.Type
⊢ (∀ (i : x.Type), ∃ (j : y.Type), Equiv.{u_1, u_2} (x.Func i) (y.Func j)) ∧
    ∀ (j : y.Type), ∃ (i : x.Type), Equiv.{u_1, u_2} (x.Func i) (y.Func j)

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
⊢ Std.Refl fun (x1 x2 : PSet.{u_1}) ↦ x1 ⊆ x2

Tactic:
⟨fun _ a => ⟨a, Equiv.refl _⟩⟩

Premises used: PSet.Equiv.refl, PSet.Func, Std.Refl.mk, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y z : PSet.{u_1}
hxy : x ⊆ y
hyz : y ⊆ z
a : x.Type
obtain :
  ∀ (b : y.Type) (hb : Equiv.{u_1, u_1} (x.Func a) (y.Func b)), ∃ (b : z.Type), Equiv.{u_1, u_1} (x.Func a) (z.Func b)
⊢ ∃ (b : z.Type), Equiv.{u_1, u_1} (x.Func a) (z.Func b)

Tactic:
obtain ⟨b, hb⟩ := hxy a
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y z : PSet.{u_1}
hxy : x ⊆ y
hyz : y ⊆ z
a : x.Type
b : y.Type
hb : Equiv.{u_1, u_1} (x.Func a) (y.Func b)
obtain :
  ∀ (c : z.Type) (hc : Equiv.{u_1, u_1} (y.Func b) (z.Func c)), ∃ (b : z.Type), Equiv.{u_1, u_1} (x.Func a) (z.Func b)
⊢ ∃ (b : z.Type), Equiv.{u_1, u_1} (x.Func a) (z.Func b)

Tactic:
obtain ⟨c, hc⟩ := hyz b
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y z : PSet.{u_1}
hxy : x ⊆ y
hyz : y ⊆ z
a : x.Type
b : y.Type
hb : Equiv.{u_1, u_1} (x.Func a) (y.Func b)
c : z.Type
hc : Equiv.{u_1, u_1} (y.Func b) (z.Func c)
⊢ ∃ (b : z.Type), Equiv.{u_1, u_1} (x.Func a) (z.Func b)

Tactic:
⟨c, hb.trans hc⟩

Premises used: PSet.Equiv.trans, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y z : PSet.{u_1}
hxy : x ⊆ y
hyz : y ⊆ z
a : x.Type
b : y.Type
hb : Equiv.{u_1, u_1} (x.Func a) (y.Func b)
c : z.Type
hc : Equiv.{u_1, u_1} (y.Func b) (z.Func c)
⊢ ∃ (b : z.Type), Equiv.{u_1, u_1} (x.Func a) (z.Func b)

Tactic:
exact ⟨c, hb.trans hc⟩
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y : PSet.{u_1}
⊢ x ≤ y ↔ x ⊆ y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y : PSet.{u_1}
⊢ x < y ↔ x ⊂ y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
⊢ IsNonstrictStrictOrder PSet.{u_1} (fun (x1 x2 : PSet.{u_1}) ↦ x1 ⊆ x2) fun (x1 x2 : PSet.{u_1}) ↦ x1 ⊂ x2

Tactic:
⟨fun _ _ ↦ Iff.rfl⟩

Premises used: Iff.rfl, IsNonstrictStrictOrder.mk
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y : PSet.{u_1}
⊢ x ∈ y ↔ ∃ (b : y.Type), x.Equiv (y.Func b)

Tactic:
Iff.rfl

Premises used: PSet.Mem, Iff.rfl
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
α : Type u
A : α → PSet.{u}
a : α
⊢ A a ∈ PSet.mk α A

Tactic:
⟨a, Equiv.refl (A a)⟩

Premises used: PSet.Mem, PSet.Equiv.refl, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
i : x.Type
⊢ x.Func i ∈ x

Tactic:
Mem.mk _ _

Premises used: PSet.Mem, PSet.Func, PSet.Mem.mk, PSet.Type
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y : PSet.{u}
⊢ x.Equiv y ↔ ∀ {w : PSet.{u}}, w ∈ x ↔ w ∈ y

Tactic:
⟨Mem.congr_right,
    match x, y with
    | ⟨_, A⟩, ⟨_, B⟩ => fun h =>
      ⟨fun a => h.1 (Mem.mk A a), fun b =>
        let ⟨a, h⟩ := h.2 (Mem.mk B b)
        ⟨a, h.symm⟩⟩⟩

Premises used: Iff.mpr, _private.0.PSet.Mem.ext.match_1, Exists, PSet.Mem.mk, PSet.Mem.congr_right, PSet.Equiv.symm, And.intro, Iff.intro, Exists.intro, Iff.mp, _private.0.PSet.Equiv.ext.match_5, PSet.Equiv
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y : PSet.{u_1}
⊢ x ⊆ y ↔ ∀ ⦃z : PSet.{u_1}⦄, z ∈ x → z ∈ y

Tactic:
⟨fun h _ => mem_of_subset h, fun h a => h (Mem.mk _ a)⟩

Premises used: PSet.mem_of_subset, PSet.Func, PSet.Mem.mk, Iff.intro
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : Equiv.{u, u} (mk α A) (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : Equiv.{u, u} (mk γ C) ((mk β B).Func b)
obtain :
  ∀ (a : (mk α A).Type) (ha : Equiv.{u, u} ((mk α A).Func a) ((mk β B).Func b)),
    Acc (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) (mk γ C)
⊢ Acc (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) (mk γ C)

Tactic:
obtain ⟨a, ha⟩ := H.exists_right b

Premises used: PSet.Equiv.exists_right
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : Equiv.{u, u} (mk α A) (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : Equiv.{u, u} (mk γ C) ((mk β B).Func b)
a : (mk α A).Type
ha : Equiv.{u, u} ((mk α A).Func a) ((mk β B).Func b)
⊢ Equiv.{u, u} ((mk α A).Func a) (mk γ C)

Tactic:
have H := ha.trans hc.symm
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H_1 : Equiv.{u, u} (mk α A) (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : Equiv.{u, u} (mk γ C) ((mk β B).Func b)
a : (mk α A).Type
ha : Equiv.{u, u} ((mk α A).Func a) ((mk β B).Func b)
H : Equiv.{u, u} ((mk α A).Func a) (mk γ C)
⊢ Equiv.{u, u} (A a) (mk γ C)

Tactic:
rw [mk_func] at H

Premises used: PSet.mk_func
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H_1 : Equiv.{u, u} (mk α A) (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : Equiv.{u, u} (mk γ C) ((mk β B).Func b)
a : (mk α A).Type
ha : Equiv.{u, u} ((mk α A).Func a) ((mk β B).Func b)
H : Equiv.{u, u} (A a) (mk γ C)
⊢ Acc (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) (mk γ C)

Tactic:
mem_wf_aux H
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H_1 : Equiv.{u, u} (mk α A) (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : Equiv.{u, u} (mk γ C) ((mk β B).Func b)
a : (mk α A).Type
ha : Equiv.{u, u} ((mk α A).Func a) ((mk β B).Func b)
H : Equiv.{u, u} (A a) (mk γ C)
⊢ Acc (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) (mk γ C)

Tactic:
exact mem_wf_aux H
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
⊢ WellFounded fun (x1 x2 : PSet.{u_1}) ↦ x1 ∈ x2

Tactic:
⟨fun x => mem_wf_aux <| Equiv.refl x⟩

Premises used: PSet.Equiv.refl, WellFounded.intro, _private.0.PSet.mem_wf_aux
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
⊢ IsWellFounded PSet.{u_1} fun (x1 x2 : PSet.{u_1}) ↦ x1 ∈ x2

Tactic:
⟨mem_wf⟩

Premises used: PSet.mem_wf, IsWellFounded.mk
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y : PSet.{u_1}
⊢ x ∈ y → y ∉ x

Tactic:
asymm_of (· ∈ ·)

Premises used: asymm_of, Membership.mem
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
⊢ x ∉ x

Tactic:
irrefl_of (· ∈ ·) x

Premises used: irrefl_of, Membership.mem
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y : PSet.{u_1}
h : x ∈ y
⊢ ¬y ⊆ x

Tactic:
fun h' ↦ mem_irrefl _ <| mem_of_subset h' h

Premises used: PSet.mem_of_subset, PSet.mem_irrefl, Not
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y : PSet.{u_1}
h : x ⊆ y
⊢ y ∉ x

Tactic:
imp_not_comm.2 not_subset_of_mem h

Premises used: Iff.mpr, PSet.not_subset_of_mem, imp_not_comm
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
a u : PSet.{u}
⊢ a ∈ u.toSet ↔ a ∈ u

Tactic:
Iff.rfl

Premises used: PSet.Mem, Set.Mem, Iff.rfl, setOf, PSet.toSet
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
u : PSet.{u_1}
⊢ u.Nonempty ↔ ∃ (x : PSet.{u_1}), x ∈ u

Tactic:
Iff.rfl

Premises used: PSet.Mem, PSet.Nonempty, Set.Mem, Iff.rfl, setOf, PSet.toSet, Set.Nonempty
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x u : PSet.{u_1}
h : x ∈ u
⊢ u.Nonempty

Tactic:
⟨x, h⟩

Premises used: PSet.Nonempty, Set.Nonempty, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
u : PSet.{u_1}
⊢ u.toSet.Nonempty ↔ u.Nonempty

Tactic:
Iff.rfl

Premises used: PSet.Nonempty, Iff.rfl
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
⊢ Nonempty.{u_1 + 1} x.Type ↔ x.Nonempty

Tactic:
⟨fun ⟨i⟩ => ⟨_, func_mem _ i⟩, fun ⟨_, j, _⟩ => ⟨j⟩⟩

Premises used: PSet.Nonempty, PSet.Func, Nonempty.intro, PSet.func_mem, _private.0.PSet.nonempty_type_iff_nonempty.match_2, _private.0.PSet.nonempty_type_iff_nonempty.match_1, Iff.intro, Exists.intro, Nonempty, PSet.Type
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
h : Nonempty.{u_1 + 1} x.Type
⊢ x.Nonempty

Tactic:
nonempty_type_iff_nonempty.1 h

Premises used: Iff.mp, PSet.nonempty_type_iff_nonempty
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y : PSet.{u_1}
⊢ x.Equiv y ↔ x.toSet = y.toSet

Tactic:
equiv_iff_mem.trans <| .symm Set.ext_iff

Premises used: PSet.equiv_iff_mem, Iff.trans, Set.ext_iff, Iff.symm
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
⊢ IsEmpty.{u_1 + 1} («Type» ∅)

Tactic:
⟨PEmpty.elim⟩

Premises used: PEmpty.elim, IsEmpty.mk
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
⊢ ∅ = mk PEmpty PEmpty.elim

Tactic:
simp [EmptyCollection.emptyCollection, PSet.empty]

Premises used: PSet.empty, EmptyCollection.emptyCollection
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u}
⊢ x ∉ ∅

Tactic:
IsEmpty.exists_iff.1

Premises used: PSet.Mem, IsEmpty.exists_iff, Iff.mp, Not
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
⊢ toSet ∅ = ∅

Tactic:
simp [toSet]

Premises used: PSet.toSet
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u}
⊢ ∅ ⊆ x

Tactic:
fun x => x.elim

Premises used: PEmpty.elim, PSet.Subset
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
⊢ ¬PSet.Nonempty.{u_1} ∅

Tactic:
simp [PSet.Nonempty]

Premises used: PSet.Nonempty
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u_1}
inst : IsEmpty.{u_1 + 1} x.Type
⊢ Equiv.{u_1, u_2} x ∅

Tactic:
PSet.equiv_of_isEmpty x _

Premises used: PSet.equiv_of_isEmpty
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
⊢ LawfulSingleton PSet.{u_1} PSet.{u_1}

Tactic:
⟨fun _ => rfl⟩

Premises used: LawfulSingleton.mk, rfl
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y : PSet.{u_1}
⊢ x ∈ insert x y

Tactic:
mem_insert_iff.2 <| Or.inl Equiv.rfl

Premises used: Iff.mpr, PSet.Equiv.rfl, Or.inl, PSet.mem_insert_iff
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
y z x : PSet.{u_1}
h : z ∈ y
⊢ z ∈ insert x y

Tactic:
mem_insert_iff.2 <| Or.inr h

Premises used: Iff.mpr, PSet.mem_insert_iff, Or.inr
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y : PSet.{u_1}
⊢ Membership.mem (γ := PSet.{u_1}) {y} x ↔ x.Equiv y

Tactic:
mem_insert_iff.trans
    ⟨fun o => Or.rec id (fun n => absurd n (notMem_empty _)) o, Or.inl⟩

Premises used: Or.rec, Iff.intro, Iff.trans, Or.inl, PSet.mem_insert_iff
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x y z : PSet.{u_1}
⊢ Membership.mem (γ := PSet.{u_1}) {y, z} x ↔ x.Equiv y ∨ x.Equiv z

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
α : Type u
A : α → PSet.{u}
y : PSet.{u}
h : 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
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : (A a).Func c ∈ A a), (A a).Func c ∈ A a
⊢ (A a).Func c ∈ A a

Tactic:
rwa [eta] at this

Premises used: PSet.eta
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
α : Type u
A : α → PSet.{u}
y : PSet.{u}
h : ∃ z ∈ mk α A, y ∈ z
β : Type u
B : β → PSet.{u}
a : (mk α A).Type
e : Equiv.{u, u} (mk β B) (A a)
b : (mk β B).Type
yb : y.Equiv ((mk β B).Func b)
rw :
  ∀ (e : Equiv.{u, u} (mk β B) (mk (A a).Type (A a).Func)) (b : (mk β B).Type) (yb : y.Equiv ((mk β B).Func b)),
    y ∈ ⋃₀ mk α A
⊢ y ∈ ⋃₀ mk α A

Tactic:
rw [← eta (A a)] at e

Premises used: PSet.eta