internlm/Lean-Github huggingface dataset:
Theorem: SetTheory.dom_rcomp
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
⊢ dom (rcomp s r) = dom r
Tactic:
ext t
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ t ∈ dom (rcomp s r) ↔ t ∈ dom r
Theorem: SetTheory.dom_rcomp
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ t ∈ dom (rcomp s r) ↔ t ∈ dom r
Tactic:
simp only [mem_dom_iff, mem_rcomp_iff, opair_injective]
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) ↔ ∃ z, opair t z ∈ r
Theorem: SetTheory.dom_rcomp
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) ↔ ∃ z, opair t z ∈ r
Tactic:
constructor
Proof state after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) → ∃ z, opair t z ∈ r

case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z, opair t z ∈ r) → ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Theorem: SetTheory.dom_rcomp
Proof state before:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) → ∃ z, opair t z ∈ r
Tactic:
rintro ⟨z, _, b, _, ⟨rfl, rfl⟩, _, hc⟩
Proof state after:
case h.mp.intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s : V
h : ran r ⊆ dom s
t z b : V
left✝ : opair b z ∈ s
hc : opair t b ∈ r
⊢ ∃ z, opair t z ∈ r
Theorem: SetTheory.dom_rcomp
Proof state before:
case h.mp.intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s : V
h : ran r ⊆ dom s
t z b : V
left✝ : opair b z ∈ s
hc : opair t b ∈ r
⊢ ∃ z, opair t z ∈ r
Tactic:
exact ⟨_, hc⟩
Proof state after:
no goals
Theorem: SetTheory.dom_rcomp
Proof state before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z, opair t z ∈ r) → ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
rintro ⟨b, hb⟩
Proof state after:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Theorem: SetTheory.dom_rcomp
Proof state before:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
have : b ∈ ran r := by
  rw [mem_ran_iff]
  exact ⟨t, hb⟩
Proof state after:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this : b ∈ ran r
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Theorem: SetTheory.dom_rcomp
Proof state before:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this : b ∈ ran r
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
have := h this
Proof state after:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this✝ : b ∈ ran r
this : b ∈ dom s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Theorem: SetTheory.dom_rcomp
Proof state before:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this✝ : b ∈ ran r
this : b ∈ dom s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
rw [mem_dom_iff] at this
Proof state after:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this✝ : b ∈ ran r
this : ∃ z, opair b z ∈ s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Theorem: SetTheory.dom_rcomp
Proof state before:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this✝ : b ∈ ran r
this : ∃ z, opair b z ∈ s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
obtain ⟨z, hz⟩ := this
Proof state after:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this : b ∈ ran r
z : V
hz : opair b z ∈ s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Theorem: SetTheory.dom_rcomp
Proof state before:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this : b ∈ ran r
z : V
hz : opair b z ∈ s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
exact ⟨z, _, b, _, ⟨rfl, rfl⟩, hz, hb⟩
Proof state after:
no goals
Theorem: SetTheory.dom_rcomp
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ b ∈ ran r
Tactic:
rw [mem_ran_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ ∃ z, opair z b ∈ r
Theorem: SetTheory.dom_rcomp
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ ∃ z, opair z b ∈ r
Tactic:
exact ⟨t, hb⟩
Proof state after:
no goals
Theorem: SetTheory.ran_rcomp
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ ran (rcomp s r) ⊆ ran s
Tactic:
intro t
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z s t : V
⊢ t ∈ ran (rcomp s r) → t ∈ ran s
Theorem: SetTheory.ran_rcomp
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z s t : V
⊢ t ∈ ran (rcomp s r) → t ∈ ran s
Tactic:
simp only [mem_ran_iff, mem_rcomp_iff, opair_injective]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z s t : V
⊢ (∃ z a b c, (z = a ∧ t = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) → ∃ z, opair z t ∈ s
Theorem: SetTheory.ran_rcomp
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z s t : V
⊢ (∃ z a b c, (z = a ∧ t = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) → ∃ z, opair z t ∈ s
Tactic:
rintro ⟨z, _, b, _, ⟨rfl, rfl⟩, hc, _⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s t z b : V
hc : opair b t ∈ s
right✝ : opair z b ∈ r
⊢ ∃ z, opair z t ∈ s
Theorem: SetTheory.ran_rcomp
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s t z b : V
hc : opair b t ∈ s
right✝ : opair z b ∈ r
⊢ ∃ z, opair z t ∈ s
Tactic:
exact ⟨_, hc⟩
Proof state after:
no goals
Theorem: SetTheory.interpret_memId'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memId x y) v l ↔ ∃ z, z ∈ interpretTerm V v l y ∧ interpretTerm V v l x = opair z z
Tactic:
unfold BoundedFormula.memId
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.and (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc y))
          (BoundedFormula.eqOPair (termSucc x) (Sum.inr (Fin.last n)) (Sum.inr (Fin.last n)))))
      v l ↔
    ∃ z, z ∈ interpretTerm V v l y ∧ interpretTerm V v l x = opair z z
