-- 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 (ι →₀ ℕ)
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
⊢ 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 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 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: 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]