internlm/Lean-Github huggingface dataset:
Theorem: SetTheory.Function.ext
Proof state before:
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
Tactic:
cases this
Proof state after:
case mk.refl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
g : a ⟶ b
isFunction✝ : IsFunction g.1
dom_eq✝ : dom g.1 = a
ran_subset✝ : ran g.1 ⊆ b
h :
  ∀ (x : V),
    x ∈ a →
      apply { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph x =
        apply g.graph x
⊢ { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ } = g
Theorem: SetTheory.Function.ext
Proof state before:
case mk.refl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
g : a ⟶ b
isFunction✝ : IsFunction g.1
dom_eq✝ : dom g.1 = a
ran_subset✝ : ran g.1 ⊆ b
h :
  ∀ (x : V),
    x ∈ a →
      apply { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph x =
        apply g.graph x
⊢ { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ } = g
Tactic:
rfl
Proof state after:
no goals
Theorem: SetTheory.Function.ext
Proof state before:
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
Tactic:
intro hx
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
hx : x ∈ f.graph
⊢ x ∈ g.graph
Theorem: SetTheory.Function.ext
Proof state before:
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
hx : x ∈ f.graph
⊢ x ∈ g.graph
Tactic:
obtain ⟨x, y, rfl⟩ := f.isFunction.1 x hx
Proof state after:
case h.mp.intro.intro
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 y : V
hx : opair x y ∈ f.graph
⊢ opair x y ∈ g.graph
Theorem: SetTheory.Function.ext
Proof state before:
case h.mp.intro.intro
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 y : V
hx : opair x y ∈ f.graph
⊢ opair x y ∈ g.graph
Tactic:
have : x ∈ a := by
  refine mem_of_mem_dom f ?_
  rw [mem_dom_iff]
  exact ⟨y, hx⟩
Proof state after:
case h.mp.intro.intro
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 y : V
hx : opair x y ∈ f.graph
this : x ∈ a
⊢ opair x y ∈ g.graph
Theorem: SetTheory.Function.ext
Proof state before:
case h.mp.intro.intro
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 y : V
hx : opair x y ∈ f.graph
this : x ∈ a
⊢ opair x y ∈ g.graph
Tactic:
rw [opair_mem_graph_iff _ this] at hx ⊢
Proof state after:
case h.mp.intro.intro
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 y : V
hx : y = apply f.graph x
this : x ∈ a
⊢ y = apply g.graph x
Theorem: SetTheory.Function.ext
Proof state before:
case h.mp.intro.intro
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 y : V
hx : y = apply f.graph x
this : x ∈ a
⊢ y = apply g.graph x
Tactic:
rw [hx]
Proof state after:
case h.mp.intro.intro
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 y : V
hx : y = apply f.graph x
this : x ∈ a
⊢ apply f.graph x = apply g.graph x
Theorem: SetTheory.Function.ext
Proof state before:
case h.mp.intro.intro
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 y : V
hx : y = apply f.graph x
this : x ∈ a
⊢ apply f.graph x = apply g.graph x
Tactic:
exact h _ this
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
x y : V
hx : opair x y ∈ f.graph
⊢ x ∈ a
Tactic:
refine mem_of_mem_dom f ?_
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
x y : V
hx : opair x y ∈ f.graph
⊢ x ∈ dom 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
x y : V
hx : opair x y ∈ f.graph
⊢ x ∈ dom f.graph
Tactic:
rw [mem_dom_iff]
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
x y : V
hx : opair x y ∈ f.graph
⊢ ∃ z, opair x z ∈ 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
x y : V
hx : opair x y ∈ f.graph
⊢ ∃ z, opair x z ∈ f.graph
Tactic:
exact ⟨y, hx⟩
Proof state after:
no goals
Theorem: SetTheory.Function.ext
Proof state before:
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
Tactic:
intro hx
Proof state after:
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
hx : x ∈ g.graph
⊢ x ∈ f.graph
Theorem: SetTheory.Function.ext
Proof state before:
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
hx : x ∈ g.graph
⊢ x ∈ f.graph
Tactic:
obtain ⟨x, y, rfl⟩ := g.isFunction.1 x hx
Proof state after:
case h.mpr.intro.intro
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 y : V
hx : opair x y ∈ g.graph
⊢ opair x y ∈ f.graph
Theorem: SetTheory.Function.ext
Proof state before:
case h.mpr.intro.intro
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 y : V
hx : opair x y ∈ g.graph
⊢ opair x y ∈ f.graph
Tactic:
have : x ∈ a := by
  refine mem_of_mem_dom g ?_
  rw [mem_dom_iff]
  exact ⟨y, hx⟩
Proof state after:
case h.mpr.intro.intro
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 y : V
hx : opair x y ∈ g.graph
this : x ∈ a
⊢ opair x y ∈ f.graph
Theorem: SetTheory.Function.ext
Proof state before:
case h.mpr.intro.intro
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 y : V
hx : opair x y ∈ g.graph
this : x ∈ a
⊢ opair x y ∈ f.graph
Tactic:
rw [opair_mem_graph_iff _ this] at hx ⊢
Proof state after:
case h.mpr.intro.intro
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 y : V
hx : y = apply g.graph x
this : x ∈ a
⊢ y = apply f.graph x
Theorem: SetTheory.Function.ext
Proof state before:
case h.mpr.intro.intro
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 y : V
hx : y = apply g.graph x
this : x ∈ a
⊢ y = apply f.graph x
Tactic:
rw [hx]
Proof state after:
case h.mpr.intro.intro
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 y : V
hx : y = apply g.graph x
this : x ∈ a
⊢ apply g.graph x = apply f.graph x
Theorem: SetTheory.Function.ext
Proof state before:
case h.mpr.intro.intro
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 y : V
hx : y = apply g.graph x
this : x ∈ a
⊢ apply g.graph x = apply f.graph x
Tactic:
exact (h _ this).symm
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
x y : V
hx : opair x y ∈ g.graph
⊢ x ∈ a
Tactic:
refine mem_of_mem_dom g ?_
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
x y : V
hx : opair x y ∈ g.graph
⊢ x ∈ dom 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
x y : V
hx : opair x y ∈ g.graph
⊢ x ∈ dom g.graph
Tactic:
rw [mem_dom_iff]
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
x y : V
hx : opair x y ∈ g.graph
⊢ ∃ z, opair x z ∈ 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
x y : V
hx : opair x y ∈ g.graph
⊢ ∃ z, opair x z ∈ g.graph
Tactic:
exact ⟨y, hx⟩
Proof state after:
no goals
Theorem: SetTheory.mem_π₂_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈ π₂ x ↔ ∃ z, y ∈ z ∧ z ∈ ⋃ x ∧ (⋃ x ≠ ⋂ x → ¬z ∈ ⋂ x)
Tactic:
unfold π₂
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈
      ⋃
        sep
          (BoundedFormula.imp (BoundedFormula.ne (Sum.inl true) (Sum.inl false))
            (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inl false))))
          (fun i => if i = true then ⋃ x else ⋂ x) (⋃ x) ↔
    ∃ z, y ∈ z ∧ z ∈ ⋃ x ∧ (⋃ x ≠ ⋂ x → ¬z ∈ ⋂ x)
