internlm/Lean-Github huggingface dataset:
Theorem: SetTheory.interpret_memPreimage
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 r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memPreimage x y r) v l ↔
    interpretTerm V v l x ∈ preimage (interpretTerm V v l r) (interpretTerm V v l y)
Tactic:
rw [mem_preimage_iff, interpret_memPreimage']
Proof state after:
no goals
Theorem: SetTheory.interpret_memInverse'
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 r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memInverse x r) v l ↔
    ∃ y z, interpretTerm V v l x = opair y z ∧ opair z y ∈ interpretTerm V v l r
Tactic:
unfold BoundedFormula.memInverse
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 r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.exists
            (BoundedFormula.and
              (BoundedFormula.and
                (BoundedFormula.eqOPair (termSucc (termSucc (termSucc x)))
                  (Sum.inr { val := n, isLt := (_ : n < n + (2 + 1)) })
                  (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (1 + 1)) }))
                (BoundedFormula.eqOPair (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (0 + 1)) })
                  (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (1 + 1)) })
                  (Sum.inr { val := n, isLt := (_ : n < n + (2 + 1)) })))
              (BoundedFormula.mem (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (0 + 1)) })
                (termSucc (termSucc (termSucc r))))))))
      v l ↔
    ∃ y z, interpretTerm V v l x = opair y z ∧ opair z y ∈ interpretTerm V v l r
Theorem: SetTheory.interpret_memInverse'
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 r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.exists
            (BoundedFormula.and
              (BoundedFormula.and
                (BoundedFormula.eqOPair (termSucc (termSucc (termSucc x)))
                  (Sum.inr { val := n, isLt := (_ : n < n + (2 + 1)) })
                  (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (1 + 1)) }))
                (BoundedFormula.eqOPair (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (0 + 1)) })
                  (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (1 + 1)) })
                  (Sum.inr { val := n, isLt := (_ : n < n + (2 + 1)) })))
              (BoundedFormula.mem (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (0 + 1)) })
                (termSucc (termSucc (termSucc r))))))))
      v l ↔
    ∃ y z, interpretTerm V v l x = opair y z ∧ opair z y ∈ interpretTerm V v l r
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.mem_inverse_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ inverse r ↔ ∃ y z, x = opair y z ∧ opair z y ∈ r
Tactic:
unfold inverse
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ sep (BoundedFormula.memInverse (Sum.inr 0) (Sum.inl ())) (fun x => r) (prod (ran r) (dom r)) ↔
    ∃ y z, x = opair y z ∧ opair z y ∈ r
Theorem: SetTheory.mem_inverse_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ sep (BoundedFormula.memInverse (Sum.inr 0) (Sum.inl ())) (fun x => r) (prod (ran r) (dom r)) ↔
    ∃ y z, x = opair y z ∧ opair z y ∈ r
Tactic:
simp only [mem_sep_iff, interpret_memInverse']
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())) ↔
    ∃ y z, x = opair y z ∧ opair z y ∈ r
Theorem: SetTheory.mem_inverse_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())) ↔
    ∃ y z, x = opair y z ∧ opair z y ∈ r
Tactic:
constructor
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())) →
    ∃ y z, x = opair y z ∧ opair z y ∈ r

case mpr
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (∃ y z, x = opair y z ∧ opair z y ∈ r) →
    x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())
Theorem: SetTheory.mem_inverse_iff
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())) →
    ∃ y z, x = opair y z ∧ opair z y ∈ r
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.mem_inverse_iff
Proof state before:
case mpr
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (∃ y z, x = opair y z ∧ opair z y ∈ r) →
    x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())
Tactic:
rintro ⟨a, b, rfl, ha⟩
Proof state after:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ opair a b ∈ prod (ran r) (dom r) ∧
    ∃ y z,
      interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inr 0) = opair y z ∧
        opair z y ∈ interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inl ())
Theorem: SetTheory.mem_inverse_iff
Proof state before:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ opair a b ∈ prod (ran r) (dom r) ∧
    ∃ y z,
      interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inr 0) = opair y z ∧
        opair z y ∈ interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inl ())
Tactic:
refine ⟨?_, by aesop⟩
Proof state after:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ opair a b ∈ prod (ran r) (dom r)
Theorem: SetTheory.mem_inverse_iff
Proof state before:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ opair a b ∈ prod (ran r) (dom r)
Tactic:
rw [mem_prod_iff]
Proof state after:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ a_1, a_1 ∈ ran r ∧ ∃ b_1, b_1 ∈ dom r ∧ opair a b = opair a_1 b_1
Theorem: SetTheory.mem_inverse_iff
Proof state before:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ a_1, a_1 ∈ ran r ∧ ∃ b_1, b_1 ∈ dom r ∧ opair a b = opair a_1 b_1
Tactic:
refine ⟨a, ?_, b, ?_, rfl⟩
Proof state after:
case mpr.intro.intro.intro.refine_1
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ a ∈ ran r

