-- Mathlib/RingTheory/Etale/Field.lean
lemma of_isSeparable [Algebra.IsSeparable K L] : FormallyEtale K L

Proof state:
case comp_bijective.refine_6.H
K L : Type u
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g => (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g => (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
x : L
⊢ ((Ideal.Quotient.mkₐ K I).comp
        { toFun := fun x => (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯,
          map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ })
      x =
    f x

Tactic:
simpa using AlgHom.congr_fun (hg₁ x) (IntermediateField.AdjoinSimple.gen K x)

Result:
no goals

Proof state:
K L : Type u
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
k : L
this✝¹ : Algebra.IsSeparable K ↥K⟮k⟯
this✝ : FiniteDimensional K ↥K⟮k⟯
this : FormallyEtale K ↥K⟮k⟯
⊢ ∃! g, (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)

Tactic:
have := FormallyEtale.comp_bijective (R := K) (A := K⟮k⟯) I h

Result:
K L : Type u
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
k : L
this✝² : Algebra.IsSeparable K ↥K⟮k⟯
this✝¹ : FiniteDimensional K ↥K⟮k⟯
this✝ : FormallyEtale K ↥K⟮k⟯
this : Function.Bijective (Ideal.Quotient.mkₐ K I).comp
⊢ ∃! g, (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)

Proof state:
K L : Type u
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g => (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g => (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
this✝ : FiniteDimensional K ↥K⟮x, y⟯
this : Algebra.IsSeparable K ↥K⟮x, y⟯
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Tactic:
obtain ⟨⟨α, hα⟩, e⟩ := Field.exists_primitive_element K K⟮x,y⟯

Result:
case intro.mk
K L : Type u
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g => (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g => (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
this✝ : FiniteDimensional K ↥K⟮x, y⟯
this : Algebra.IsSeparable K ↥K⟮x, y⟯
α : L
hα : α ∈ K⟮x, y⟯
e : K⟮⟨α, hα⟩⟯ = ⊤
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Proof state:
K L : Type u
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g => (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g => (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
⊢ ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Tactic:
intro x y

Result:
K L : Type u
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g => (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g => (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