case intro
α : Type u_1
β : Type ?u.6233
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))
α : Type u_1
β : Type ?u.6233
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))
induction' ha with a _ iha generalizing b
case intro.intro
α : Type u_1
β : Type ?u.6233
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))
case intro
α : Type u_1
β : Type ?u.6233
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))
induction' hb with b hb ihb
case intro.intro
α : Type u_1
β : Type ?u.6233
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
case intro.intro
α : Type u_1
β : Type ?u.6233
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))
refine' Acc.intro _ fun s => _
case intro.intro.hf
α : Type u_1
β : Type ?u.6233
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))
case intro.intro
α : Type u_1
β : Type ?u.6233
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
induction' s using Sym2.inductionOn with c d
case intro.intro.hf
α : Type u_1
β : Type ?u.6233
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))
case intro.intro.hf
α : Type u_1
β : Type ?u.6233
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))
rw [Sym2.GameAdd]
case intro.intro.hf
α : Type u_1
β : Type ?u.6233
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))
case intro.intro.hf
α : Type u_1
β : Type ?u.6233
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))
dsimp
case intro.intro.hf.inl.fst
α : Type u_1
β : Type ?u.6233
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))

case intro.intro.hf.inl.snd
α : Type u_1
β : Type ?u.6233
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))

case intro.intro.hf.inr.fst
α : Type u_1
β : Type ?u.6233
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))

case intro.intro.hf.inr.snd
α : Type u_1
β : Type ?u.6233
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))
case intro.intro.hf
α : Type u_1
β : Type ?u.6233
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))
rintro ((rc | rd) | (rd | rc))
no goals
case intro.intro.hf.inl.fst
α : Type u_1
β : Type ?u.6233
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))
exact iha c rc ⟨b, hb⟩
no goals
case intro.intro.hf.inl.snd
α : Type u_1
β : Type ?u.6233
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))
exact ihb d rd
case intro.intro.hf.inr.fst
α : Type u_1
β : Type ?u.6233
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))
case intro.intro.hf.inr.fst
α : Type u_1
β : Type ?u.6233
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))
rw [Sym2.eq_swap]
no goals
case intro.intro.hf.inr.fst
α : Type u_1
β : Type ?u.6233
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))
exact iha d rd ⟨b, hb⟩
case intro.intro.hf.inr.snd
α : Type u_1
β : Type ?u.6233
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))
case intro.intro.hf.inr.snd
α : Type u_1
β : Type ?u.6233
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))
rw [Sym2.eq_swap]
no goals
case intro.intro.hf.inr.snd
α : Type u_1
β : Type ?u.6233
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))
exact ihb c rc