Theorem: SetTheory.mem_π₂_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈
      ⋃
        sep
          (BoundedFormula.imp (BoundedFormula.ne (Sum.inl true) (Sum.inl false))
            (BoundedFormula.not (BoundedFormula.mem (Sum.inr 0) (Sum.inl false))))
          (fun i => if i = true then ⋃ x else ⋂ x) (⋃ x) ↔
    ∃ z, y ∈ z ∧ z ∈ ⋃ x ∧ (⋃ x ≠ ⋂ x → ¬z ∈ ⋂ x)
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.π₁_opair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ π₁ (opair x y) = x
Tactic:
unfold π₁ opair
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ⋃ ⋂ pair {x} (pair x y) = x
Theorem: SetTheory.π₁_opair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ⋃ ⋂ pair {x} (pair x y) = x
Tactic:
ext z
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ ⋃ ⋂ pair {x} (pair x y) ↔ z ∈ x
Theorem: SetTheory.π₁_opair
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ ⋃ ⋂ pair {x} (pair x y) ↔ z ∈ x
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.π₂_opair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ π₂ (opair x y) = y
Tactic:
unfold opair
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ π₂ (pair {x} (pair x y)) = y
Theorem: SetTheory.π₂_opair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ π₂ (pair {x} (pair x y)) = y
Tactic:
ext z
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ π₂ (pair {x} (pair x y)) ↔ z ∈ y
Theorem: SetTheory.π₂_opair
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ π₂ (pair {x} (pair x y)) ↔ z ∈ y
Tactic:
rw [mem_π₂_iff]
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1,
      z ∈ z_1 ∧
        z_1 ∈ ⋃ pair {x} (pair x y) ∧ (⋃ pair {x} (pair x y) ≠ ⋂ pair {x} (pair x y) → ¬z_1 ∈ ⋂ pair {x} (pair x y))) ↔
    z ∈ y
