Theorem: SetTheory.opair_injective (SetTheory/OPair.lean)

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
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

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
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

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
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

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
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

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₂
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

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₂⟩
State after:
no goals

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⟩
State after:
case mpr.intro
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z x y : V
⊢ opair x y = opair x y

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
State after:
no goals