case mk.mk
α : Type u_1
β : Type ?u.5319
rα : α → α → Prop
rβ : β → β → Prop
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (fst✝¹, snd✝¹)) (Quotient.mk (Rel.setoid α) (fst✝, snd✝)) ↔
    Prod.GameAdd rα rα (fst✝¹, snd✝¹) (fst✝, snd✝) ∨ Prod.GameAdd rα rα (Prod.swap (fst✝¹, snd✝¹)) (fst✝, snd✝)
α : Type u_1
β : Type ?u.5319
rα : α → α → Prop
rβ : β → β → Prop
⊢ ∀ {x y : α × α},
    GameAdd rα (Quotient.mk (Rel.setoid α) x) (Quotient.mk (Rel.setoid α) y) ↔
      Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα (Prod.swap x) y
rintro ⟨_, _⟩ ⟨_, _⟩
no goals
case mk.mk
α : Type u_1
β : Type ?u.5319
rα : α → α → Prop
rβ : β → β → Prop
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (fst✝¹, snd✝¹)) (Quotient.mk (Rel.setoid α) (fst✝, snd✝)) ↔
    Prod.GameAdd rα rα (fst✝¹, snd✝¹) (fst✝, snd✝) ∨ Prod.GameAdd rα rα (Prod.swap (fst✝¹, snd✝¹)) (fst✝, snd✝)
rfl