-- Mathlib/RingTheory/Etale/Field.lean
theorem iff_exists_algEquiv_prod [EssFiniteType K A] :
    FormallyEtale K A ↔
      ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (_ : ∀ i, Field (Ai i))
        (_ : ∀ i, Algebra K (Ai i)) (_ : A ≃ₐ[K] Π i, Ai i),
        ∀ i, Algebra.IsSeparable K (Ai i)

Proof state:
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
I : Type u
w✝² : Finite I
Ai : I → Type u
w✝¹ : (i : I) → Field (Ai i)
w✝ : (i : I) → Algebra K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h✝ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
i : I
this✝¹ : Algebra A (Ai i) := ((Pi.evalRingHom Ai i).comp e.toRingEquiv.toRingHom).toAlgebra
this✝ : IsScalarTower K A (Ai i)
this : FiniteType A (Ai i)
⊢ EssFiniteType K (Ai i)

Tactic:
exact EssFiniteType.comp K A (Ai i)

Result:
no goals

Proof state:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this✝² : Module.Finite K A
this✝¹ : IsReduced A
this✝ : IsArtinianRing A
this : Fintype (MaximalSpectrum A) := ⋯.some
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
let v (i : MaximalSpectrum A) : A := (IsArtinianRing.equivPi A).symm (Pi.single i 1)

Result:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this✝² : Module.Finite K A
this✝¹ : IsReduced A
this✝ : IsArtinianRing A
this : Fintype (MaximalSpectrum A) := ⋯.some
v : MaximalSpectrum A → A := fun i => (IsArtinianRing.equivPi A).symm (Pi.single i 1)
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Proof state:
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
I : Type u
w✝² : Finite I
Ai : I → Type u
w✝¹ : (i : I) → Field (Ai i)
w✝ : (i : I) → Algebra K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h✝ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
i : I
this : Algebra A (Ai i) := ((Pi.evalRingHom Ai i).comp e.toRingEquiv.toRingHom).toAlgebra
⊢ EssFiniteType K (Ai i)

Tactic:
have : IsScalarTower K A (Ai i) :=
  .of_algebraMap_eq fun r ↦ by simp [RingHom.algebraMap_toAlgebra]

Result:
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
I : Type u
w✝² : Finite I
Ai : I → Type u
w✝¹ : (i : I) → Field (Ai i)
w✝ : (i : I) → Algebra K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h✝ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
i : I
this✝ : Algebra A (Ai i) := ((Pi.evalRingHom Ai i).comp e.toRingEquiv.toRingHom).toAlgebra
this : IsScalarTower K A (Ai i)
⊢ EssFiniteType K (Ai i)

Proof state:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this✝³ : Module.Finite K A
this✝² : IsReduced A
this✝¹ : IsArtinianRing A
this✝ : Fintype (MaximalSpectrum A) := ⋯.some
v : MaximalSpectrum A → A := fun i => (IsArtinianRing.equivPi A).symm (Pi.single i 1)
e : A ≃ₐ[K] (I : MaximalSpectrum A) → A ⧸ I.asIdeal :=
  let __spread.0 := IsArtinianRing.equivPi A;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : FormallyEtale K ((I : MaximalSpectrum A) → A ⧸ I.asIdeal)
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
rw [FormallyEtale.pi_iff] at this

Result:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this✝³ : Module.Finite K A
this✝² : IsReduced A
this✝¹ : IsArtinianRing A
this✝ : Fintype (MaximalSpectrum A) := ⋯.some
v : MaximalSpectrum A → A := fun i => (IsArtinianRing.equivPi A).symm (Pi.single i 1)
e : A ≃ₐ[K] (I : MaximalSpectrum A) → A ⧸ I.asIdeal :=
  let __spread.0 := IsArtinianRing.equivPi A;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (i : MaximalSpectrum A), FormallyEtale K (A ⧸ i.asIdeal)
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Proof state:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this✝³ : Module.Finite K A
this✝² : IsReduced A
this✝¹ : IsArtinianRing A
this✝ : Fintype (MaximalSpectrum A) := ⋯.some
v : MaximalSpectrum A → A := fun i => (IsArtinianRing.equivPi A).symm (Pi.single i 1)
e : A ≃ₐ[K] (I : MaximalSpectrum A) → A ⧸ I.asIdeal :=
  let __spread.0 := IsArtinianRing.equivPi A;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (i : MaximalSpectrum A), FormallyEtale K (A ⧸ i.asIdeal)
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
exact ⟨_, inferInstance, _, _, _, e, fun I ↦ (iff_isSeparable _ _).mp inferInstance⟩

Result:
no goals

Proof state:
case mpr
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
I : Type u
w✝² : Finite I
Ai : I → Type u
w✝¹ : (i : I) → Field (Ai i)
w✝ : (i : I) → Algebra K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h✝ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
this : ∀ (i : I), EssFiniteType K (Ai i)
⊢ ∀ (i : I), FormallyEtale K (Ai i)

Tactic:
exact fun I ↦ (iff_isSeparable _ _).mpr inferInstance

Result:
no goals

Proof state:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
⊢ FormallyEtale K A → ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
intro H

Result:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Proof state:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this✝² : Module.Finite K A
this✝¹ : IsReduced A
this✝ : IsArtinianRing A
this : Fintype (MaximalSpectrum A) := ⋯.some
v : MaximalSpectrum A → A := fun i => (IsArtinianRing.equivPi A).symm (Pi.single i 1)
e : A ≃ₐ[K] (I : MaximalSpectrum A) → A ⧸ I.asIdeal :=
  let __spread.0 := IsArtinianRing.equivPi A;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
have := (FormallyEtale.iff_of_equiv e).mp inferInstance

Result:
case mp
K A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this✝³ : Module.Finite K A
this✝² : IsReduced A
this✝¹ : IsArtinianRing A
this✝ : Fintype (MaximalSpectrum A) := ⋯.some
v : MaximalSpectrum A → A := fun i => (IsArtinianRing.equivPi A).symm (Pi.single i 1)
e : A ≃ₐ[K] (I : MaximalSpectrum A) → A ⧸ I.asIdeal :=
  let __spread.0 := IsArtinianRing.equivPi A;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : FormallyEtale K ((I : MaximalSpectrum A) → A ⧸ I.asIdeal)
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)