Theorem: SetTheory.interpret_memId'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.and (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc y))
          (BoundedFormula.eqOPair (termSucc x) (Sum.inr (Fin.last n)) (Sum.inr (Fin.last n)))))
      v l ↔
    ∃ z, z ∈ interpretTerm V v l y ∧ interpretTerm V v l x = opair z z
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.mem_id_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ y ∈ id x ↔ ∃ z, z ∈ x ∧ y = opair z z
Tactic:
unfold id
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ y ∈ sep (BoundedFormula.memId (Sum.inr 0) (Sum.inl ())) (fun x_1 => x) (prod x x) ↔ ∃ z, z ∈ x ∧ y = opair z z
Theorem: SetTheory.mem_id_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ y ∈ sep (BoundedFormula.memId (Sum.inr 0) (Sum.inl ())) (fun x_1 => x) (prod x x) ↔ ∃ z, z ∈ x ∧ y = opair z z
Tactic:
simp only [mem_sep_iff, interpret_memId']
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (y ∈ prod x x ∧
      ∃ z,
        z ∈ interpretTerm V (fun x_1 => x) (fun x => y) (Sum.inl ()) ∧
          interpretTerm V (fun x_1 => x) (fun x => y) (Sum.inr 0) = opair z z) ↔
    ∃ z, z ∈ x ∧ y = opair z z
Theorem: SetTheory.mem_id_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (y ∈ prod x x ∧
      ∃ z,
        z ∈ interpretTerm V (fun x_1 => x) (fun x => y) (Sum.inl ()) ∧
          interpretTerm V (fun x_1 => x) (fun x => y) (Sum.inr 0) = opair z z) ↔
    ∃ z, z ∈ x ∧ y = opair z z
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_memId
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memId x y) v l ↔ interpretTerm V v l x ∈ id (interpretTerm V v l y)
Tactic:
rw [mem_id_iff, interpret_memId']
Proof state after:
no goals
Theorem: SetTheory.interpret_isFunction
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
α : Type
n : Nat
v : α → V
l : Fin n → V
f : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isFunction f) v l ↔ IsFunction (interpretTerm V v l f)
Tactic:
unfold BoundedFormula.isFunction IsFunction
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
α : Type
n : Nat
v : α → V
l : Fin n → V
f : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and (BoundedFormula.isRelation f)
        (BoundedFormula.all
          (BoundedFormula.all
            (BoundedFormula.all
              (BoundedFormula.all
                (BoundedFormula.all
                  (BoundedFormula.imp
                    (BoundedFormula.eqOPair (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                      (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                      (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) }))
                    (BoundedFormula.imp
                      (BoundedFormula.eqOPair (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                        (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                        (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))
                      (BoundedFormula.imp
                        (BoundedFormula.mem (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                          (termSucc (termSucc (termSucc (termSucc (termSucc f))))))
                        (BoundedFormula.imp
                          (BoundedFormula.mem (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                            (termSucc (termSucc (termSucc (termSucc (termSucc f))))))
                          (BoundedFormula.eq (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) })
                            (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))))))))))))
      v l ↔
    IsRelation (interpretTerm V v l f) ∧
      ∀ (x s t : V), opair x s ∈ interpretTerm V v l f → opair x t ∈ interpretTerm V v l f → s = t
Theorem: SetTheory.interpret_isFunction
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
α : Type
n : Nat
v : α → V
l : Fin n → V
f : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and (BoundedFormula.isRelation f)
        (BoundedFormula.all
          (BoundedFormula.all
            (BoundedFormula.all
              (BoundedFormula.all
                (BoundedFormula.all
                  (BoundedFormula.imp
                    (BoundedFormula.eqOPair (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                      (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                      (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) }))
                    (BoundedFormula.imp
                      (BoundedFormula.eqOPair (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                        (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                        (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))
                      (BoundedFormula.imp
                        (BoundedFormula.mem (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                          (termSucc (termSucc (termSucc (termSucc (termSucc f))))))
                        (BoundedFormula.imp
                          (BoundedFormula.mem (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                            (termSucc (termSucc (termSucc (termSucc (termSucc f))))))
                          (BoundedFormula.eq (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) })
                            (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))))))))))))
      v l ↔
    IsRelation (interpretTerm V v l f) ∧
      ∀ (x s t : V), opair x s ∈ interpretTerm V v l f → opair x t ∈ interpretTerm V v l f → s = t
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_maps
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
α : Type
n : Nat
v : α → V
l : Fin n → V
f x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.maps f x y) v l ↔
    opair (interpretTerm V v l x) (interpretTerm V v l y) ∈ interpretTerm V v l f
Tactic:
unfold BoundedFormula.maps
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
α : Type
n : Nat
v : α → V
l : Fin n → V
f x y : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.and (BoundedFormula.eqOPair (Sum.inr (Fin.last n)) (termSucc x) (termSucc y))
          (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc f))))
      v l ↔
    opair (interpretTerm V v l x) (interpretTerm V v l y) ∈ interpretTerm V v l f
