-- Mathlib/FieldTheory/AxGrothendieck.lean
theorem realize_genericPolyMapSurjOnOfInjOn
    [Finite ι] (φ : ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) :
    (K ⊨ genericPolyMapSurjOnOfInjOn φ mons) ↔
      ∀ (v : α → K) (p : { p : ι → MvPolynomial ι K // (∀ i, (p i).support ⊆ mons i) }),
        let f : (ι → K) → (ι → K) := fun v i => eval v (p.1 i)
        let S : Set (ι → K) := fun x => φ.Realize (Sum.elim v x)
        S.MapsTo f S → S.InjOn f → S.SurjOn f S

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) ↔
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y

Tactic:
tauto

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ K ⊨ genericPolyMapSurjOnOfInjOn φ mons ↔
    ∀ (v : α → K) (p : { p // ∀ (i : ι), (p i).support ⊆ mons i }),
      let f := fun v i => (eval v) (↑p i);
      let S := fun x => φ.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,
  Finset.mem_univ, realize_bdEqual, Term.realize_relabel, true_imp_iff,
  Equiv.forall_congr_left (Equiv.curry (Fin 2) ι K), Equiv.curry_symm_apply, Function.uncurry,
  Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, realize_iExs, realize_inf, Sum.forall_sum,
  Set.MapsTo, Set.mem_def, injOnAlt, funext_iff, Set.SurjOn, Set.image, setOf,
  Set.subset_def, Equiv.forall_congr_left (mvPolynomialSupportLEEquiv mons)]
simp +singlePass only [← Sum.elim_comp_inl_inr]
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]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ K ⊨ genericPolyMapSurjOnOfInjOn φ mons ↔
    ∀ (v : α → K) (p : { p // ∀ (i : ι), (p i).support ⊆ mons i }),
      let f := fun v i => (eval v) (↑p i);
      let S := fun x => φ.Realize (Sum.elim v x);
      Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S

Tactic:
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

Result:
ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : 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 // ∀ (i : ι), (p i).support ⊆ mons i }),
      let f := fun v i => (eval v) (↑p i);
      let S := fun x => φ.Realize (Sum.elim v x);
      Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S