awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c_1 : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ (a : γ), PSet.Equiv.{u, u} (Γ a) (Δ b)
c : (A a).Type := c_1
mk :
  ∀ (d : δ) (hd : PSet.Equiv.{u, u} (Γ (Eq.mp ⋯ c)) (Δ d)),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
      ((⋃₀ PSet.mk β B).Func b)

Tactic:
let ⟨d, hd⟩ := γδ (by rwa [ea] at c)
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c_1 : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ (a : γ), PSet.Equiv.{u, u} (Γ a) (Δ b)
c : (A a).Type := c_1
d : δ
hd : PSet.Equiv.{u, u} (Γ (Eq.mp ⋯ c)) (Δ d)
h :
  PSet.Equiv.{u, u}
    ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
    ((⋃₀ PSet.mk β B).Func
      (Sigma.mk (β := fun (x : (PSet.mk β B).Type) ↦ ((PSet.mk β B).Func x).Type) b (Eq.ndrec (motive := «Type») d ⋯)))
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
      ((⋃₀ PSet.mk β B).Func b)

Tactic:
use ⟨b, Eq.ndrec d (Eq.symm eb)⟩
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c_1 : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ (a : γ), PSet.Equiv.{u, u} (Γ a) (Δ b)
c : (A a).Type := c_1
d : δ
hd : PSet.Equiv.{u, u} (Γ (Eq.mp ⋯ c)) (Δ d)
h : PSet.Equiv.{u, u} ((A a).Func c) ((B b).Func (Eq.ndrec (motive := «Type») d ⋯))
⊢ PSet.Equiv.{u, u}
    ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
    ((⋃₀ PSet.mk β B).Func
      (Sigma.mk (β := fun (x : (PSet.mk β B).Type) ↦ ((PSet.mk β B).Func x).Type) b (Eq.ndrec (motive := «Type») d ⋯)))

Tactic:
change PSet.Equiv ((A a).Func c) ((B b).Func (Eq.ndrec d eb.symm))

Premises used: PSet.Func, Eq.ndrec, Eq.symm, PSet.Equiv
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c_1 : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ (a : γ), PSet.Equiv.{u, u} (Γ a) (Δ b)
c : (A a).Type := c_1
d : δ
hd_1 : PSet.Equiv.{u, u} (Γ (Eq.mp ⋯ c)) (Δ d)
x : (PSet.mk γ Γ).Type
x_1 : δ
hd : PSet.Equiv.{u, u} (Γ (Eq.mp ⋯ x)) (Δ x_1)
⊢ PSet.Equiv.{u, u} ((PSet.mk γ Γ).Func x) ((PSet.mk δ Δ).Func (Eq.ndrec (motive := «Type») x_1 ⋯))

Tactic:
hd

Premises used: PSet.Func, Eq.mp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c_1 : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ (a : γ), PSet.Equiv.{u, u} (Γ a) (Δ b)
c : (A a).Type := c_1
d : δ
hd_1 : PSet.Equiv.{u, u} (Γ (Eq.mp ⋯ c)) (Δ d)
x : (PSet.mk γ Γ).Type
x_1 : δ
hd : PSet.Equiv.{u, u} (Γ (Eq.mp ⋯ x)) (Δ x_1)
⊢ PSet.Equiv.{u, u} ((PSet.mk γ Γ).Func x) ((PSet.mk δ Δ).Func (Eq.ndrec (motive := «Type») x_1 ⋯))

Tactic:
exact hd
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c_1 : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ (a : γ), PSet.Equiv.{u, u} (Γ a) (Δ b)
c : (A a).Type := c_1
d : δ
hd : PSet.Equiv.{u, u} (Γ (Eq.mp ⋯ c)) (Δ d)
⊢ PSet.Equiv.{u, u} ((A a).Func c) ((B b).Func (Eq.ndrec (motive := «Type») d ⋯))

Tactic:
match A a, B b, ea, eb, c, d, hd with
    | _, _, rfl, rfl, _, _, hd => exact hd
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

