[GOAL]
α : 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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rintro (@⟨a₁, a₂, b, h⟩ | @⟨a, b₁, b₂, h⟩)
[GOAL]
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
[PROOFSTEP]
exacts [Or.inl ⟨h, rfl⟩, Or.inr ⟨h, rfl⟩]
[GOAL]
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
[PROOFSTEP]
revert x y
[GOAL]
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
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (⟨h, rfl : b₁ = b₂⟩ | ⟨h, rfl : a₁ = a₂⟩)
[GOAL]
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₂)
[PROOFSTEP]
exacts [GameAdd.fst h, GameAdd.snd h]
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ GameAdd rβ rα (swap (a₁, b₁)) (swap (a₂, b₂)) ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
⊢ ∀ {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β}, rα a₁ a₂ → rβ b₁ b₂ → Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
intro _ _ _ _ hα hβ
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
a₁✝ : α
b₁✝ : β
a₂✝ : α
b₂✝ : β
hα : rα a₁✝ a₂✝
hβ : rβ b₁✝ b₂✝
⊢ Relation.TransGen (GameAdd rα rβ) (a₁✝, b₁✝) (a₂✝, b₂✝)
[PROOFSTEP]
exact Relation.TransGen.tail (Relation.TransGen.single $ GameAdd.fst hα) (GameAdd.snd hβ)
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a : α
b : β
ha : Acc rα a
hb : Acc rβ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
[PROOFSTEP]
induction' ha with a _ iha generalizing b
[GOAL]
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ : α
b✝ : β
hb✝ : Acc rβ b✝
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b : β
hb : Acc rβ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
[PROOFSTEP]
induction' hb with b hb ihb
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ : α
b✝¹ : β
hb✝ : Acc rβ b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
[PROOFSTEP]
refine' Acc.intro _ fun h => _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ : α
b✝¹ : β
hb✝ : Acc rβ b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
h : α × β
⊢ Prod.GameAdd rα rβ h (a, b) → Acc (Prod.GameAdd rα rβ) h
[PROOFSTEP]
rintro (⟨ra⟩ | ⟨rb⟩)
[GOAL]
case intro.intro.fst
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ : α
b✝¹ : β
hb✝ : Acc rβ b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
a₁✝ : α
ra : rα a₁✝ a
⊢ Acc (Prod.GameAdd rα rβ) (a₁✝, b)
case intro.intro.snd
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ : α
b✝¹ : β
hb✝ : Acc rβ b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
b₁✝ : β
rb : rβ b₁✝ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b₁✝)
[PROOFSTEP]
exacts [iha _ ra (Acc.intro b hb), ihb _ rb]
[GOAL]
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ : β → β → Prop
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂ b₂ =
      (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁ a₂ b₂ ∧
    (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂ b₂ =
      (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ b₂ a₂
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ : β → β → Prop
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (a₁, b₁) (b₂, a₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (b₂, a₂))
[PROOFSTEP]
rw [Prod.gameAdd_swap_swap_mk _ _ b₁ b₂ a₁ a₂, Prod.gameAdd_swap_swap_mk _ _ a₁ b₂ b₁ a₂]
[GOAL]
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ : β → β → Prop
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂))
[PROOFSTEP]
simp [or_comm]
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rintro ⟨_, _⟩ ⟨_, _⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
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✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (a₁, b)) (Quotient.mk (Rel.setoid α) (b, a₂))
[PROOFSTEP]
rw [Sym2.eq_swap]
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (b, a₁)) (Quotient.mk (Rel.setoid α) (b, a₂))
[PROOFSTEP]
exact GameAdd.snd h
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (b, a₁)) (Quotient.mk (Rel.setoid α) (a₂, b))
[PROOFSTEP]
rw [Sym2.eq_swap]
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (a₁, b)) (Quotient.mk (Rel.setoid α) (a₂, b))
[PROOFSTEP]
exact GameAdd.fst h
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a b : α
ha : Acc rα a
hb : Acc rα b
⊢ Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, b))
[PROOFSTEP]
induction' ha with a _ iha generalizing b
[GOAL]
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝ : α
hb✝ : Acc rα b✝
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b : α
hb : Acc rα b
⊢ Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, b))
[PROOFSTEP]
induction' hb with b hb ihb
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
⊢ Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, b))
[PROOFSTEP]
refine' Acc.intro _ fun s => _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
s : Sym2 α
⊢ Sym2.GameAdd rα s (Quotient.mk (Sym2.Rel.setoid α) (a, b)) → Acc (Sym2.GameAdd rα) s
[PROOFSTEP]
induction' s using Sym2.inductionOn with c d
[GOAL]
case intro.intro.hf
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c d : α
⊢ Sym2.GameAdd rα (Quotient.mk (Sym2.Rel.setoid α) (c, d)) (Quotient.mk (Sym2.Rel.setoid α) (a, b)) →
    Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (c, d))