Theorem: SetTheory.interpret_maps
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
α : Type
n : Nat
v : α → V
l : Fin n → V
f x y : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.and (BoundedFormula.eqOPair (Sum.inr (Fin.last n)) (termSucc x) (termSucc y))
          (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc f))))
      v l ↔
    opair (interpretTerm V v l x) (interpretTerm V v l y) ∈ interpretTerm V v l f
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.mem_of_mem_dom
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
hx : x ∈ dom f.graph
⊢ x ∈ a
Tactic:
rwa [← f.dom_eq]
Proof state after:
no goals
Theorem: SetTheory.mem_dom_of_mem
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
hx : x ∈ a
⊢ x ∈ dom f.graph
Tactic:
rwa [f.dom_eq]
Proof state after:
no goals
Theorem: SetTheory.mem_apply_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c f : V
⊢ y ∈ apply f x ↔ ∃ z, opair x z ∈ f ∧ y ∈ z
Tactic:
unfold apply
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c f : V
⊢ y ∈ ⋃ image f {x} ↔ ∃ z, opair x z ∈ f ∧ y ∈ z
Theorem: SetTheory.mem_apply_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c f : V
⊢ y ∈ ⋃ image f {x} ↔ ∃ z, opair x z ∈ f ∧ y ∈ z
Tactic:
simp [mem_image_iff]
Proof state after:
no goals
Theorem: SetTheory.eq_of_opair_mem_graph
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
⊢ y = apply f.graph x
Tactic:
ext z
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y ↔ z ∈ apply f.graph x
Theorem: SetTheory.eq_of_opair_mem_graph
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y ↔ z ∈ apply f.graph x
Tactic:
rw [mem_apply_iff]
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y ↔ ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1
Theorem: SetTheory.eq_of_opair_mem_graph
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y ↔ ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1
Tactic:
constructor
Proof state after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y → ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1