Tactic:
Quotient.inductionOn₂ x y fun _ _ => PSet.mem_sUnion.trans
    ⟨fun ⟨z, h⟩ => ⟨⟦z⟧, h⟩, fun ⟨z, h⟩ => Quotient.inductionOn z (fun z h => ⟨z, h⟩) h⟩

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u_1}
h : x.Nonempty
simp : (∀ z ∈ x, y ∈ z) → y ∈ ⋃₀ x
⊢ y ∈ ZFSet.sep (fun (y : ZFSet.{u_1}) ↦ ∀ z ∈ x, y ∈ z) (⋃₀ x) ↔ ∀ z ∈ x, y ∈ z

Tactic:
simp only [and_iff_right_iff_imp, mem_sep]

Premises used: ZFSet.mem_sep, and_iff_right_iff_imp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u_1}
h : x.Nonempty
mem : ∀ z ∈ x, y ∈ z
apply : ∃ z ∈ x, y ∈ z
⊢ y ∈ ⋃₀ x

Tactic:
apply mem_sUnion.mpr

Premises used: Iff.mpr, ZFSet.mem_sUnion
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u_1}
h : x.Nonempty
mem : ∀ z ∈ x, y ∈ z
replace : ∀ (s : ZFSet.{u_1}) (h : s ∈ (↑x : Set ZFSet.{u_1})), ∃ z ∈ x, y ∈ z
⊢ ∃ z ∈ x, y ∈ z

Tactic:
replace ⟨s, h⟩ := h
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u_1}
mem : ∀ z ∈ x, y ∈ z
s : ZFSet.{u_1}
h : s ∈ (↑x : Set ZFSet.{u_1})
⊢ ∃ z ∈ x, y ∈ z

Tactic:
⟨_, h, mem _ h⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u_1}
mem : ∀ z ∈ x, y ∈ z
s : ZFSet.{u_1}
h : s ∈ (↑x : Set ZFSet.{u_1})
⊢ ∃ z ∈ x, y ∈ z

Tactic:
exact ⟨_, h, mem _ h⟩
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
a : ∀ (z : ZFSet.{u}), z ∈ ⋃₀ ∅ ↔ Membership.mem (γ := ZFSet.{u}) ∅ z
⊢ ⋃₀ ∅ = ∅

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
z : ZFSet.{u}
⊢ z ∈ ⋃₀ ∅ ↔ Membership.mem (γ := ZFSet.{u}) ∅ z

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
⊢ ⋂₀ ∅ = ∅

Tactic:
simp [sInter]

Premises used: ZFSet.sInter
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
inl : ∀ (hy : y ∈ ⋂₀ ∅) (hz : Membership.mem (γ := ZFSet.{u_1}) ∅ z), y ∈ z
inr : ∀ (hx : x.Nonempty), y ∈ z
⊢ y ∈ z

Tactic:
rcases eq_empty_or_nonempty x with (rfl | hx)

Premises used: ZFSet.eq_empty_or_nonempty, rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ ∅
hz : Membership.mem (γ := ZFSet.{u_1}) ∅ z
⊢ y ∈ z

Tactic:
(notMem_empty z hz).elim

Premises used: ZFSet.notMem_empty, False.elim
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ ∅
hz : Membership.mem (γ := ZFSet.{u_1}) ∅ z
⊢ y ∈ z

Tactic:
exact (notMem_empty z hz).elim

Premises used: ZFSet.notMem_empty, False.elim
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
hx : x.Nonempty
⊢ y ∈ z

Tactic:
(mem_sInter hx).1 hy z hz

Premises used: Iff.mp, ZFSet.mem_sInter
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
hx : x.Nonempty
⊢ y ∈ z

Tactic:
exact (mem_sInter hx).1 hy z hz

Premises used: Iff.mp, ZFSet.mem_sInter
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
hy : y ∈ z
hz : z ∈ x
⊢ y ∈ ⋃₀ x

Tactic:
mem_sUnion.2 ⟨z, hz, hy⟩

Premises used: Iff.mpr, ZFSet.mem_sUnion, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
hy : y ∉ z
hz : z ∈ x
⊢ y ∉ ⋂₀ x

Tactic:
fun hx => hy <| mem_of_mem_sInter hx hz

Premises used: ZFSet.mem_of_mem_sInter, Not
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
simp_rw : (∃ (z : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) {x} z ∧ y ∈ z) ↔ y ∈ x
simp_rw₁ : (∃ (z : ZFSet.{u}), z = x ∧ y ∈ z) ↔ y ∈ x
⊢ y ∈ ⋃₀ {x} ↔ y ∈ x