Theorem: SetTheory.π₂_opair
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1,
      z ∈ z_1 ∧
        z_1 ∈ ⋃ pair {x} (pair x y) ∧ (⋃ pair {x} (pair x y) ≠ ⋂ pair {x} (pair x y) → ¬z_1 ∈ ⋂ pair {x} (pair x y))) ↔
    z ∈ y
Tactic:
simp only [sUnion_pair, sInter_pair, ne_eq, union_pair_eq_inter_pair]
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)) ↔ z ∈ y
Theorem: SetTheory.π₂_opair
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)) ↔ z ∈ y
Tactic:
constructor
Proof state after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)) → z ∈ y

case h.mpr
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ y → ∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)
Theorem: SetTheory.π₂_opair
Proof state before:
case h.mp
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)) → z ∈ y
Tactic:
rintro ⟨s, hzs, hsx, hs⟩
Proof state after:
case h.mp.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
⊢ z ∈ y
Theorem: SetTheory.π₂_opair
Proof state before:
case h.mp.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
⊢ z ∈ y
Tactic:
by_cases h : s = y
Proof state after:
case pos
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
h : s = y
⊢ z ∈ y

case neg
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
h : ¬s = y
⊢ z ∈ y
Theorem: SetTheory.π₂_opair
Proof state before:
case pos
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
h : s = y
⊢ z ∈ y
Tactic:
subst h
Proof state after:
case pos
V : Type u_1
inst✝ : Zermelo V
x z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x s
hs : ¬x = s → ¬s ∈ {x} ∩ pair x s
⊢ z ∈ s
Theorem: SetTheory.π₂_opair
Proof state before:
case pos
V : Type u_1
inst✝ : Zermelo V
x z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x s
hs : ¬x = s → ¬s ∈ {x} ∩ pair x s
⊢ z ∈ s
Tactic:
exact hzs
Proof state after:
no goals
Theorem: SetTheory.π₂_opair
Proof state before:
case neg
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
h : ¬s = y
⊢ z ∈ y
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.π₂_opair
Proof state before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ y → ∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.opair_injective
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
⊢ opair x y = opair z w ↔ x = z ∧ y = w
Tactic:
constructor
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
⊢ opair x y = opair z w → x = z ∧ y = w

