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

Tactic:
let e : A ≃ₐ[K] _ := { __ := IsArtinianRing.equivPi A, commutes' := fun r ↦ rfl }

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' := ⋯ }
⊢ ∃ 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
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
letI : Fintype (MaximalSpectrum A) := (nonempty_fintype _).some

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
⊢ ∃ 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
⊢ EssFiniteType K (Ai i)

Tactic:
letI := ((Pi.evalRingHom Ai i).comp e.toRingHom).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
⊢ EssFiniteType 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
r : K
⊢ (algebraMap K (Ai i)) r = (algebraMap A (Ai i)) ((algebraMap K A) r)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Result:
no goals

Proof state:
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:
constructor

Result:
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)

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

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
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
have : IsArtinianRing A := isArtinian_of_tower K 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
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

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)
⊢ ∀ (i : I), FormallyEtale K (Ai i)

Tactic:
have (i) : EssFiniteType K (Ai i) := by
  letI := ((Pi.evalRingHom Ai i).comp e.toRingHom).toAlgebra
  have : IsScalarTower K A (Ai i) :=
    .of_algebraMap_eq fun r ↦ by simp [RingHom.algebraMap_toAlgebra]
  have : Algebra.FiniteType A (Ai i) := .of_surjective inferInstance (Algebra.ofId _ _)
    (RingHomSurjective.is_surjective (σ := Pi.evalRingHom Ai i).comp e.surjective)
  exact EssFiniteType.comp K A (Ai i)

Result:
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)

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)
⊢ FormallyEtale K A

Tactic:
rw [FormallyEtale.iff_of_equiv e, FormallyEtale.pi_iff]

Result:
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)
⊢ ∀ (i : I), FormallyEtale 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)
⊢ EssFiniteType K (Ai i)

Tactic:
have : Algebra.FiniteType A (Ai i) := .of_surjective inferInstance (Algebra.ofId _ _)
  (RingHomSurjective.is_surjective (σ := Pi.evalRingHom Ai i).comp e.surjective)

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)
this : FiniteType A (Ai i)
⊢ EssFiniteType K (Ai i)