Tactic:
simp_rw [mem_sUnion, mem_singleton, exists_eq_left]

Premises used: ZFSet.mem_sUnion, exists_eq_left, ZFSet.mem_singleton
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
simp_rw : (∀ (z : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) {x} z → y ∈ z) ↔ y ∈ x
simp_rw₁ : (∀ (z : ZFSet.{u}), z = x → y ∈ z) ↔ y ∈ x
⊢ y ∈ ⋂₀ {x} ↔ y ∈ x

Tactic:
simp_rw [mem_sInter (singleton_nonempty x), mem_singleton, forall_eq]

Premises used: ZFSet.singleton_nonempty, forall_eq, ZFSet.mem_singleton, ZFSet.mem_sInter
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u}
h : ∀ (x_1 : ZFSet.{u}), x_1 ∈ (↑(⋃₀ x) : Set ZFSet.{u}) ↔ x_1 ∈ ⋃₀ (SetLike.coe '' (↑x : Set ZFSet.{u}))
⊢ (↑(⋃₀ x) : Set ZFSet.{u}) = ⋃₀ (SetLike.coe '' (↑x : Set ZFSet.{u}))

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x x_1 : ZFSet.{u}
⊢ x_1 ∈ (↑(⋃₀ x) : Set ZFSet.{u}) ↔ x_1 ∈ ⋃₀ (SetLike.coe '' (↑x : Set ZFSet.{u}))

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u}
h : x.Nonempty
h₁ : ∀ (x_1 : ZFSet.{u}), x_1 ∈ (↑(⋂₀ x) : Set ZFSet.{u}) ↔ x_1 ∈ ⋂₀ (SetLike.coe '' (↑x : Set ZFSet.{u}))
⊢ (↑(⋂₀ x) : Set ZFSet.{u}) = ⋂₀ (SetLike.coe '' (↑x : Set ZFSet.{u}))

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u}
h : x.Nonempty
x_1 : ZFSet.{u}
⊢ x_1 ∈ (↑(⋂₀ x) : Set ZFSet.{u}) ↔ x_1 ∈ ⋂₀ (SetLike.coe '' (↑x : Set ZFSet.{u}))

Tactic:
simp [mem_sInter h]

Premises used: ZFSet.mem_sInter
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u_1}
H : Eq (α := ZFSet.{u_1}) {x} {y}
this : ⋃₀ {x} = ⋃₀ {y} := ⋯
rwa : ∀ (this : x = ⋃₀ {y}), x = y
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : x = y), x = y
⊢ x = y

Tactic:
rwa [sUnion_singleton, sUnion_singleton] at this

Premises used: ZFSet.sUnion_singleton
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u_1}
⊢ Eq (α := ZFSet.{u_1}) {x} {y} ↔ x = y

Tactic:
singleton_injective.eq_iff

Premises used: Function.Injective.eq_iff, ZFSet.singleton_injective
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ ⋃₀ {x, y} = x ∪ y

Tactic:
rfl

Premises used: Quotient.map, ZFSet.sUnion, ZFSet.union, Quot.map, rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ ZFSet.sep (fun (x : ZFSet.{u}) ↦ x ∈ y) x = x ∩ y

Tactic:
rfl

Premises used: ZFSet.sep, Quotient.map, Quot.map, ZFSet.inter, rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ ZFSet.sep (fun (x : ZFSet.{u}) ↦ x ∉ y) x = x \ y

Tactic:
rfl

Premises used: ZFSet.sep, Quotient.map, ZFSet.diff, Quot.map, rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y

Tactic:
simp [← sUnion_pair]

Premises used: ZFSet.sUnion_pair
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y

Tactic:
simp [← sep_mem]

Premises used: ZFSet.sep_mem
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ z ∈ x \ y ↔ z ∈ x ∧ z ∉ y

Tactic:
simp [← sep_notMem]

