case mp
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y → rα x.fst y.fst ∧ x.snd = y.snd ∨ rβ x.snd y.snd ∧ x.fst = y.fst

case mpr
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ rα x.fst y.fst ∧ x.snd = y.snd ∨ rβ x.snd y.snd ∧ x.fst = y.fst → GameAdd rα rβ x y
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y ↔ rα x.fst y.fst ∧ x.snd = y.snd ∨ rβ x.snd y.snd ∧ x.fst = y.fst
constructor
case mp.fst
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ : α
b : β
h : rα a₁ a₂
⊢ rα (a₁, b).fst (a₂, b).fst ∧ (a₁, b).snd = (a₂, b).snd ∨ rβ (a₁, b).snd (a₂, b).snd ∧ (a₁, b).fst = (a₂, b).fst

case mp.snd
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a : α
b₁ b₂ : β
h : rβ b₁ b₂
⊢ rα (a, b₁).fst (a, b₂).fst ∧ (a, b₁).snd = (a, b₂).snd ∨ rβ (a, b₁).snd (a, b₂).snd ∧ (a, b₁).fst = (a, b₂).fst
case mp
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y → rα x.fst y.fst ∧ x.snd = y.snd ∨ rβ x.snd y.snd ∧ x.fst = y.fst
rintro (@⟨a₁, a₂, b, h⟩ | @⟨a, b₁, b₂, h⟩)
no goals
case mp.fst
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ : α
b : β
h : rα a₁ a₂
⊢ rα (a₁, b).fst (a₂, b).fst ∧ (a₁, b).snd = (a₂, b).snd ∨ rβ (a₁, b).snd (a₂, b).snd ∧ (a₁, b).fst = (a₂, b).fst

case mp.snd
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a : α
b₁ b₂ : β
h : rβ b₁ b₂
⊢ rα (a, b₁).fst (a, b₂).fst ∧ (a, b₁).snd = (a, b₂).snd ∨ rβ (a, b₁).snd (a, b₂).snd ∧ (a, b₁).fst = (a, b₂).fst
exacts [Or.inl ⟨h, rfl⟩, Or.inr ⟨h, rfl⟩]
case mpr
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
⊢ ∀ {x y : α × β}, rα x.fst y.fst ∧ x.snd = y.snd ∨ rβ x.snd y.snd ∧ x.fst = y.fst → GameAdd rα rβ x y
case mpr
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ rα x.fst y.fst ∧ x.snd = y.snd ∨ rβ x.snd y.snd ∧ x.fst = y.fst → GameAdd rα rβ x y
revert x y
case mpr.mk.mk.inl.intro
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ : β
a₂ : α
h : rα (a₁, b₁).fst (a₂, b₁).fst
⊢ GameAdd rα rβ (a₁, b₁) (a₂, b₁)

case mpr.mk.mk.inr.intro
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ b₂ : β
h : rβ (a₁, b₁).snd (a₁, b₂).snd
⊢ GameAdd rα rβ (a₁, b₁) (a₁, b₂)
case mpr
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
⊢ ∀ {x y : α × β}, rα x.fst y.fst ∧ x.snd = y.snd ∨ rβ x.snd y.snd ∧ x.fst = y.fst → GameAdd rα rβ x y
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (⟨h, rfl : b₁ = b₂⟩ | ⟨h, rfl : a₁ = a₂⟩)
no goals
case mpr.mk.mk.inl.intro
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ : β
a₂ : α
h : rα (a₁, b₁).fst (a₂, b₁).fst
⊢ GameAdd rα rβ (a₁, b₁) (a₂, b₁)

case mpr.mk.mk.inr.intro
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ b₂ : β
h : rβ (a₁, b₁).snd (a₁, b₂).snd
⊢ GameAdd rα rβ (a₁, b₁) (a₁, b₂)
exacts [GameAdd.fst h, GameAdd.snd h]