-- Mathlib/FieldTheory/Extension.lean
theorem exists_algHom_adjoin_of_splits' :
    ∃ φ : adjoin L S →ₐ[F] K, φ.restrictDomain L = f

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)
⊢ ∃ φ, AlgHom.restrictDomain L φ = f

Tactic:
let L' := (IsScalarTower.toAlgHom F L E).fieldRange

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
⊢ ∃ φ, AlgHom.restrictDomain L φ = f

Proof state:
case refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
this : ∃ φ, AlgHom.restrictDomain (↥L') φ = f'
⊢ ∃ φ, AlgHom.restrictDomain L φ = f

Tactic:
obtain ⟨φ, hφ⟩ := this

Result:
case refine_2.intro
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
φ : ↥(adjoin (↥L') S) →ₐ[F] K
hφ : AlgHom.restrictDomain (↥L') φ = f'
⊢ ∃ φ, AlgHom.restrictDomain L φ = f

Proof state:
case refine_2.intro.refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
φ : ↥(adjoin (↥L') S) →ₐ[F] K
hφ : AlgHom.restrictDomain (↥L') φ = f'
⊢ AlgHom.restrictDomain L (φ.comp (inclusion ⋯)) = f

Tactic:
ext x

Result:
case refine_2.intro.refine_2.H
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
φ : ↥(adjoin (↥L') S) →ₐ[F] K
hφ : AlgHom.restrictDomain (↥L') φ = f'
x : L
⊢ (AlgHom.restrictDomain L (φ.comp (inclusion ⋯))) x = f x

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
⊢ ∃ φ, AlgHom.restrictDomain L φ = f

Tactic:
have := exists_algHom_adjoin_of_splits'' f' (S := S) fun s hs ↦ ?_

Result:
case refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
this : ∃ φ, AlgHom.restrictDomain (↥L') φ = f'
⊢ ∃ φ, AlgHom.restrictDomain L φ = f

case refine_1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
s : E
hs : s ∈ S
⊢ IsIntegral (↥L') s ∧ Splits f'.toRingHom (minpoly (↥L') s)

Proof state:
case h.e'_5.a
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ Splits f.toRingHom (minpoly L s)
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
s : E
hs : s ∈ S
this✝ : Algebra L ↥L' := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower L (↥L') E
x✝ : L
⊢ (f'.comp (algebraMap L ↥L')) x✝ = f.toRingHom x✝

Tactic:
exact congr_arg f (AlgEquiv.symm_apply_apply _ _)

Result:
no goals