[PROOFSTEP]
rw [Sym2.GameAdd]
[GOAL]
case intro.intro.hf
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c d : α
⊢ ↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) }
      (Quotient.mk (Sym2.Rel.setoid α) (c, d)) (Quotient.mk (Sym2.Rel.setoid α) (a, b)) →
    Acc
      (↑Sym2.lift₂
        { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
          property :=
            (_ :
              ∀ (a₁ b₁ a₂ b₂ : α),
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                      a₂ b₂ =
                    (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁
                      a₁ a₂ b₂ ∧
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                      a₂ b₂ =
                    (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁
                      b₁ b₂ a₂) })
      (Quotient.mk (Sym2.Rel.setoid α) (c, d))
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.hf
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c d : α
⊢ Prod.GameAdd rα rα (c, d) (a, b) ∨ Prod.GameAdd rα rα (d, c) (a, b) →
    Acc
      (↑Sym2.lift₂
        { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
          property :=
            (_ :
              ∀ (a₁ b₁ a₂ b₂ : α),
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                      a₂ b₂ =
                    (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁
                      a₁ a₂ b₂ ∧
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                      a₂ b₂ =
                    (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁
                      b₁ b₂ a₂) })
      (Quotient.mk (Sym2.Rel.setoid α) (c, d))
[PROOFSTEP]
rintro ((rc | rd) | (rd | rc))
[GOAL]
case intro.intro.hf.inl.fst
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c : α
rc : rα c a
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (c, b))
[PROOFSTEP]
exact iha c rc ⟨b, hb⟩
[GOAL]
case intro.intro.hf.inl.snd
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
d : α
rd : rα d b
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (a, d))
[PROOFSTEP]
exact ihb d rd
[GOAL]
case intro.intro.hf.inr.fst
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
d : α
rd : rα d a
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (b, d))
[PROOFSTEP]
rw [Sym2.eq_swap]
[GOAL]
case intro.intro.hf.inr.fst
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
d : α
rd : rα d a
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (d, b))
[PROOFSTEP]
exact iha d rd ⟨b, hb⟩
[GOAL]
case intro.intro.hf.inr.snd
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c : α
rc : rα c b
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (c, a))
[PROOFSTEP]
rw [Sym2.eq_swap]
[GOAL]
case intro.intro.hf.inr.snd
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c : α
rc : rα c b
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (a, c))
[PROOFSTEP]
exact ihb c rc
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH :
  (a₁ b₁ : α) →
    ((a₂ b₂ : α) → GameAdd rα (Quotient.mk (Rel.setoid α) (a₂, b₂)) (Quotient.mk (Rel.setoid α) (a₁, b₁)) → C a₂ b₂) →
      C a₁ b₁
a b : α
⊢ C a b
[PROOFSTEP]
have := hr.sym2_gameAdd
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH :
  (a₁ b₁ : α) →
    ((a₂ b₂ : α) → GameAdd rα (Quotient.mk (Rel.setoid α) (a₂, b₂)) (Quotient.mk (Rel.setoid α) (a₁, b₁)) → C a₂ b₂) →
      C a₁ b₁