Premises used: ZFSet.sep_notMem
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
h : ∀ (x_1 : ZFSet.{u}), x_1 ∈ (↑(x ∪ y) : Set ZFSet.{u}) ↔ x_1 ∈ (↑x : Set ZFSet.{u}) ∪ (↑y : Set ZFSet.{u})
⊢ (↑(x ∪ y) : Set ZFSet.{u}) = (↑x : Set ZFSet.{u}) ∪ (↑y : Set ZFSet.{u})

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y x_1 : ZFSet.{u}
⊢ x_1 ∈ (↑(x ∪ y) : Set ZFSet.{u}) ↔ x_1 ∈ (↑x : Set ZFSet.{u}) ∪ (↑y : Set ZFSet.{u})

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
h : ∀ (x_1 : ZFSet.{u}), x_1 ∈ (↑(x ∩ y) : Set ZFSet.{u}) ↔ x_1 ∈ (↑x : Set ZFSet.{u}) ∩ (↑y : Set ZFSet.{u})
⊢ (↑(x ∩ y) : Set ZFSet.{u}) = (↑x : Set ZFSet.{u}) ∩ (↑y : Set ZFSet.{u})

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y x_1 : ZFSet.{u}
⊢ x_1 ∈ (↑(x ∩ y) : Set ZFSet.{u}) ↔ x_1 ∈ (↑x : Set ZFSet.{u}) ∩ (↑y : Set ZFSet.{u})

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
h : ∀ (x_1 : ZFSet.{u}), x_1 ∈ (↑(x \ y) : Set ZFSet.{u}) ↔ x_1 ∈ (↑x : Set ZFSet.{u}) \ (↑y : Set ZFSet.{u})
⊢ (↑(x \ y) : Set ZFSet.{u}) = (↑x : Set ZFSet.{u}) \ (↑y : Set ZFSet.{u})

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y x_1 : ZFSet.{u}
⊢ x_1 ∈ (↑(x \ y) : Set ZFSet.{u}) ↔ x_1 ∈ (↑x : Set ZFSet.{u}) \ (↑y : Set ZFSet.{u})

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
hxy : x ⊆ y
a : ∀ (z : ZFSet.{u}), z ∈ x ∩ y ↔ z ∈ x
⊢ x ∩ y = x

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
hxy : x ⊆ y
z : ZFSet.{u}
⊢ z ∈ x ∩ y ↔ z ∈ x

Tactic:
simpa using @hxy _
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
hyx : y ⊆ x
a : ∀ (z : ZFSet.{u}), z ∈ x ∩ y ↔ z ∈ y
⊢ x ∩ y = y

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
hyx : y ⊆ x
z : ZFSet.{u}
⊢ z ∈ x ∩ y ↔ z ∈ y

Tactic:
simpa using @hyx _
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y z x : ZFSet.{u}
⊢ Function.LeftInverse
    (fun (s : (↑(𝒫 (↑x : Set ZFSet.{u})) : Type (u + 1))) ↦
      Subtype.mk (p := fun (x_2 : ZFSet.{u}) ↦ x_2 ∈ x.powerset)
        (ZFSet.sep (fun (x_2 : ZFSet.{u}) ↦ x_2 ∈ (↑s : Set ZFSet.{u})) x) ⋯)
    fun (y : ↥x.powerset) ↦
    Subtype.mk (p := fun (x_2 : Set ZFSet.{u}) ↦ x_2 ∈ 𝒫 (↑x : Set ZFSet.{u})) (↑(↑y : ZFSet.{u}) : Set ZFSet.{u}) ⋯

Tactic:
simp +contextual [Function.LeftInverse]

Premises used: Function.LeftInverse
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y z x : ZFSet.{u}
⊢ Function.RightInverse
    (fun (s : (↑(𝒫 (↑x : Set ZFSet.{u})) : Type (u + 1))) ↦
      Subtype.mk (p := fun (x_2 : ZFSet.{u}) ↦ x_2 ∈ x.powerset)
        (ZFSet.sep (fun (x_2 : ZFSet.{u}) ↦ x_2 ∈ (↑s : Set ZFSet.{u})) x) ⋯)
    fun (y : ↥x.powerset) ↦
    Subtype.mk (p := fun (x_2 : Set ZFSet.{u}) ↦ x_2 ∈ 𝒫 (↑x : Set ZFSet.{u})) (↑(↑y : ZFSet.{u}) : Set ZFSet.{u}) ⋯

