-- Module: Mathlib.FieldTheory.AxGrothendieck
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
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (∀ (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 ⋯ 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 ⋯ 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 ⋯ 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 ⋯ 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 ⋯ 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 ⋯ 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 ⋯ 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 ⋯ 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 ⋯ (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 ⋯ (Fin.cast ⋯ 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 ⋯ (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 ⋯ (Fin.cast ⋯ 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 ⋯ (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 ⋯ (Fin.cast ⋯ 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 +singlePass only [← Sum.elim_comp_inl_inr]

Premises used: Sum.elim_comp_inl_inr