internlm/Lean-Github huggingface dataset:
Theorem: SetTheory.inter_self
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ x ↔ z✝ ∈ x
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.union_pair_eq_inter_pair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ {x} ∪ pair x y = {x} ∩ pair x y ↔ x = y
Tactic:
constructor
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ {x} ∪ pair x y = {x} ∩ pair x y → x = y

case mpr
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x = y → {x} ∪ pair x y = {x} ∩ pair x y
Theorem: SetTheory.union_pair_eq_inter_pair
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ {x} ∪ pair x y = {x} ∩ pair x y → x = y
Tactic:
intro h
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
h : {x} ∪ pair x y = {x} ∩ pair x y
⊢ x = y
Theorem: SetTheory.union_pair_eq_inter_pair
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
h : {x} ∪ pair x y = {x} ∩ pair x y
⊢ x = y
Tactic:
rw [ext_iff] at h
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
⊢ x = y
Theorem: SetTheory.union_pair_eq_inter_pair
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
⊢ x = y
Tactic:
have := (h y).mp ?_
Proof state after:
case mp.refine_2
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
this : y ∈ {x} ∩ pair x y
⊢ x = y

case mp.refine_1
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
⊢ y ∈ {x} ∪ pair x y
Theorem: SetTheory.union_pair_eq_inter_pair
Proof state before:
case mp.refine_2
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
this : y ∈ {x} ∩ pair x y
⊢ x = y
Tactic:
rw [mem_inter_iff, mem_singleton_iff] at this
Proof state after:
case mp.refine_2
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
this : y = x ∧ y ∈ pair x y
⊢ x = y
Theorem: SetTheory.union_pair_eq_inter_pair
Proof state before:
case mp.refine_2
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
this : y = x ∧ y ∈ pair x y
⊢ x = y
Tactic:
exact this.1.symm
Proof state after:
no goals
Theorem: SetTheory.union_pair_eq_inter_pair
Proof state before:
case mp.refine_1
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
⊢ y ∈ {x} ∪ pair x y
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.union_pair_eq_inter_pair
Proof state before:
case mpr
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x = y → {x} ∪ pair x y = {x} ∩ pair x y
Tactic:
rintro rfl
Proof state after:
case mpr
V : Type u_1
inst✝ : Zermelo V
x z : V
⊢ {x} ∪ pair x x = {x} ∩ pair x x
Theorem: SetTheory.union_pair_eq_inter_pair
Proof state before:
case mpr
V : Type u_1
inst✝ : Zermelo V
x z : V
⊢ {x} ∪ pair x x = {x} ∩ pair x x
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.forall_not_mem
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
h : ∀ (y : V), ¬y ∈ x
⊢ x = ∅
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z : V
h : ∀ (y : V), ¬y ∈ x
z✝ : V
⊢ z✝ ∈ x ↔ z✝ ∈ ∅
Theorem: SetTheory.forall_not_mem
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z : V
h : ∀ (y : V), ¬y ∈ x
z✝ : V
⊢ z✝ ∈ x ↔ z✝ ∈ ∅
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.eq_empty_iff_forall_not_mem
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x = ∅ → ∀ (y : V), ¬y ∈ x
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.subset_of_eq
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
h : x = y
⊢ x ⊆ y
Tactic:
subst h
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x z : V
⊢ x ⊆ x
Theorem: SetTheory.subset_of_eq
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x z : V
⊢ x ⊆ x
Tactic:
exact subset_rfl
Proof state after:
no goals
Theorem: SetTheory.subset_antisymm
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
h₁ : x ⊆ y
h₂ : y ⊆ x
⊢ x = y
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z : V
h₁ : x ⊆ y
h₂ : y ⊆ x
z✝ : V
⊢ z✝ ∈ x ↔ z✝ ∈ y
Theorem: SetTheory.subset_antisymm
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z : V
h₁ : x ⊆ y
h₂ : y ⊆ x
z✝ : V
⊢ z✝ ∈ x ↔ z✝ ∈ y
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.russellSet_subset
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ russellSet x ⊆ x
Tactic:
unfold russellSet
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ sep (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inr 0))) (fun i => Empty.elim i) x ⊆ x
Theorem: SetTheory.russellSet_subset
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ sep (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inr 0))) (fun i => Empty.elim i) x ⊆ x
Tactic:
intro y hy
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z x y : V
hy : y ∈ sep (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inr 0))) (fun i => Empty.elim i) x
⊢ y ∈ x
Theorem: SetTheory.russellSet_subset
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z x y : V
hy : y ∈ sep (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inr 0))) (fun i => Empty.elim i) x
⊢ y ∈ x
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.mem_russellSet_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈ russellSet x ↔ y ∈ x ∧ ¬y ∈ y
Tactic:
unfold russellSet
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈ sep (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inr 0))) (fun i => Empty.elim i) x ↔ y ∈ x ∧ ¬y ∈ y
Theorem: SetTheory.mem_russellSet_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈ sep (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inr 0))) (fun i => Empty.elim i) x ↔ y ∈ x ∧ ¬y ∈ y
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.russellSet_not_mem
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ ¬russellSet x ∈ x
Tactic:
intro h
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
⊢ False
Theorem: SetTheory.russellSet_not_mem
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
⊢ False
Tactic:
by_cases h' : russellSet x ∈ russellSet x
Proof state after:
case pos
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : russellSet x ∈ russellSet x
⊢ False