case mpr
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
⊢ x = z ∧ y = w → opair x y = opair z w
Theorem: SetTheory.opair_injective
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
⊢ opair x y = opair z w → x = z ∧ y = w
Tactic:
intro h
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
h : opair x y = opair z w
⊢ x = z ∧ y = w
Theorem: SetTheory.opair_injective
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
h : opair x y = opair z w
⊢ x = z ∧ y = w
Tactic:
have h₁ := congrArg π₁ h
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
h : opair x y = opair z w
h₁ : π₁ (opair x y) = π₁ (opair z w)
⊢ x = z ∧ y = w
Theorem: SetTheory.opair_injective
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
h : opair x y = opair z w
h₁ : π₁ (opair x y) = π₁ (opair z w)
⊢ x = z ∧ y = w
Tactic:
have h₂ := congrArg π₂ h
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
h : opair x y = opair z w
h₁ : π₁ (opair x y) = π₁ (opair z w)
h₂ : π₂ (opair x y) = π₂ (opair z w)
⊢ x = z ∧ y = w
Theorem: SetTheory.opair_injective
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
h : opair x y = opair z w
h₁ : π₁ (opair x y) = π₁ (opair z w)
h₂ : π₂ (opair x y) = π₂ (opair z w)
⊢ x = z ∧ y = w
Tactic:
simp at h₁ h₂
Proof state after:
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
h : opair x y = opair z w
h₁ : x = z
h₂ : y = w
⊢ x = z ∧ y = w
Theorem: SetTheory.opair_injective
Proof state before:
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
h : opair x y = opair z w
h₁ : x = z
h₂ : y = w
⊢ x = z ∧ y = w
Tactic:
exact ⟨h₁, h₂⟩
Proof state after:
no goals
Theorem: SetTheory.opair_injective
Proof state before:
case mpr
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
⊢ x = z ∧ y = w → opair x y = opair z w
Tactic:
rintro ⟨rfl, rfl⟩
Proof state after:
case mpr.intro
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z x y : V
⊢ opair x y = opair x y
Theorem: SetTheory.opair_injective
Proof state before:
case mpr.intro
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z x y : V
⊢ opair x y = opair x y
Tactic:
rfl
Proof state after:
no goals
Theorem: SetTheory.eq_pair_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x = pair y z ↔ ∀ (t : V), t ∈ x ↔ t = y ∨ t = z
Tactic:
rw [ext_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ (∀ (z_1 : V), z_1 ∈ x ↔ z_1 ∈ pair y z) ↔ ∀ (t : V), t ∈ x ↔ t = y ∨ t = z
Theorem: SetTheory.eq_pair_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ (∀ (z_1 : V), z_1 ∈ x ↔ z_1 ∈ pair y z) ↔ ∀ (t : V), t ∈ x ↔ t = y ∨ t = z
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.interpret_eqPair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqPair x y z) v l ↔
    interpretTerm V v l x = pair (interpretTerm V v l y) (interpretTerm V v l z)
Tactic:
unfold BoundedFormula.eqPair
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : 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.eq (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    interpretTerm V v l x = pair (interpretTerm V v l y) (interpretTerm V v l z)
Theorem: SetTheory.interpret_eqPair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : 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.eq (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    interpretTerm V v l x = pair (interpretTerm V v l y) (interpretTerm V v l z)
Tactic:
rw [eq_pair_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : 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.eq (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    ∀ (t : V), t ∈ interpretTerm V v l x ↔ t = interpretTerm V v l y ∨ t = interpretTerm V v l z
Theorem: SetTheory.interpret_eqPair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : 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.eq (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    ∀ (t : V), t ∈ interpretTerm V v l x ↔ t = interpretTerm V v l y ∨ t = interpretTerm V v l z
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.interpret_eqSingleton
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqSingleton x y) v l ↔ interpretTerm V v l x = {interpretTerm V v l y}
Tactic:
unfold BoundedFormula.eqSingleton
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqPair x y y) v l ↔ interpretTerm V v l x = {interpretTerm V v l y}
Theorem: SetTheory.interpret_eqSingleton
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqPair x y y) v l ↔ interpretTerm V v l x = {interpretTerm V v l y}
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.interpret_isPair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isPair x) v l ↔ IsPair (interpretTerm V v l x)
Tactic:
unfold BoundedFormula.isPair IsPair
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.eqPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
            (Sum.inr (Fin.last (n + 1))))))
      v l ↔
    ∃ y z, interpretTerm V v l x = pair y z
Theorem: SetTheory.interpret_isPair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.eqPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
            (Sum.inr (Fin.last (n + 1))))))
      v l ↔
    ∃ y z, interpretTerm V v l x = pair y z
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.interpret_eqOPair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqOPair x y z) v l ↔
    interpretTerm V v l x = opair (interpretTerm V v l y) (interpretTerm V v l z)
Tactic:
unfold BoundedFormula.eqOPair opair
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.and
              (BoundedFormula.eqSingleton (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc y)))
              (BoundedFormula.eqPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc y)) (termSucc (termSucc z))))
            (BoundedFormula.eqPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
              (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })))))
      v l ↔
    interpretTerm V v l x = pair {interpretTerm V v l y} (pair (interpretTerm V v l y) (interpretTerm V v l z))