Tactic:
simp +contextual [Function.LeftInverse, Function.RightInverse, Set.setOf_and]

Premises used: Function.LeftInverse, Set.setOf_and, Function.RightInverse
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u_1}
a : ∀ (z : ZFSet.{u_1}), z ∈ insert x y ↔ z ∈ {x} ∪ y
⊢ insert x y = {x} ∪ y

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
⊢ z ∈ insert x y ↔ z ∈ {x} ∪ y

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
⊢ WellFounded fun (x1 x2 : ZFSet.{u_1}) ↦ x1 ∈ x2

Tactic:
(wellFounded_lift₂_iff (H := fun a b c d hx hy =>
    propext ((@Mem.congr_left a c hx).trans (@Mem.congr_right b d hy _)))).mpr PSet.mem_wf

Premises used: Iff.mpr, PSet.mem_wf, wellFounded_lift₂_iff, Set.Mem, ZFSet, setOf, ZFSet.toSet
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u_1} → Prop
x : ZFSet.{u_1}
h : ∀ (x : ZFSet.{u_1}), (∀ y ∈ x, p y) → p x
⊢ p x

Tactic:
mem_wf.induction x h

Premises used: ZFSet.mem_wf, WellFounded.induction
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ IsWellFounded ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) ↦ x1 ∈ x2

Tactic:
⟨mem_wf⟩

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

Tactic:
asymm_of (· ∈ ·)

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

Tactic:
irrefl_of (· ∈ ·) x

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

Tactic:
fun h' ↦ mem_irrefl _ (h' h)

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

Tactic:
imp_not_comm.2 not_subset_of_mem h

Premises used: Iff.mpr, ZFSet.not_subset_of_mem, imp_not_comm
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u}
h : x ≠ ∅
⊢ ∃ y ∈ x, x ∩ y = ∅

Tactic:
by_contradiction fun ne =>
    h <| (eq_empty x).2 fun y =>
      @inductionOn (fun z => z ∉ x) y fun z IH zx =>
        ne ⟨z, zx, (eq_empty _).2 fun w wxz =>
          let ⟨wx, wz⟩ := mem_inter.1 wxz
          IH w wz wx⟩

Premises used: Iff.mpr, False, ZFSet.eq_empty, ZFSet.mem_inter, ZFSet.inductionOn, Inter.inter, _private.0.ZFSet.regularity.match_1, And.intro, by_contradiction, Exists.intro, Iff.mp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
x_1 x_2 : PSet.{u}
α : Type u
A : α → PSet.{u}
h : ⟦x_2⟧ ∈ ⟦PSet.mk α A⟧
a : (PSet.mk α A).Type
ya : x_2.Equiv ((PSet.mk α A).Func a)
simp : ZFSet.mk (Definable₁.out f x_2) ∈ image f (ZFSet.mk (PSet.mk α A))
⊢ f ⟦x_2⟧ ∈ image f ⟦PSet.mk α A⟧

Tactic:
simp only [mk_eq, ← Definable₁.mk_out (f := f)]

Premises used: ZFSet.mk_eq, ZFSet.Definable₁.mk_out
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
x_1 x_2 : PSet.{u}
α : Type u
A : α → PSet.{u}
h : ⟦x_2⟧ ∈ ⟦PSet.mk α A⟧
a : (PSet.mk α A).Type
ya : x_2.Equiv ((PSet.mk α A).Func a)
⊢ ZFSet.mk (Definable₁.out f x_2) ∈ image f (ZFSet.mk (PSet.mk α A))

Tactic:
⟨a, Definable₁.out_equiv f ya⟩

Premises used: ZFSet.Definable₁.out_equiv, PSet.Mem, Set.Mem, setOf, ZFSet.toSet, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
x_1 x_2 : PSet.{u}
α : Type u
A : α → PSet.{u}
h : ⟦x_2⟧ ∈ ⟦PSet.mk α A⟧
a : (PSet.mk α A).Type
ya : x_2.Equiv ((PSet.mk α A).Func a)
⊢ ZFSet.mk (Definable₁.out f x_2) ∈ image f (ZFSet.mk (PSet.mk α A))

