α : Type u_2
β : Type ?u.8826
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_1
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')
α : Type u_2
β : Type ?u.8826
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_1
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'
dsimp [GameAdd.fix]
no goals
α : Type u_2
β : Type ?u.8826
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_1
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')
exact WellFounded.fix_eq _ _ _