case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ (∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1) → z ∈ y
Theorem: SetTheory.eq_of_opair_mem_graph
Proof state before:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y → ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1
Tactic:
intro h'
Proof state after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
h' : z ∈ y
⊢ ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1
Theorem: SetTheory.eq_of_opair_mem_graph
Proof state before:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
h' : z ∈ y
⊢ ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1
Tactic:
exact ⟨_, h, h'⟩
Proof state after:
no goals
Theorem: SetTheory.eq_of_opair_mem_graph
Proof state before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ (∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1) → z ∈ y
Tactic:
intro ⟨t, ht, ht'⟩
Proof state after:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z t : V
ht : opair x t ∈ f.graph
ht' : z ∈ t
⊢ z ∈ y
Theorem: SetTheory.eq_of_opair_mem_graph
Proof state before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z t : V
ht : opair x t ∈ f.graph
ht' : z ∈ t
⊢ z ∈ y
Tactic:
cases f.isFunction.2 x y t h ht
Proof state after:
case h.mpr.refl
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
ht : opair x y ∈ f.graph
ht' : z ∈ y
⊢ z ∈ y
Theorem: SetTheory.eq_of_opair_mem_graph
Proof state before:
case h.mpr.refl
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
ht : opair x y ∈ f.graph
ht' : z ∈ y
⊢ z ∈ y
Tactic:
exact ht'
Proof state after:
no goals
Theorem: SetTheory.opair_mem_graph
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ opair x (apply f.graph x) ∈ f.graph
Tactic:
have := mem_dom_of_mem f h
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
this : x ∈ dom f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Theorem: SetTheory.opair_mem_graph
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
this : x ∈ dom f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Tactic:
rw [mem_dom_iff] at this
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
this : ∃ z, opair x z ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Theorem: SetTheory.opair_mem_graph
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
this : ∃ z, opair x z ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Tactic:
rcases this with ⟨y, hy⟩
Proof state after:
case intro
V : Type u_1
inst✝ : Zermelo V
r x y✝ z a b c : V
f : a ⟶ b
h : x ∈ a
y : V
hy : opair x y ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Theorem: SetTheory.opair_mem_graph
Proof state before:
case intro
V : Type u_1
inst✝ : Zermelo V
r x y✝ z a b c : V
f : a ⟶ b
h : x ∈ a
y : V
hy : opair x y ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Tactic:
cases eq_of_opair_mem_graph f hy
Proof state after:
case intro.refl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
hy : opair x (apply f.graph x) ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Theorem: SetTheory.opair_mem_graph
Proof state before:
case intro.refl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
hy : opair x (apply f.graph x) ∈ f.graph
⊢ opair x (apply f.graph x) ∈ f.graph
Tactic:
exact hy
Proof state after:
no goals
Theorem: SetTheory.opair_mem_graph_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ opair x y ∈ f.graph ↔ y = apply f.graph x
Tactic:
constructor
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ opair x y ∈ f.graph → y = apply f.graph x

case mpr
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ y = apply f.graph x → opair x y ∈ f.graph
Theorem: SetTheory.opair_mem_graph_iff
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ opair x y ∈ f.graph → y = apply f.graph x
Tactic:
exact eq_of_opair_mem_graph f
Proof state after:
no goals
Theorem: SetTheory.opair_mem_graph_iff
Proof state before:
case mpr
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ y = apply f.graph x → opair x y ∈ f.graph
Tactic:
rintro rfl
Proof state after:
case mpr
V : Type u_1
inst✝ : Zermelo V
r x z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ opair x (apply f.graph x) ∈ f.graph
Theorem: SetTheory.opair_mem_graph_iff
Proof state before:
case mpr
V : Type u_1
inst✝ : Zermelo V
r x z a b c : V
f : a ⟶ b
h : x ∈ a
⊢ opair x (apply f.graph x) ∈ f.graph
Tactic:
exact opair_mem_graph f h
Proof state after:
no goals
Theorem: SetTheory.Function.ext
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
⊢ f = g
Tactic:
suffices f.graph = g.graph from by
  cases f
  cases this
  rfl
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
⊢ f.graph = g.graph
Theorem: SetTheory.Function.ext
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
⊢ f.graph = g.graph
Tactic:
ext x
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
⊢ x ∈ f.graph ↔ x ∈ g.graph
Theorem: SetTheory.Function.ext
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
⊢ x ∈ f.graph ↔ x ∈ g.graph
Tactic:
constructor
Proof state after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
⊢ x ∈ f.graph → x ∈ g.graph

case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
⊢ x ∈ g.graph → x ∈ f.graph
Theorem: SetTheory.Function.ext
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
this : f.graph = g.graph
⊢ f = g
Tactic:
cases f
Proof state after:
case mk
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
g : a ⟶ b
graph✝ : V
isFunction✝ : IsFunction graph✝
dom_eq✝ : dom graph✝ = a
ran_subset✝ : ran graph✝ ⊆ b
h :
  ∀ (x : V),
    x ∈ a →
      apply { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph x =
        apply g.graph x
this : { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph = g.graph
⊢ { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ } = g