-- Mathlib/FieldTheory/AxGrothendieck.lean
theorem realize_genericPolyMapSurjOnOfInjOn
    [Finite ι] (φ : ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) :
    (K ⊨ genericPolyMapSurjOnOfInjOn φ mons) ↔
      ∀ (v : α → K) (p : { p : ι → MvPolynomial ι K // (∀ i, (p i).support ⊆ mons i) }),
        let f : (ι → K) → (ι → K) := fun v i => eval v (p.1 i)
        let S : Set (ι → K) := fun x => φ.Realize (Sum.elim v x)
        S.MapsTo f S → S.InjOn f → S.SurjOn f S

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
⊢ (∀ (fa : α → K) (fb : (i : ι) × { x // x ∈ mons i } → K),
      (∀ (i : ι → K),
          (Realize φ
              (fun x =>
                Sum.elim
                  (fun a =>
                    Sum.elim
                      (fun x =>
                        Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                      i a)
                  (fun x => default (Fin.castAdd 0 x))
                  (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inl x)) (fun x => Sum.inr x) x)))
              fun x => default (Fin.cast ⋯ x)) →
            Realize φ
              (fun a =>
                Term.realize
                  (fun a =>
                    Sum.elim
                      (fun x =>
                        Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                      i a)
                  (Sum.elim (fun a => var (Sum.inl (Sum.inl a)))
                    (fun i =>
                      Term.relabel (fun i => Sum.elim (fun x => Sum.inl (Sum.inr x)) Sum.inr i)
                        (termOfFreeCommRing (genericPolyMap mons i)))
                    a))
              default) →
        (∀ (a a_1 : ι → K),
            (Realize φ
                (fun x =>
                  Sum.elim
                    (fun a_2 =>
                      Sum.elim
                        (fun x =>
                          Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                            (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                        (Function.uncurry (Fin.cons a (Fin.cons a_1 finZeroElim))) a_2)
                    (fun x => default (Fin.castAdd 0 x))
                    (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inl x)) (fun x => Sum.inr (0, x)) x)))
                fun x => default (Fin.cast ⋯ x)) →
              (Realize φ
                  (fun x =>
                    Sum.elim
                      (fun a_3 =>
                        Sum.elim
                          (fun x =>
                            Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                              (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                          (Function.uncurry (Fin.cons a (Fin.cons a_1 finZeroElim))) a_3)
                      (fun x => default (Fin.castAdd 0 x))
                      (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inl x)) (fun x => Sum.inr (1, x)) x)))
                  fun x => default (Fin.cast ⋯ x)) →
                (∀ (b : ι),
                    Term.realize
                        (fun x =>
                          Sum.elim
                            (fun x =>
                              Sum.elim
                                (fun a_4 =>
                                  Sum.elim
                                    (fun x =>
                                      Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                                        (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                    (Function.uncurry (Fin.cons a (Fin.cons a_1 finZeroElim))) a_4)
                                (fun x => default (Fin.castAdd 0 x))
                                (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inr x)) Sum.inr x)))
                            (fun x => default (Fin.cast ⋯ x))
                            (Sum.inl (Sum.elim (fun x => Sum.inl x) (fun x => Sum.inr (0, x)) x)))
                        (termOfFreeCommRing (genericPolyMap mons b)) =
                      Term.realize
                        (fun x =>
                          Sum.elim
                            (fun x =>
                              Sum.elim
                                (fun a_4 =>
                                  Sum.elim
                                    (fun x =>
                                      Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                                        (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                    (Function.uncurry (Fin.cons a (Fin.cons a_1 finZeroElim))) a_4)
                                (fun x => default (Fin.castAdd 0 x))
                                (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inr x)) Sum.inr x)))
                            (fun x => default (Fin.cast ⋯ x))
                            (Sum.inl (Sum.elim (fun x => Sum.inl x) (fun x => Sum.inr (1, x)) x)))
                        (termOfFreeCommRing (genericPolyMap mons b))) →
                  ∀ (b : ι),
                    Term.realize
                        (Sum.elim
                          (fun x =>
                            Sum.elim
                              (fun a_5 =>
                                Sum.elim
                                  (fun x =>
                                    Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                                      (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                  (Function.uncurry (Fin.cons a (Fin.cons a_1 finZeroElim))) a_5)
                              (fun x => default (Fin.castAdd 0 x))
                              (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inr x)) Sum.inr x)))
                          fun x => default (Fin.cast ⋯ x))
                        (var (Sum.inl (Sum.inr (0, b)))) =
                      Term.realize
                        (Sum.elim
                          (fun x =>
                            Sum.elim
                              (fun a_5 =>
                                Sum.elim
                                  (fun x =>
                                    Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                                      (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                  (Function.uncurry (Fin.cons a (Fin.cons a_1 finZeroElim))) a_5)
                              (fun x => default (Fin.castAdd 0 x))
                              (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inr x)) Sum.inr x)))
                          fun x => default (Fin.cast ⋯ x))
                        (var (Sum.inl (Sum.inr (1, b))))) →
          ∀ (i : ι → K),
            (Realize φ
                (fun x =>
                  Sum.elim
                    (fun a =>
                      Sum.elim
                        (fun x =>
                          Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                            (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                        i a)
                    (fun x => default (Fin.castAdd 0 x))
                    (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inl x)) (fun x => Sum.inr x) x)))
                fun x => default (Fin.cast ⋯ x)) →
              ∃ i_1,
                (Realize φ
                    (fun x =>
                      Sum.elim
                        (fun x =>
                          Sum.elim
                            (Sum.elim
                              (fun a =>
                                Sum.elim
                                  (fun x =>
                                    Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                                      (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                  i a)
                              i_1)
                            (fun x => default (Fin.castAdd 0 x))
                            (Sum.inl
                              (Sum.elim (fun x => Sum.inl (Sum.inl x))
                                (fun i => if i.1 = 0 then Sum.inr i.2 else Sum.inl (Sum.inr i.2)) x)))
                        (fun x => default (Fin.cast ⋯ (Fin.castAdd 0 x)))
                        (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inl x)) (fun x => Sum.inr (0, x)) x)))
                    fun x => default (Fin.cast ⋯ (Fin.cast ⋯ x))) ∧
                  ∀ (b : ι),
                    Term.realize
                        (fun x =>
                          Sum.elim
                            (fun x =>
                              Sum.elim
                                (fun x =>
                                  Sum.elim
                                    (Sum.elim
                                      (fun a =>
                                        Sum.elim
                                          (fun x =>
                                            Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                                              (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                          i a)
                                      i_1)
                                    (fun x => default (Fin.castAdd 0 x))
                                    (Sum.inl
                                      (Sum.elim (fun x => Sum.inl (Sum.inl x))
                                        (fun i => if i.1 = 0 then Sum.inr i.2 else Sum.inl (Sum.inr i.2)) x)))
                                (fun x => default (Fin.cast ⋯ (Fin.castAdd 0 x)))
                                (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inr x)) Sum.inr x)))
                            (fun x => default (Fin.cast ⋯ (Fin.cast ⋯ x)))
                            (Sum.inl (Sum.elim (fun x => Sum.inl x) (fun x => Sum.inr (0, x)) x)))
                        (termOfFreeCommRing (genericPolyMap mons b)) =
                      Term.realize
                        (Sum.elim
                          (fun x =>
                            Sum.elim
                              (fun x =>
                                Sum.elim
                                  (Sum.elim
                                    (fun a =>
                                      Sum.elim
                                        (fun x =>
                                          Sum.elim (fun a => Sum.elim default (fun t => Sum.rec fa fb t) a)
                                            (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                        i a)
                                    i_1)
                                  (fun x => default (Fin.castAdd 0 x))
                                  (Sum.inl
                                    (Sum.elim (fun x => Sum.inl (Sum.inl x))
                                      (fun i => if i.1 = 0 then Sum.inr i.2 else Sum.inl (Sum.inr i.2)) x)))
                              (fun x => default (Fin.cast ⋯ (Fin.castAdd 0 x)))
                              (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inr x)) Sum.inr x)))
                          fun x => default (Fin.cast ⋯ (Fin.cast ⋯ x)))
                        (var (Sum.inl (Sum.inr (1, b))))) ↔
    ∀ (v : α → K) (b : (i : ι) × { x // x ∈ mons i } → K),
      (∀ ⦃x : ι → K⦄,
          Realize φ (Sum.elim v x) default →
            Realize φ (Sum.elim v fun i => (eval x) (↑((mvPolynomialSupportLEEquiv mons).symm b) i)) default) →
        (∀ (x y : ι → K),
            Realize φ (Sum.elim v x) default →
              Realize φ (Sum.elim v y) default →
                (∀ (x_1 : ι),
                    (eval x) (↑((mvPolynomialSupportLEEquiv mons).symm b) x_1) =
                      (eval y) (↑((mvPolynomialSupportLEEquiv mons).symm b) x_1)) →
                  ∀ (x_1 : ι), x x_1 = y x_1) →
          ∀ (x : ι → K),
            Realize φ (Sum.elim v x) default →
              ∃ a,
                Realize φ (Sum.elim v a) default ∧
                  ∀ (x_1 : ι), (eval a) (↑((mvPolynomialSupportLEEquiv mons).symm b) x_1) = x x_1

Tactic:
simp +singlePass only [← Sum.elim_comp_inl_inr]

Result:
ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
⊢ (∀ (fa : ⋯) (fb : ⋯),
      ⋯ →
        ⋯ →
          ∀ (i : ⋯),
            ⋯ →
              ∃ i_1,
                Realize φ
                    (Sum.elim
                      ((fun x =>
                          Sum.elim
                            (Sum.elim
                              ((fun x =>
                                  Sum.elim
                                    (Sum.elim
                                      (Sum.elim
                                          (Sum.elim
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inl)
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inr))
                                          i_1 ∘
                                        Sum.inl)
                                      (Sum.elim
                                          (Sum.elim
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inl)
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inr))
                                          i_1 ∘
                                        Sum.inr))
                                    (fun x => default (Fin.castAdd 0 x))
                                    (Sum.inl
                                      (Sum.elim
                                        (Sum.elim ((fun x => Sum.inl (Sum.inl x)) ∘ Sum.inl)
                                          ((fun x => Sum.inl (Sum.inl x)) ∘ Sum.inr))
                                        (fun i => if i.1 = 0 then Sum.inr i.2 else Sum.inl (Sum.inr i.2)) x))) ∘
                                Sum.inl)
                              ((fun x =>
                                  Sum.elim
                                    (Sum.elim
                                      (Sum.elim
                                          (Sum.elim
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inl)
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inr))
                                          i_1 ∘
                                        Sum.inl)
                                      (Sum.elim
                                          (Sum.elim
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inl)
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inr))
                                          i_1 ∘
                                        Sum.inr))
                                    (fun x => default (Fin.castAdd 0 x))
                                    (Sum.inl
                                      (Sum.elim
                                        (Sum.elim ((fun x => Sum.inl (Sum.inl x)) ∘ Sum.inl)
                                          ((fun x => Sum.inl (Sum.inl x)) ∘ Sum.inr))
                                        (fun i => if i.1 = 0 then Sum.inr i.2 else Sum.inl (Sum.inr i.2)) x))) ∘
                                Sum.inr))
                            (fun x => default (Fin.cast ⋯ (Fin.castAdd 0 x)))
                            (Sum.inl (Sum.elim (fun x => Sum.inl (Sum.inl x)) (fun x => Sum.inr (0, x)) x))) ∘
                        Sum.inl)
                      ((fun x =>
                          Sum.elim
                            (Sum.elim
                              ((fun x =>
                                  Sum.elim
                                    (Sum.elim
                                      (Sum.elim
                                          (Sum.elim
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inl)
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inr))
                                          i_1 ∘
                                        Sum.inl)
                                      (Sum.elim
                                          (Sum.elim
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inl)
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inr))
                                          i_1 ∘
                                        Sum.inr))
                                    (fun x => default (Fin.castAdd 0 x))
                                    (Sum.inl
                                      (Sum.elim
                                        (Sum.elim ((fun x => Sum.inl (Sum.inl x)) ∘ Sum.inl)
                                          ((fun x => Sum.inl (Sum.inl x)) ∘ Sum.inr))
                                        (fun i => if i.1 = 0 then Sum.inr i.2 else Sum.inl (Sum.inr i.2)) x))) ∘
                                Sum.inl)
                              ((fun x =>
                                  Sum.elim
                                    (Sum.elim
                                      (Sum.elim
                                          (Sum.elim
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inr))
                                                  i a) ∘
                                              Sum.inl)
                                            ((fun a =>
                                                Sum.elim
                                                  (Sum.elim
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inl)
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ Sum.inr))
                                                                  a) ∘
                                                              Sum.inr))
                                                          (fun x => default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x))) ∘
                                                      Sum.inl)
                                                    ((fun x =>
                                                        Sum.elim
                                                          (Sum.elim
                                                            ((fun a =>
                                                                Sum.elim default
                                                                  (Sum.elim ((fun t => Sum.rec fa fb t) ∘ Sum.inl)
                                                                    ((fun t => Sum.rec fa fb t) ∘ ⋯))
                                                                  ⋯) ∘
                                                              ⋯)
                                                            ⋯)
                                                          ⋯ ⋯) ∘
                                                      ⋯))
                                                  ⋯ ⋯) ∘
                                              ⋯))
                                          ⋯ ∘
                                        ⋯)
                                      ⋯)
                                    ⋯ ⋯) ∘
                                ⋯))
                            ⋯ ⋯) ∘
                        ⋯))
                    ⋯ ∧
                  ⋯) ↔
    ⋯