-- Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
theorem algHom_fieldRange_eq_of_comp_eq_of_range_eq
    (h : RingHom.comp f (algebraMap A K) = (g : A →+* L))
    {s : Set L} (hs : g.range = Algebra.adjoin F s) :
    f.fieldRange = IntermediateField.adjoin F s

Proof state:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑f).fieldRange = Subfield.closure (Set.range ⇑(algebraMap F L) ∪ s)

Tactic:
refine ringHom_fieldRange_eq_of_comp_eq_of_range_eq h ?_

Result:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑g).range = Subring.closure (Set.range ⇑(algebraMap F L) ∪ s)

Proof state:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ f.fieldRange.toSubfield = (IntermediateField.adjoin F s).toSubfield

Tactic:
simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]

Result:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑f).fieldRange = Subfield.closure (Set.range ⇑(algebraMap F L) ∪ s)

Proof state:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑g).range = g.range.toSubring

Tactic:
rfl

Result:
no goals

Proof state:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑g).range = Subring.closure (Set.range ⇑(algebraMap F L) ∪ s)

Tactic:
rw [← Algebra.adjoin_eq_ring_closure, ← hs]

Result:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑g).range = g.range.toSubring

Proof state:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ f.fieldRange = IntermediateField.adjoin F s

Tactic:
apply IntermediateField.toSubfield_injective

Result:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ f.fieldRange.toSubfield = (IntermediateField.adjoin F s).toSubfield