Tactic:
exact ⟨a, Definable₁.out_equiv f ya⟩
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
⊢ y ∈ image f x ↔ ∃ z ∈ x, f z = y

Tactic:
Quotient.inductionOn₂ x y fun ⟨_, A⟩ _ =>
    ⟨fun ⟨a, ya⟩ => ⟨⟦A a⟧, Mem.mk A a, ((Quotient.sound ya).trans Definable₁.mk_out).symm⟩,
      fun ⟨_, hz, e⟩ => e ▸ image.mk _ _ hz⟩

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u_1} → ZFSet.{u_1}
inst : Definable₁ f
x : ZFSet.{u_1}
h : ∀ (x_1 : ZFSet.{u_1}), x_1 ∈ (↑(image f x) : Set ZFSet.{u_1}) ↔ x_1 ∈ f '' (↑x : Set ZFSet.{u_1})
⊢ (↑(image f x) : Set ZFSet.{u_1}) = f '' (↑x : Set ZFSet.{u_1})

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u_1} → ZFSet.{u_1}
inst : Definable₁ f
x x_1 : ZFSet.{u_1}
⊢ x_1 ∈ (↑(image f x) : Set ZFSet.{u_1}) ↔ x_1 ∈ f '' (↑x : Set ZFSet.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
mp : ⟦y⟧ ∈ range f → ∃ (i : α), f i = ⟦y⟧
mpr : (∃ (i : α), f i = ⟦y⟧) → ⟦y⟧ ∈ range f
⊢ ⟦y⟧ ∈ range f ↔ ∃ (i : α), f i = ⟦y⟧

Tactic:
constructor
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z :
  (PSet.mk (Shrink.{u, u_1} α) (Quotient.out ∘ f ∘ (⇑(Equiv.symm (equivShrink α)) : (a : Shrink.{u, u_1} α) → α))).Type
hz :
  y.Equiv
    ((PSet.mk (Shrink.{u, u_1} α)
          (Quotient.out ∘ f ∘ (⇑(Equiv.symm (equivShrink α)) : (a : Shrink.{u, u_1} α) → α))).Func
      z)
⊢ ∃ (i : α), f i = ⟦y⟧

Tactic:
⟨(equivShrink α).symm z, Quotient.eq_mk_iff_out.2 hz.symm⟩

Premises used: Iff.mpr, PSet.Equiv.symm, Quotient.eq_mk_iff_out, Exists.intro, Equiv.symm, equivShrink, DFunLike.coe
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z :
  (PSet.mk (Shrink.{u, u_1} α) (Quotient.out ∘ f ∘ (⇑(Equiv.symm (equivShrink α)) : (a : Shrink.{u, u_1} α) → α))).Type
hz :
  y.Equiv
    ((PSet.mk (Shrink.{u, u_1} α)
          (Quotient.out ∘ f ∘ (⇑(Equiv.symm (equivShrink α)) : (a : Shrink.{u, u_1} α) → α))).Func
      z)
⊢ ∃ (i : α), f i = ⟦y⟧

Tactic:
exact ⟨(equivShrink α).symm z, Quotient.eq_mk_iff_out.2 hz.symm⟩
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : α
hz : f z = ⟦y⟧
h :
  y.Equiv
    ((PSet.mk (Shrink.{u, u_1} α)
          (Quotient.out ∘ f ∘ (⇑(Equiv.symm (equivShrink α)) : (a : Shrink.{u, u_1} α) → α))).Func
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α) z))
⊢ ⟦y⟧ ∈ range f

Tactic:
use equivShrink α z

Premises used: equivShrink, DFunLike.coe
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : α
hz : f z = ⟦y⟧
⊢ y.Equiv
    ((PSet.mk (Shrink.{u, u_1} α)
          (Quotient.out ∘ f ∘ (⇑(Equiv.symm (equivShrink α)) : (a : Shrink.{u, u_1} α) → α))).Func
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α) z))

Tactic:
simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)

Premises used: PSet.Equiv.symm, Quotient.mk_out
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
h : ∀ (x : ZFSet.{u}), x ∈ (↑(range f) : Set ZFSet.{u}) ↔ x ∈ Set.range f
⊢ (↑(range f) : Set ZFSet.{u}) = Set.range f

Tactic:
ext