-- Mathlib/RingTheory/Etale/Field.lean
theorem Algebra.Etale.iff_exists_algEquiv_prod :
    Etale 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, Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)

Proof state:
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra K A
⊢ Etale K A ↔ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Module.Finite K (Ai 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
⊢ Etale K A → ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)

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

Proof state:
case mp
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra K A
⊢ Etale K A → ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Module.Finite K (Ai 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
H : Etale K A
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)

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

Tactic:
obtain ⟨I, _, Ai, _, _, e, _⟩ := (FormallyEtale.iff_exists_algEquiv_prod K A).mp inferInstance

Result:
case mp.intro.intro.intro.intro.intro.intro
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra K A
H : Etale 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, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)

Proof state:
case mpr
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra 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), Module.Finite K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
⊢ Etale K A

Tactic:
have := Module.Finite.of_surjective e.symm.toLinearMap e.symm.surjective

Result:
case mpr
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra 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), Module.Finite K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
this : Module.Finite K A
⊢ Etale K A

Proof state:
case mp.intro.intro.intro.intro.intro.intro
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra K A
H : Etale 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 : Module.Finite K A
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)

Tactic:
exact ⟨_, ‹_›, _, _, _, e, fun i ↦ ⟨.of_surjective ((LinearMap.proj i).comp e.toLinearMap)
  ((Function.surjective_eval i).comp e.surjective), inferInstance⟩⟩

Result:
no goals

Proof state:
case mpr
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra 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), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)
⊢ Etale K A

Tactic:
choose h₁ h₂ using H

Result:
case mpr
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra 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), Module.Finite K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
⊢ Etale K A

Proof state:
case mpr
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra 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), Module.Finite K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
this : Module.Finite K A
⊢ Etale K A

Tactic:
refine ⟨?_, FinitePresentation.of_finiteType.mp inferInstance⟩

Result:
case mpr
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra 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), Module.Finite K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
this : Module.Finite K A
⊢ FormallyEtale K A

Proof state:
case mp.intro.intro.intro.intro.intro.intro
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra K A
H : Etale 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, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)

Tactic:
have := FormallyUnramified.finite_of_free K A

Result:
case mp.intro.intro.intro.intro.intro.intro
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra K A
H : Etale 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 : Module.Finite K A
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)

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

Tactic:
intro ⟨I, _, Ai, _, _, e, H⟩

Result:
case mpr
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra 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), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)
⊢ Etale K A

Proof state:
case mpr
K A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra 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), Module.Finite K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
this : Module.Finite K A
⊢ FormallyEtale K A

Tactic:
exact (FormallyEtale.iff_exists_algEquiv_prod K A).mpr ⟨_, inferInstance, _, _, _, e, h₂⟩

Result:
no goals