case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : ¬russellSet x ∈ russellSet x
⊢ False
Theorem: SetTheory.russellSet_not_mem
Proof state before:
case pos
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : russellSet x ∈ russellSet x
⊢ False
Tactic:
have := mem_russellSet_iff.mp h'
Proof state after:
case pos
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : russellSet x ∈ russellSet x
this : russellSet x ∈ x ∧ ¬russellSet x ∈ russellSet x
⊢ False
Theorem: SetTheory.russellSet_not_mem
Proof state before:
case pos
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : russellSet x ∈ russellSet x
this : russellSet x ∈ x ∧ ¬russellSet x ∈ russellSet x
⊢ False
Tactic:
exact this.2 h'
Proof state after:
no goals
Theorem: SetTheory.russellSet_not_mem
Proof state before:
case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : ¬russellSet x ∈ russellSet x
⊢ False
Tactic:
have := h'
Proof state after:
case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' this : ¬russellSet x ∈ russellSet x
⊢ False
Theorem: SetTheory.russellSet_not_mem
Proof state before:
case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' this : ¬russellSet x ∈ russellSet x
⊢ False
Tactic:
rw [mem_russellSet_iff, not_and, not_not] at this
Proof state after:
case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : ¬russellSet x ∈ russellSet x
this : russellSet x ∈ x → russellSet x ∈ russellSet x
⊢ False
Theorem: SetTheory.russellSet_not_mem
Proof state before:
case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : ¬russellSet x ∈ russellSet x
this : russellSet x ∈ x → russellSet x ∈ russellSet x
⊢ False
Tactic:
exact h' (this h)
Proof state after:
no goals
Theorem: SetTheory.univ_not_set
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ ∃ y, ¬y ∈ x
Tactic:
by_contra h
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : ¬∃ y, ¬y ∈ x
⊢ False
Theorem: SetTheory.univ_not_set
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : ¬∃ y, ¬y ∈ x
⊢ False
Tactic:
simp only [not_exists, not_not] at h
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : ∀ (x_1 : V), x_1 ∈ x
⊢ False
Theorem: SetTheory.univ_not_set
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : ∀ (x_1 : V), x_1 ∈ x
⊢ False
Tactic:
exact russellSet_not_mem x (h _)
Proof state after:
no goals
Theorem: SetTheory.power_not_subset
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ ¬power x ⊆ x
Tactic:
intro h
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ False
Theorem: SetTheory.power_not_subset
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ False
Tactic:
refine russellSet_not_mem x (h ?_)
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ russellSet x ∈ power x
Theorem: SetTheory.power_not_subset
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ russellSet x ∈ power x
Tactic:
rw [mem_power_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ russellSet x ⊆ x
Theorem: SetTheory.power_not_subset
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ russellSet x ⊆ x
Tactic:
exact russellSet_subset x
Proof state after:
no goals
Theorem: SetTheory.power_ne
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ power x ≠ x
Tactic:
intro h
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x = x
⊢ False
Theorem: SetTheory.power_ne
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x = x
⊢ False
Tactic:
exact (power_not_subset x) (subset_of_eq h)
Proof state after:
no goals
Theorem: SetTheory.inter_comm
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∩ y = y ∩ x
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ y ↔ z✝ ∈ y ∩ x
Theorem: SetTheory.inter_comm
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ y ↔ z✝ ∈ y ∩ x
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.union_comm
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∪ y = y ∪ x
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∪ y ↔ z✝ ∈ y ∪ x
Theorem: SetTheory.union_comm
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∪ y ↔ z✝ ∈ y ∪ x
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.inter_assoc
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∩ y ∩ z = x ∩ (y ∩ z)
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ y ∩ z ↔ z✝ ∈ x ∩ (y ∩ z)
Theorem: SetTheory.inter_assoc
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ y ∩ z ↔ z✝ ∈ x ∩ (y ∩ z)
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.union_assoc
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∪ y ∪ z = x ∪ (y ∪ z)
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∪ y ∪ z ↔ z✝ ∈ x ∪ (y ∪ z)
Theorem: SetTheory.union_assoc
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∪ y ∪ z ↔ z✝ ∈ x ∪ (y ∪ z)
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.inter_distrib_left
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∩ (y ∪ z) = x ∩ y ∪ x ∩ z
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ (y ∪ z) ↔ z✝ ∈ x ∩ y ∪ x ∩ z
Theorem: SetTheory.inter_distrib_left
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ (y ∪ z) ↔ z✝ ∈ x ∩ y ∪ x ∩ z
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.inter_distrib_right
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ (x ∪ y) ∩ z = x ∩ z ∪ y ∩ z
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ (x ∪ y) ∩ z ↔ z✝ ∈ x ∩ z ∪ y ∩ z
Theorem: SetTheory.inter_distrib_right
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ (x ∪ y) ∩ z ↔ z✝ ∈ x ∩ z ∪ y ∩ z
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.union_distrib_left
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∪ y ∩ z = (x ∪ y) ∩ (x ∪ z)
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∪ y ∩ z ↔ z✝ ∈ (x ∪ y) ∩ (x ∪ z)
Theorem: SetTheory.union_distrib_left
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∪ y ∩ z ↔ z✝ ∈ (x ∪ y) ∩ (x ∪ z)
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.union_distrib_right
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∩ y ∪ z = (x ∪ z) ∩ (y ∪ z)
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ y ∪ z ↔ z✝ ∈ (x ∪ z) ∩ (y ∪ z)
Theorem: SetTheory.union_distrib_right
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ y ∪ z ↔ z✝ ∈ (x ∪ z) ∩ (y ∪ z)
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.inter_empty
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∩ ∅ = ∅
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ ∅ ↔ z✝ ∈ ∅
Theorem: SetTheory.inter_empty
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ ∅ ↔ z✝ ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.empty_inter
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ∅ ∩ x = ∅
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ ∅ ∩ x ↔ z✝ ∈ ∅
Theorem: SetTheory.empty_inter
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ ∅ ∩ x ↔ z✝ ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.union_empty
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∪ ∅ = x
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∪ ∅ ↔ z✝ ∈ x
Theorem: SetTheory.union_empty
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∪ ∅ ↔ z✝ ∈ x
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.empty_union
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ∅ ∪ x = x
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ ∅ ∪ x ↔ z✝ ∈ x
Theorem: SetTheory.empty_union
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ ∅ ∪ x ↔ z✝ ∈ x
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.interpret_eqUnion
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqUnion x y z) v l ↔ interpretTerm V v l x = interpretTerm V v l y ∪ interpretTerm V v l z
Tactic:
unfold BoundedFormula.eqUnion
Proof state after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.iff (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.or (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    interpretTerm V v l x = interpretTerm V v l y ∪ interpretTerm V v l z
Theorem: SetTheory.interpret_eqUnion
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.iff (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.or (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    interpretTerm V v l x = interpretTerm V v l y ∪ interpretTerm V v l z
Tactic:
rw [ext_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.iff (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.or (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    ∀ (z_1 : V), z_1 ∈ interpretTerm V v l x ↔ z_1 ∈ interpretTerm V v l y ∪ interpretTerm V v l z
Theorem: SetTheory.interpret_eqUnion
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.iff (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.or (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    ∀ (z_1 : V), z_1 ∈ interpretTerm V v l x ↔ z_1 ∈ interpretTerm V v l y ∪ interpretTerm V v l z
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.interpret_eqSucc
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqSucc x y) v l ↔ interpretTerm V v l x = succ (interpretTerm V v l y)
Tactic:
unfold BoundedFormula.eqSucc succ
Proof state after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.and (BoundedFormula.eqSingleton (Sum.inr (Fin.last n)) (termSucc y))
          (BoundedFormula.eqUnion (termSucc x) (termSucc y) (Sum.inr (Fin.last n)))))
      v l ↔
    interpretTerm V v l x = interpretTerm V v l y ∪ {interpretTerm V v l y}
Theorem: SetTheory.interpret_eqSucc
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.and (BoundedFormula.eqSingleton (Sum.inr (Fin.last n)) (termSucc y))
          (BoundedFormula.eqUnion (termSucc x) (termSucc y) (Sum.inr (Fin.last n)))))
      v l ↔
    interpretTerm V v l x = interpretTerm V v l y ∪ {interpretTerm V v l y}
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.interpret_eqEmpty
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqEmpty x) v l ↔ interpretTerm V v l x = ∅
Tactic:
unfold BoundedFormula.eqEmpty
Proof state after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.all (BoundedFormula.not (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x)))) v l ↔
    interpretTerm V v l x = ∅
Theorem: SetTheory.interpret_eqEmpty
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.all (BoundedFormula.not (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x)))) v l ↔
    interpretTerm V v l x = ∅