a b : α
this : WellFounded (GameAdd rα)
⊢ C a b
[PROOFSTEP]
dsimp only [GameAdd, lift₂, FunLike.coe, EquivLike.coe] at this 
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH :
  (a₁ b₁ : α) →
    ((a₂ b₂ : α) → GameAdd rα (Quotient.mk (Rel.setoid α) (a₂, b₂)) (Quotient.mk (Rel.setoid α) (a₁, b₁)) → C a₂ b₂) →
      C a₁ b₁
a b : α
this :
  WellFounded
    (Quotient.lift₂
      (fun a b => Prod.GameAdd rα rα (a.fst, a.snd) (b.fst, b.snd) ∨ Prod.GameAdd rα rα (a.snd, a.fst) (b.fst, b.snd))
      (_ :
        ∀ (a₁ b₁ a₂ b₂ : α × α),
          a₁ ≈ a₂ →
            b₁ ≈ b₂ →
              (fun a b =>
                    ↑{
                          val := fun a₁ b₁ a₂ b₂ =>
                            Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
                          property :=
                            (_ :
                              ∀ (a₁ b₁ a₂ b₂ : α),
                                (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ a₂ b₂ =
                                    (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      b₁ a₁ a₂ b₂ ∧
                                  (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ a₂ b₂ =
                                    (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ b₂ a₂) }
                      a.fst a.snd b.fst b.snd)
                  a₁ b₁ =
                (fun a b =>
                    ↑{
                          val := fun a₁ b₁ a₂ b₂ =>
                            Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
                          property :=
                            (_ :
                              ∀ (a₁ b₁ a₂ b₂ : α),
                                (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ a₂ b₂ =
                                    (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      b₁ a₁ a₂ b₂ ∧
                                  (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ a₂ b₂ =
                                    (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ b₂ a₂) }
                      a.fst a.snd b.fst b.snd)
                  a₂ b₂))
⊢ C a b
[PROOFSTEP]
exact
  @WellFounded.fix (α × α) (fun x => C x.1 x.2) _ this.of_quotient_lift₂
    (fun ⟨x₁, x₂⟩ IH' => IH x₁ x₂ fun a' b' => IH' ⟨a', b'⟩) (a, b)
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH :
  (a₁ b₁ : α) →
    ((a₂ b₂ : α) → GameAdd rα (Quotient.mk (Rel.setoid α) (a₂, b₂)) (Quotient.mk (Rel.setoid α) (a₁, b₁)) → C a₂ b₂) →
      C a₁ b₁
a b : α
⊢ fix hr IH a b = IH a b fun a' b' x => fix hr IH a' b'
[PROOFSTEP]
dsimp [GameAdd.fix]
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH :
  (a₁ b₁ : α) →
    ((a₂ b₂ : α) → GameAdd rα (Quotient.mk (Rel.setoid α) (a₂, b₂)) (Quotient.mk (Rel.setoid α) (a₁, b₁)) → C a₂ b₂) →
      C a₁ b₁
a b : α
⊢ WellFounded.fix
      (_ :
        WellFounded fun a b =>
          Prod.GameAdd rα rα (a.fst, a.snd) (b.fst, b.snd) ∨ Prod.GameAdd rα rα (a.snd, a.fst) (b.fst, b.snd))
      (fun x IH' => IH x.fst x.snd fun a' b' => IH' (a', b')) (a, b) =
    IH a b fun a' b' x =>
      WellFounded.fix
        (_ :
          WellFounded fun a b =>
            Prod.GameAdd rα rα (a.fst, a.snd) (b.fst, b.snd) ∨ Prod.GameAdd rα rα (a.snd, a.fst) (b.fst, b.snd))
        (fun x IH' => IH x.fst x.snd fun a' b' => IH' (a', b')) (a', b')
[PROOFSTEP]
exact WellFounded.fix_eq _ _ _
