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

Proof state:
case comp_bijective
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 = ⊥
⊢ Function.Surjective (Ideal.Quotient.mkₐ K I).comp

Tactic:
intro f

Result:
case comp_bijective
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
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

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
x y : L
h : x ∈ K⟮y⟯
e : K⟮x⟯ ≤ K⟮y⟯
⊢ (fun g => (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮x⟯) L))
    ((g y).comp (IntermediateField.inclusion e))

Tactic:
apply AlgHom.ext

Result:
case 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
x y : L
h : x ∈ K⟮y⟯
e : K⟮x⟯ ≤ K⟮y⟯
⊢ ∀ (x_1 : ↥K⟮x⟯),
    ((Ideal.Quotient.mkₐ K I).comp ((g y).comp (IntermediateField.inclusion e))) x_1 =
      (f.comp (IsScalarTower.toAlgHom K (↥K⟮x⟯) L)) x_1

Proof state:
case 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
x y : L
h : x ∈ K⟮y⟯
e : K⟮x⟯ ≤ K⟮y⟯
a : L
property✝ : a ∈ K⟮x⟯
⊢ (f.comp ((IsScalarTower.toAlgHom K (↥K⟮y⟯) L).comp (IntermediateField.inclusion e))) ⟨a, property✝⟩ =
    (f.comp (IsScalarTower.toAlgHom K (↥K⟮x⟯) L)) ⟨a, property✝⟩

Tactic:
simp

Result:
no goals

Proof state:
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 : IntermediateField.map K⟮x, y⟯.val K⟮⟨α, hα⟩⟯ = IntermediateField.map K⟮x, y⟯.val ⊤
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Tactic:
rw [IntermediateField.adjoin_map, ← AlgHom.fieldRange_eq_map] at e

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 : IntermediateField.adjoin K (⇑K⟮x, y⟯.val '' {⟨α, hα⟩}) = K⟮x, y⟯.val.fieldRange
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Proof state:
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⟮α⟯ = K⟮x, y⟯
hx : x ∈ K⟮α⟯
hy : y ∈ K⟮α⟯
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Tactic:
exact ⟨α, hx, hy⟩

Result:
no goals

Proof state:
case 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
x y : L
h : x ∈ K⟮y⟯
e : K⟮x⟯ ≤ K⟮y⟯
a : L
property✝ : a ∈ K⟮x⟯
⊢ ((Ideal.Quotient.mkₐ K I).comp ((g y).comp (IntermediateField.inclusion e))) ⟨a, property✝⟩ =
    (f.comp (IsScalarTower.toAlgHom K (↥K⟮x⟯) L)) ⟨a, property✝⟩

Tactic:
rw [← AlgHom.comp_assoc, hg₁, AlgHom.comp_assoc]

Result:
case 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
x y : L
h : x ∈ K⟮y⟯
e : K⟮x⟯ ≤ K⟮y⟯
a : L
property✝ : a ∈ K⟮x⟯
⊢ (f.comp ((IsScalarTower.toAlgHom K (↥K⟮y⟯) L).comp (IntermediateField.inclusion e))) ⟨a, property✝⟩ =
    (f.comp (IsScalarTower.toAlgHom K (↥K⟮x⟯) L)) ⟨a, property✝⟩

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
⊢ ∃! g, (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)

Tactic:
have := IsSeparable.of_algHom _ _ (IsScalarTower.toAlgHom K (K⟮k⟯) L)

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⟯
⊢ ∃! g, (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)