Tactic:
rw [eq_empty_iff_forall_not_mem]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.all (BoundedFormula.not (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x)))) v l ↔
    ∀ (y : V), ¬y ∈ interpretTerm V v l x
Theorem: SetTheory.interpret_eqEmpty
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.all (BoundedFormula.not (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x)))) v l ↔
    ∀ (y : V), ¬y ∈ interpretTerm V v l x
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.interpret_succClosed
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.succClosed x) v l ↔ ∀ (y : V), y ∈ interpretTerm V v l x → succ y ∈ interpretTerm V v l x
Tactic:
unfold BoundedFormula.succClosed
Proof state after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.exists
            (BoundedFormula.and
              (BoundedFormula.eqSucc (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }))
              (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc x)))))))
      v l ↔
    ∀ (y : V), y ∈ interpretTerm V v l x → succ y ∈ interpretTerm V v l x
Theorem: SetTheory.interpret_succClosed
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.exists
            (BoundedFormula.and
              (BoundedFormula.eqSucc (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }))
              (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc x)))))))
      v l ↔
    ∀ (y : V), y ∈ interpretTerm V v l x → succ y ∈ interpretTerm V v l x
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.inductive_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x : V
⊢ Inductive x ↔ ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x
Tactic:
constructor
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
x : V
⊢ Inductive x → ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x

case mpr
V : Type u_1
inst✝ : Zermelo V
x : V
⊢ (∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x) → Inductive x
Theorem: SetTheory.inductive_iff
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
x : V
⊢ Inductive x → ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x
Tactic:
intro h
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
x : V
h : Inductive x
⊢ ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x
Theorem: SetTheory.inductive_iff
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
x : V
h : Inductive x
⊢ ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x
Tactic:
exact ⟨h.empty_mem, h.succ_mem⟩
Proof state after:
no goals
Theorem: SetTheory.inductive_iff
Proof state before:
case mpr
V : Type u_1
inst✝ : Zermelo V
x : V
⊢ (∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x) → Inductive x
Tactic:
intro h
Proof state after:
case mpr
V : Type u_1
inst✝ : Zermelo V
x : V
h : ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x
⊢ Inductive x
Theorem: SetTheory.inductive_iff
Proof state before:
case mpr
V : Type u_1
inst✝ : Zermelo V
x : V
h : ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x
⊢ Inductive x
Tactic:
exact ⟨h.1, h.2⟩
Proof state after:
no goals