-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
K : Type u_3
inst_1 : Field K
inst_2 : CompatibleRing K
inst_3 : 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
⊢ K ⊨ genericPolyMapSurjOnOfInjOn φ mons ↔
    ∀ (v : α → K) (p : { p : ι → MvPolynomial ι K // ∀ (i : ι), (p i).support ⊆ mons i }),
      let f : (ι → K) → ι → K := fun (v : ι → K) (i : ι) ↦
        (eval v : (a : MvPolynomial ι K) → K) ((↑p : ι → MvPolynomial ι K) i);
      let S : Set (ι → K) := {x : ι → K | φ.Realize (Sum.elim v x)};
      Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
have simp : (∀ (fa : (val : α) → K) (fb : (val : (i : ι) × ↥(mons i)) → K),
    (∀ (i : ι → K),
        (Realize (M := K) φ
            (fun (x : α ⊕ ι) ↦
              Sum.elim
                (fun (a : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ ι) ↦
                  Sum.elim
                    (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                      Sum.elim
                        (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                          Sum.elim default
                            (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                              Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ K) fa fb t)
                            a)
                        (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                    i a)
                (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x))
                (Sum.inl (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) (fun (x : ι) ↦ Sum.inr x) x)))
            fun (x : Fin 0) ↦ default (Fin.cast sorry x)) →
          Realize (M := K) φ
            (fun (a : α ⊕ ι) ↦
              Term.realize (L := ring)
                (fun (a : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ ι) ↦
                  Sum.elim
                    (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                      Sum.elim
                        (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                          Sum.elim default
                            (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                              Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ K) fa fb t)
                            a)
                        (fun (x : Fin 0) ↦ 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 : (i : ι) × ↥(mons i) ⊕ ι) ↦
                        Sum.elim (fun (x : (i : ι) × ↥(mons i)) ↦ Sum.inl (Sum.inr x)) Sum.inr i)
                      (termOfFreeCommRing (genericPolyMap mons i)))
                  a))
            default) →
      (∀ (a a_1 : ι → K),
          (Realize (M := K) φ
              (fun (x : α ⊕ ι) ↦
                Sum.elim
                  (fun (a_2 : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ Fin 2 × ι) ↦
                    Sum.elim
                      (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                        Sum.elim
                          (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                            Sum.elim default
                              (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ K) fa fb t)
                              a)
                          (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                      (Function.uncurry
                        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ι → K) a
                          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ι → K) a_1
                            (finZeroElim (α := fun (i : Fin 0) ↦ ι → K)))))
                      a_2)
                  (fun (x : Fin 0) ↦ 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 : Fin 0) ↦ default (Fin.cast sorry x)) →
            (Realize (M := K) φ
                (fun (x : α ⊕ ι) ↦
                  Sum.elim
                    (fun (a_3 : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ Fin 2 × ι) ↦
                      Sum.elim
                        (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                          Sum.elim
                            (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                              Sum.elim default
                                (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                  Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ K) fa fb t)
                                a)
                            (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                        (Function.uncurry
                          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ι → K) a
                            (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ι → K) a_1
                              (finZeroElim (α := fun (i : Fin 0) ↦ ι → K)))))
                        a_3)
                    (fun (x : Fin 0) ↦ 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 : Fin 0) ↦ default (Fin.cast sorry x)) →
              (∀ (b : ι),
                  Eq.{u_3 + 1} (α := K)
                    (Term.realize
                      (fun (x : (i : ι) × ↥(mons i) ⊕ ι) ↦
                        Sum.elim
                          (fun (x : (i : ι) × ↥(mons i) ⊕ Fin 2 × ι) ↦
                            Sum.elim
                              (fun (a_4 : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ Fin 2 × ι) ↦
                                Sum.elim
                                  (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                    Sum.elim
                                      (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                        Sum.elim default
                                          (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                            Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ K) fa
                                              fb t)
                                          a)
                                      (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                  (Function.uncurry
                                    (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ι → K) a
                                      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ι → K) a_1
                                        (finZeroElim (α := fun (i : Fin 0) ↦ ι → K)))))
                                  a_4)
                              (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x))
                              (Sum.inl (Sum.elim (fun (x : (i : ι) × ↥(mons i)) ↦ Sum.inl (Sum.inr x)) Sum.inr x)))
                          (fun (x : Fin 0) ↦ default (Fin.cast sorry x))
                          (Sum.inl
                            (Sum.elim (fun (x : (i : ι) × ↥(mons i)) ↦ Sum.inl x) (fun (x : ι) ↦ Sum.inr (0, x)) x)))
                      (termOfFreeCommRing (genericPolyMap mons b)))
                    (Term.realize
                      (fun (x : (i : ι) × ↥(mons i) ⊕ ι) ↦
                        Sum.elim
                          (fun (x : (i : ι) × ↥(mons i) ⊕ Fin 2 × ι) ↦
                            Sum.elim
                              (fun (a_4 : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ Fin 2 × ι) ↦
                                Sum.elim
                                  (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                    Sum.elim
                                      (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                        Sum.elim default
                                          (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                            Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ K) fa
                                              fb t)
                                          a)
                                      (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                  (Function.uncurry
                                    (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ι → K) a
                                      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ι → K) a_1
                                        (finZeroElim (α := fun (i : Fin 0) ↦ ι → K)))))
                                  a_4)
                              (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x))
                              (Sum.inl (Sum.elim (fun (x : (i : ι) × ↥(mons i)) ↦ Sum.inl (Sum.inr x)) Sum.inr x)))
                          (fun (x : Fin 0) ↦ default (Fin.cast sorry x))
                          (Sum.inl
                            (Sum.elim (fun (x : (i : ι) × ↥(mons i)) ↦ Sum.inl x) (fun (x : ι) ↦ Sum.inr (1, x)) x)))
                      (termOfFreeCommRing (genericPolyMap mons b)))) →
                ∀ (b : ι),
                  Eq.{u_3 + 1} (α := K)
                    (Term.realize (L := ring) (α := ((i : ι) × ↥(mons i) ⊕ Fin 2 × ι) ⊕ Fin 0)
                      (Sum.elim
                        (fun (x : (i : ι) × ↥(mons i) ⊕ Fin 2 × ι) ↦
                          Sum.elim
                            (fun (a_5 : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ Fin 2 × ι) ↦
                              Sum.elim
                                (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                  Sum.elim
                                    (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                      Sum.elim default
                                        (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                          Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ K) fa fb
                                            t)
                                        a)
                                    (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                (Function.uncurry
                                  (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ι → K) a
                                    (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ι → K) a_1
                                      (finZeroElim (α := fun (i : Fin 0) ↦ ι → K)))))
                                a_5)
                            (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x))
                            (Sum.inl (Sum.elim (fun (x : (i : ι) × ↥(mons i)) ↦ Sum.inl (Sum.inr x)) Sum.inr x)))
                        fun (x : Fin 0) ↦ default (Fin.cast sorry x))
                      (var (Sum.inl (Sum.inr (0, b)))))
                    (Term.realize (L := ring) (α := ((i : ι) × ↥(mons i) ⊕ Fin 2 × ι) ⊕ Fin 0)
                      (Sum.elim
                        (fun (x : (i : ι) × ↥(mons i) ⊕ Fin 2 × ι) ↦
                          Sum.elim
                            (fun (a_5 : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ Fin 2 × ι) ↦
                              Sum.elim
                                (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                  Sum.elim
                                    (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                      Sum.elim default
                                        (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                          Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ K) fa fb
                                            t)
                                        a)
                                    (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                (Function.uncurry
                                  (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ι → K) a
                                    (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ι → K) a_1
                                      (finZeroElim (α := fun (i : Fin 0) ↦ ι → K)))))
                                a_5)
                            (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x))
                            (Sum.inl (Sum.elim (fun (x : (i : ι) × ↥(mons i)) ↦ Sum.inl (Sum.inr x)) Sum.inr x)))
                        fun (x : Fin 0) ↦ default (Fin.cast sorry x))
                      (var (Sum.inl (Sum.inr (1, b)))))) →
        ∀ (i : ι → K),
          (Realize (M := K) φ
              (fun (x : α ⊕ ι) ↦
                Sum.elim
                  (fun (a : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ ι) ↦
                    Sum.elim
                      (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                        Sum.elim
                          (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                            Sum.elim default
                              (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ K) fa fb t)
                              a)
                          (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                      i a)
                  (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x))
                  (Sum.inl (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) (fun (x : ι) ↦ Sum.inr x) x)))
              fun (x : Fin 0) ↦ default (Fin.cast sorry x)) →
            ∃ (i_1 : ι → K),
              (Realize (M := K) φ
                  (fun (x : α ⊕ ι) ↦
                    Sum.elim
                      (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ Fin 2 × ι) ↦
                        Sum.elim (α := (Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ ι) ⊕ ι)
                          (Sum.elim
                            (fun (a : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ ι) ↦
                              Sum.elim
                                (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                  Sum.elim
                                    (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                      Sum.elim default
                                        (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                          Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ K) fa fb
                                            t)
                                        a)
                                    (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                i a)
                            i_1)
                          (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x))
                          (Sum.inl
                            (Sum.elim (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ Sum.inl (Sum.inl x))
                              (fun (i : Fin 2 × ι) ↦ if i.1 = 0 then Sum.inr i.2 else Sum.inl (Sum.inr i.2)) x)))
                      (fun (x : Fin 0) ↦ default (Fin.cast sorry (Fin.castAdd 0 x)))
                      (Sum.inl (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) (fun (x : ι) ↦ Sum.inr (0, x)) x)))
                  fun (x : Fin 0) ↦ default (Fin.cast sorry (Fin.cast sorry x))) ∧
                ∀ (b : ι),
                  Eq.{u_3 + 1} (α := K)
                    (Term.realize
                      (fun (x : (i : ι) × ↥(mons i) ⊕ ι) ↦
                        Sum.elim
                          (fun (x : (i : ι) × ↥(mons i) ⊕ Fin 2 × ι) ↦
                            Sum.elim
                              (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ Fin 2 × ι) ↦
                                Sum.elim (α := (Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ ι) ⊕ ι)
                                  (Sum.elim
                                    (fun (a : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ ι) ↦
                                      Sum.elim
                                        (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                          Sum.elim
                                            (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                              Sum.elim default
                                                (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                                  Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                                    K) fa fb t)
                                                a)
                                            (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                        i a)
                                    i_1)
                                  (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x))
                                  (Sum.inl
                                    (Sum.elim (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ Sum.inl (Sum.inl x))
                                      (fun (i : Fin 2 × ι) ↦ if i.1 = 0 then Sum.inr i.2 else Sum.inl (Sum.inr i.2))
                                      x)))
                              (fun (x : Fin 0) ↦ default (Fin.cast sorry (Fin.castAdd 0 x)))
                              (Sum.inl (Sum.elim (fun (x : (i : ι) × ↥(mons i)) ↦ Sum.inl (Sum.inr x)) Sum.inr x)))
                          (fun (x : Fin 0) ↦ default (Fin.cast sorry (Fin.cast sorry x)))
                          (Sum.inl
                            (Sum.elim (fun (x : (i : ι) × ↥(mons i)) ↦ Sum.inl x) (fun (x : ι) ↦ Sum.inr (0, x)) x)))
                      (termOfFreeCommRing (genericPolyMap mons b)))
                    (Term.realize (L := ring) (α := ((i : ι) × ↥(mons i) ⊕ Fin 2 × ι) ⊕ Fin 0)
                      (Sum.elim
                        (fun (x : (i : ι) × ↥(mons i) ⊕ Fin 2 × ι) ↦
                          Sum.elim
                            (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ Fin 2 × ι) ↦
                              Sum.elim (α := (Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ ι) ⊕ ι)
                                (Sum.elim
                                  (fun (a : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i)) ⊕ ι) ↦
                                    Sum.elim
                                      (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                        Sum.elim
                                          (fun (a : Empty ⊕ Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                            Sum.elim default
                                              (fun (t : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦
                                                Sum.rec (motive := fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ K)
                                                  fa fb t)
                                              a)
                                          (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x)) (Sum.inl (Sum.inr x)))
                                      i a)
                                  i_1)
                                (fun (x : Fin 0) ↦ default (Fin.castAdd 0 x))
                                (Sum.inl
                                  (Sum.elim (fun (x : Sum.{u_2, u_1} α ((i : ι) × ↥(mons i))) ↦ Sum.inl (Sum.inl x))
                                    (fun (i : Fin 2 × ι) ↦ if i.1 = 0 then Sum.inr i.2 else Sum.inl (Sum.inr i.2)) x)))
                            (fun (x : Fin 0) ↦ default (Fin.cast sorry (Fin.castAdd 0 x)))
                            (Sum.inl (Sum.elim (fun (x : (i : ι) × ↥(mons i)) ↦ Sum.inl (Sum.inr x)) Sum.inr x)))
                        fun (x : Fin 0) ↦ default (Fin.cast sorry (Fin.cast sorry x)))
                      (var (Sum.inl (Sum.inr (1, b)))))) ↔
  ∀ (v : α → K) (b : (i : ι) × ↥(mons i) → K),
    (∀ ⦃x : ι → K⦄,
        Realize φ (Sum.elim v x) default →
          Realize φ
            (Sum.elim v fun (i : ι) ↦
              (eval x : (a : MvPolynomial ι K) → K)
                ((↑((Equiv.symm (mvPolynomialSupportLEEquiv mons) :
                          (a : (i : ι) × ↥(mons i) → K) →
                            { p : ι → MvPolynomial ι K // ∀ (i : ι), (p i).support ⊆ mons i })
                        b) :
                    ι → MvPolynomial ι K)
                  i))
            default) →
      (∀ (x y : ι → K),
          Realize φ (Sum.elim v x) default →
            Realize φ (Sum.elim v y) default →
              (∀ (x_1 : ι),
                  Eq.{u_3 + 1} (α := K)
                    ((eval x : (a : MvPolynomial ι K) → K)
                        ((↑((Equiv.symm (mvPolynomialSupportLEEquiv mons) :
                                  (a : (i : ι) × ↥(mons i) → K) →
                                    { p : ι → MvPolynomial ι K // ∀ (i : ι), (p i).support ⊆ mons i })
                                b) :
                            ι → MvPolynomial ι K)
                          x_1) :
                      K)
                    ((eval y : (a : MvPolynomial ι K) → K)
                        ((↑((Equiv.symm (mvPolynomialSupportLEEquiv mons) :
                                  (a : (i : ι) × ↥(mons i) → K) →
                                    { p : ι → MvPolynomial ι K // ∀ (i : ι), (p i).support ⊆ mons i })
                                b) :
                            ι → MvPolynomial ι K)
                          x_1) :
                      K)) →
                ∀ (x_1 : ι), x x_1 = y x_1) →
        ∀ (x : ι → K),
          Realize φ (Sum.elim v x) default →
            ∃ (a : ι → K),
              Realize φ (Sum.elim v a) default ∧
                ∀ (x_1 : ι),
                  (eval a : (a : MvPolynomial ι K) → K)
                      ((↑((Equiv.symm (mvPolynomialSupportLEEquiv mons) :
                                (a : (i : ι) × ↥(mons i) → K) →
                                  { p : ι → MvPolynomial ι K // ∀ (i : ι), (p i).support ⊆ mons i })
                              b) :
                          ι → MvPolynomial ι K)
                        x_1) =
                    x x_1
Tactic: simp only [Sentence.Realize, Formula.Realize, genericPolyMapSurjOnOfInjOn, Formula.relabel,
    Function.comp_def, Sum.map, id_eq, Equiv.sumAssoc, Equiv.coe_fn_symm_mk, Sum.elim_inr,
    realize_iAlls, realize_imp, realize_relabel, Fin.natAdd_zero, realize_subst, realize_iInf,
    realize_bdEqual, Term.realize_relabel,
    Equiv.forall_congr_left (Equiv.curry (Fin 2) ι K), Equiv.curry_symm_apply,
    Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, realize_iExs, realize_inf, Sum.forall_sum,
    Set.MapsTo, Set.mem_setOf_eq, injOnAlt, funext_iff, Set.SurjOn, Set.image,
    Set.subset_def, Equiv.forall_congr_left (mvPolynomialSupportLEEquiv mons)]