case mpr.intro.intro.intro.refine_2
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ b ∈ dom r
Theorem: SetTheory.mem_inverse_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ y z,
    interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inr 0) = opair y z ∧
      opair z y ∈ interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inl ())
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.mem_inverse_iff
Proof state before:
case mpr.intro.intro.intro.refine_1
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ a ∈ ran r
Tactic:
rw [mem_ran_iff]
Proof state after:
case mpr.intro.intro.intro.refine_1
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ z, opair z a ∈ r
Theorem: SetTheory.mem_inverse_iff
Proof state before:
case mpr.intro.intro.intro.refine_1
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ z, opair z a ∈ r
Tactic:
exact ⟨b, ha⟩
Proof state after:
no goals
Theorem: SetTheory.mem_inverse_iff
Proof state before:
case mpr.intro.intro.intro.refine_2
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ b ∈ dom r
Tactic:
rw [mem_dom_iff]
Proof state after:
case mpr.intro.intro.intro.refine_2
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ z, opair b z ∈ r
Theorem: SetTheory.mem_inverse_iff
Proof state before:
case mpr.intro.intro.intro.refine_2
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ z, opair b z ∈ r
Tactic:
exact ⟨a, ha⟩
Proof state after:
no goals
Theorem: SetTheory.interpret_memInverse
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 r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memInverse x r) v l ↔ interpretTerm V v l x ∈ inverse (interpretTerm V v l r)
Tactic:
rw [mem_inverse_iff, interpret_memInverse']
Proof state after:
no goals
Theorem: SetTheory.inverse_inverse
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hr : IsRelation r
⊢ inverse (inverse r) = r
Tactic:
ext x
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ x ∈ inverse (inverse r) ↔ x ∈ r
Theorem: SetTheory.inverse_inverse
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ x ∈ inverse (inverse r) ↔ x ∈ r
Tactic:
simp only [mem_inverse_iff]
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ (∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ x ∈ r
Theorem: SetTheory.inverse_inverse
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ (∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ x ∈ r
Tactic:
constructor
Proof state after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ (∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) → x ∈ r

case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ x ∈ r → ∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r
Theorem: SetTheory.inverse_inverse
Proof state before:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ (∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) → x ∈ r
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.inverse_inverse
Proof state before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ x ∈ r → ∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r
Tactic:
intro h
Proof state after:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
h : x ∈ r
⊢ ∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r
Theorem: SetTheory.inverse_inverse
Proof state before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
h : x ∈ r
⊢ ∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r
Tactic:
obtain ⟨y, z, rfl⟩ := hr x h
Proof state after:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y✝ z✝ : V
hr : IsRelation r
y z : V
h : opair y z ∈ r
⊢ ∃ y_1 z_1, opair y z = opair y_1 z_1 ∧ ∃ y z, opair z_1 y_1 = opair y z ∧ opair z y ∈ r
Theorem: SetTheory.inverse_inverse
Proof state before:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y✝ z✝ : V
hr : IsRelation r
y z : V
h : opair y z ∈ r
⊢ ∃ y_1 z_1, opair y z = opair y_1 z_1 ∧ ∃ y z, opair z_1 y_1 = opair y z ∧ opair z y ∈ r
Tactic:
exact ⟨y, z, rfl, z, y, rfl, h⟩
Proof state after:
no goals
Theorem: SetTheory.image_inverse
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ image (inverse r) x = preimage r x
Tactic:
ext y
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ y ∈ image (inverse r) x ↔ y ∈ preimage r x
Theorem: SetTheory.image_inverse
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ y ∈ image (inverse r) x ↔ y ∈ preimage r x
Tactic:
simp only [mem_image_iff, mem_preimage_iff, mem_inverse_iff]
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ (∃ z, z ∈ x ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ ∃ z, z ∈ x ∧ opair y z ∈ r
Theorem: SetTheory.image_inverse
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ (∃ z, z ∈ x ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ ∃ z, z ∈ x ∧ opair y z ∈ r
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.preimage_inverse
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ preimage (inverse r) x = image r x
Tactic:
ext y
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ y ∈ preimage (inverse r) x ↔ y ∈ image r x
Theorem: SetTheory.preimage_inverse
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ y ∈ preimage (inverse r) x ↔ y ∈ image r x
Tactic:
simp only [mem_image_iff, mem_preimage_iff, mem_inverse_iff]
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ (∃ z, z ∈ x ∧ ∃ y_1 z_1, opair y z = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ ∃ z, z ∈ x ∧ opair z y ∈ r
Theorem: SetTheory.preimage_inverse
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ (∃ z, z ∈ x ∧ ∃ y_1 z_1, opair y z = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ ∃ z, z ∈ x ∧ opair z y ∈ r
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_memRComp'
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 s r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memRComp x s r) v l ↔
    ∃ a b c, interpretTerm V v l x = opair a c ∧ opair b c ∈ interpretTerm V v l s ∧ opair a b ∈ interpretTerm V v l r
Tactic:
unfold BoundedFormula.memRComp
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 s r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.exists
            (BoundedFormula.exists
              (BoundedFormula.exists
                (BoundedFormula.and
                  (BoundedFormula.and
                    (BoundedFormula.and
                      (BoundedFormula.and
                        (BoundedFormula.eqOPair (termSucc (termSucc (termSucc (termSucc (termSucc x)))))
                          (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                          (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))
                        (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.eqOPair (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                        (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) })
                        (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) })))
                    (BoundedFormula.mem (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                      (termSucc (termSucc (termSucc (termSucc (termSucc s)))))))
                  (BoundedFormula.mem (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                    (termSucc (termSucc (termSucc (termSucc (termSucc r))))))))))))
      v l ↔
    ∃ a b c, interpretTerm V v l x = opair a c ∧ opair b c ∈ interpretTerm V v l s ∧ opair a b ∈ interpretTerm V v l r
Theorem: SetTheory.interpret_memRComp'
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 s r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.exists
            (BoundedFormula.exists
              (BoundedFormula.exists
                (BoundedFormula.and
                  (BoundedFormula.and
                    (BoundedFormula.and
                      (BoundedFormula.and
                        (BoundedFormula.eqOPair (termSucc (termSucc (termSucc (termSucc (termSucc x)))))
                          (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                          (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))
                        (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.eqOPair (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                        (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) })
                        (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) })))
                    (BoundedFormula.mem (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                      (termSucc (termSucc (termSucc (termSucc (termSucc s)))))))
                  (BoundedFormula.mem (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                    (termSucc (termSucc (termSucc (termSucc (termSucc r))))))))))))
      v l ↔
    ∃ a b c, interpretTerm V v l x = opair a c ∧ opair b c ∈ interpretTerm V v l s ∧ opair a b ∈ interpretTerm V v l r
Tactic:
simp [and_assoc]
Proof state after:
no goals
Theorem: SetTheory.mem_rcomp_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ x ∈ rcomp s r ↔ ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
unfold rcomp
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ x ∈
      sep (BoundedFormula.memRComp (Sum.inr 0) (Sum.inl true) (Sum.inl false)) (fun i => if i = true then s else r)
        (prod (dom r) (ran s)) ↔
    ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r
Theorem: SetTheory.mem_rcomp_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ x ∈
      sep (BoundedFormula.memRComp (Sum.inr 0) (Sum.inl true) (Sum.inl false)) (fun i => if i = true then s else r)
        (prod (dom r) (ran s)) ↔
    ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
simp only [mem_sep_iff, interpret_memRComp', interpret_inr, interpret_inl, ite_true, ite_false,
  and_iff_right_iff_imp, forall_exists_index, and_imp]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ ∀ (x_1 x_2 x_3 : V), x = opair x_1 x_3 → opair x_2 x_3 ∈ s → opair x_1 x_2 ∈ r → x ∈ prod (dom r) (ran s)
Theorem: SetTheory.mem_rcomp_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ ∀ (x_1 x_2 x_3 : V), x = opair x_1 x_3 → opair x_2 x_3 ∈ s → opair x_1 x_2 ∈ r → x ∈ prod (dom r) (ran s)
Tactic:
rintro a b c rfl hs hr
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ opair a c ∈ prod (dom r) (ran s)
Theorem: SetTheory.mem_rcomp_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ opair a c ∈ prod (dom r) (ran s)
Tactic:
rw [mem_prod_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ a_1, a_1 ∈ dom r ∧ ∃ b, b ∈ ran s ∧ opair a c = opair a_1 b
Theorem: SetTheory.mem_rcomp_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ a_1, a_1 ∈ dom r ∧ ∃ b, b ∈ ran s ∧ opair a c = opair a_1 b
Tactic:
refine ⟨a, ?_, c, ?_, rfl⟩
Proof state after:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ a ∈ dom r

case refine_2
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ c ∈ ran s
Theorem: SetTheory.mem_rcomp_iff
Proof state before:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ a ∈ dom r
Tactic:
rw [mem_dom_iff]
Proof state after:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ z, opair a z ∈ r
Theorem: SetTheory.mem_rcomp_iff
Proof state before:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ z, opair a z ∈ r
Tactic:
exact ⟨b, hr⟩
Proof state after:
no goals
Theorem: SetTheory.mem_rcomp_iff
Proof state before:
case refine_2
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ c ∈ ran s
Tactic:
rw [mem_ran_iff]
Proof state after:
case refine_2
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ z, opair z c ∈ s
Theorem: SetTheory.mem_rcomp_iff
Proof state before:
case refine_2
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ z, opair z c ∈ s
Tactic:
exact ⟨b, hs⟩
Proof state after:
no goals
Theorem: SetTheory.opair_mem_rcomp_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a c s : V
⊢ opair a c ∈ rcomp s r ↔ ∃ b, opair b c ∈ s ∧ opair a b ∈ r
Tactic:
rw [mem_rcomp_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z a c s : V
⊢ (∃ a_1 b c_1, opair a c = opair a_1 c_1 ∧ opair b c_1 ∈ s ∧ opair a_1 b ∈ r) ↔ ∃ b, opair b c ∈ s ∧ opair a b ∈ r
Theorem: SetTheory.opair_mem_rcomp_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z a c s : V
⊢ (∃ a_1 b c_1, opair a c = opair a_1 c_1 ∧ opair b c_1 ∈ s ∧ opair a_1 b ∈ r) ↔ ∃ b, opair b c ∈ s ∧ opair a b ∈ r
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_memRComp
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 s r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memRComp x s r) v l ↔
    interpretTerm V v l x ∈ rcomp (interpretTerm V v l s) (interpretTerm V v l r)
Tactic:
rw [mem_rcomp_iff, interpret_memRComp']
Proof state after:
no goals
Theorem: SetTheory.rcomp_assoc
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z t s : V
⊢ rcomp (rcomp t s) r = rcomp t (rcomp s r)
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z t s z✝ : V
⊢ z✝ ∈ rcomp (rcomp t s) r ↔ z✝ ∈ rcomp t (rcomp s r)
Theorem: SetTheory.rcomp_assoc
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z t s z✝ : V
⊢ z✝ ∈ rcomp (rcomp t s) r ↔ z✝ ∈ rcomp t (rcomp s r)
Tactic:
simp only [mem_rcomp_iff]
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z t s z✝ : V
⊢ (∃ a b c,
      z✝ = opair a c ∧ (∃ a b_1 c_1, opair b c = opair a c_1 ∧ opair b_1 c_1 ∈ t ∧ opair a b_1 ∈ s) ∧ opair a b ∈ r) ↔
    ∃ a b c, z✝ = opair a c ∧ opair b c ∈ t ∧ ∃ a_1 b_1 c, opair a b = opair a_1 c ∧ opair b_1 c ∈ s ∧ opair a_1 b_1 ∈ r
Theorem: SetTheory.rcomp_assoc
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z t s z✝ : V
⊢ (∃ a b c,
      z✝ = opair a c ∧ (∃ a b_1 c_1, opair b c = opair a c_1 ∧ opair b_1 c_1 ∈ t ∧ opair a b_1 ∈ s) ∧ opair a b ∈ r) ↔
    ∃ a b c, z✝ = opair a c ∧ opair b c ∈ t ∧ ∃ a_1 b_1 c, opair a b = opair a_1 c ∧ opair b_1 c ∈ s ∧ opair a_1 b_1 ∈ r
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.rcomp_isRelation
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
hr : IsRelation r
⊢ IsRelation (rcomp s r)
Tactic:
intro x hx
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x✝ y z s : V
hr : IsRelation r
x : V
hx : x ∈ rcomp s r
⊢ IsOPair x
Theorem: SetTheory.rcomp_isRelation
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y z s : V
hr : IsRelation r
x : V
hx : x ∈ rcomp s r
⊢ IsOPair x
Tactic:
rw [mem_rcomp_iff] at hx
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x✝ y z s : V
hr : IsRelation r
x : V
hx : ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r
⊢ IsOPair x
Theorem: SetTheory.rcomp_isRelation
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y z s : V
hr : IsRelation r
x : V
hx : ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r
⊢ IsOPair x
Tactic:
aesop
Proof state after:
no goals