-- Mathlib.FieldTheory.AxGrothendieck
FirstOrder.genericPolyMapSurjOnOfInjOn.eq_1 : ∀ {ι : Type u_1} {α : Type u_2} [inst : Finite α] [inst_1 : Finite ι] (φ : FirstOrder.Language.ring.Formula (α ⊕ ι))
  (mons : ι → Finset (ι →₀ ℕ)),
  FirstOrder.genericPolyMapSurjOnOfInjOn φ mons =
    FirstOrder.Language.Formula.iAlls (α ⊕ (i : ι) × ↥(mons i))
      (FirstOrder.Language.Formula.relabel Sum.inr
        ((FirstOrder.Language.Formula.iAlls ι
              ((FirstOrder.Language.Formula.relabel (Sum.map Sum.inl id) φ).imp
                (FirstOrder.Language.BoundedFormula.subst φ
                  (Sum.elim (fun a => FirstOrder.Language.var (Sum.inl (Sum.inl a))) fun i =>
                    FirstOrder.Language.Term.relabel
                      (fun i => (Equiv.sumAssoc α ((i : ι) × ↥(mons i)) ι).symm (Sum.inr i))
                      (FirstOrder.Ring.termOfFreeCommRing (FirstOrder.Ring.genericPolyMap mons i)))))).imp
          ((FirstOrder.Language.Formula.iAlls (Fin 2 × ι)
                (FirstOrder.Language.BoundedFormula.imp
                  (FirstOrder.Language.Formula.relabel (Sum.map Sum.inl fun i => (0, i)) φ)
                  (FirstOrder.Language.BoundedFormula.imp
                    (FirstOrder.Language.Formula.relabel (Sum.map Sum.inl fun i => (1, i)) φ)
                    (FirstOrder.Language.Formula.relabel
                      (fun x => (Equiv.sumAssoc α ((i : ι) × ↥(mons i)) (Fin 2 × ι)).symm (Sum.inr x))
                      (FirstOrder.Language.Formula.imp
                        (FirstOrder.Language.BoundedFormula.iInf fun i =>
                          (FirstOrder.Language.Term.relabel (Sum.inl ∘ Sum.map id fun i => (0, i))
                                (FirstOrder.Ring.termOfFreeCommRing (FirstOrder.Ring.genericPolyMap mons i))).bdEqual
                            (FirstOrder.Language.Term.relabel (Sum.inl ∘ Sum.map id fun i => (1, i))
                              (FirstOrder.Ring.termOfFreeCommRing (FirstOrder.Ring.genericPolyMap mons i))))
                        (FirstOrder.Language.BoundedFormula.iInf fun i =>
                          (FirstOrder.Language.var (Sum.inl (Sum.inr (0, i)))).bdEqual
                            (FirstOrder.Language.var (Sum.inl (Sum.inr (1, i)))))))))).imp
            (FirstOrder.Language.Formula.iAlls ι
              ((FirstOrder.Language.Formula.relabel (Sum.map Sum.inl id) φ).imp
                (FirstOrder.Language.Formula.iExs ι
                  (FirstOrder.Language.Formula.relabel
                    (fun i =>
                      have this :=
                        Sum.elim (Sum.inl ∘ Sum.inl) (fun i => if i.1 = 0 then Sum.inr i.2 else Sum.inl (Sum.inr i.2))
                          i;
                      this)
                    (FirstOrder.Language.Formula.relabel (Sum.map Sum.inl fun i => (0, i)) φ ⊓
                      FirstOrder.Language.Formula.relabel
                        (fun x => (Equiv.sumAssoc α ((i : ι) × ↥(mons i)) (Fin 2 × ι)).symm (Sum.inr x))
                        (FirstOrder.Language.BoundedFormula.iInf fun i =>
                          (FirstOrder.Language.Term.relabel (Sum.inl ∘ Sum.map id fun i => (0, i))
                                (FirstOrder.Ring.termOfFreeCommRing (FirstOrder.Ring.genericPolyMap mons i))).bdEqual
                            (FirstOrder.Language.var (Sum.inl (Sum.inr (1, i)))))))))))))