-- 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 (ι →₀ ℕ)
have : ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
have₁ :
  ∀
    (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₂ : ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
have₃ have₄ :
  ∀
    (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₅ :
  ∀
    (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 : (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
have₆ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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

Tactic:
classical
  have injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → (ι → K)),
      S.InjOn f ↔ ∀ x y, x ∈ S → y ∈ S → f x = f y → x = y := by
    simp [Set.InjOn]; tauto
  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)]
  simp +singlePass only [← Sum.elim_comp_inl_inr]
  -- was `simp` and very slow (https://github.com/leanprover-community/mathlib4/issues/19751)
  simp only [Function.comp_def, Sum.elim_inl, Sum.elim_inr, Fin.castAdd_zero, Fin.cast_eq_self,
    Nat.add_zero, Term.realize_var, Term.realize_relabel, realize_termOfFreeCommRing,
    lift_genericPolyMap, Nat.reduceAdd, Fin.isValue, Function.uncurry_apply_pair, Fin.cons_zero,
    Fin.cons_one, ↓reduceIte, one_ne_zero]

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.genericPolyMapSurjOnOfInjOn, FirstOrder.Language.BoundedFormula.realize_inf, Equiv.coe_fn_symm_mk, Sum.map, Set.subset_def, FirstOrder.Ring.lift_genericPolyMap, FirstOrder.Ring.realize_termOfFreeCommRing, FirstOrder.Language.BoundedFormula.realize_iExs, Equiv.forall_congr_left, Set.SurjOn, funext_iff, Fin.castAdd_zero, Nat.reduceAdd, FirstOrder.Language.Term.realize_relabel, Sum.forall_sum, Set.mem_setOf_eq, FirstOrder.Language.BoundedFormula.realize_relabel, FirstOrder.Language.BoundedFormula.realize_subst, Fin.cons_one, FirstOrder.Language.BoundedFormula.realize_iAlls, Sum.elim_inr, Function.comp_def, FirstOrder.Language.Formula.relabel, FirstOrder.Language.Term.realize_var, Fin.isValue, Set.MapsTo, Fin.cast_eq_self, Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, FirstOrder.Language.BoundedFormula.realize_bdEqual, Equiv.curry, Sum.elim_inl, reduceIte, Set.image, Nat.add_zero, Equiv.sumAssoc, Fin.natAdd_zero, FirstOrder.Language.BoundedFormula.realize_iInf, FirstOrder.Language.BoundedFormula.realize_imp, one_ne_zero, OfNat.ofNat, Sum.elim_comp_inl_inr, Fin, Function.uncurry_apply_pair, Equiv.curry_symm_apply, FirstOrder.Language.Formula.Realize, id_eq, Fin.cons_zero