-- Mathlib/RingTheory/EssentialFiniteness.lean
lemma EssFiniteType.algHom_ext [EssFiniteType R S]
    (f g : S →ₐ[R] T) (H : ∀ s ∈ finset R S, f s = g s) : f = g

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
this : f.comp (IsScalarTower.toAlgHom R ?m.92928 S) = g.comp (IsScalarTower.toAlgHom R ?m.92928 S)
⊢ f.comp (algebraMap (↥(subalgebra R S)) S) = g.comp (algebraMap (↥(subalgebra R S)) S)

Tactic:
ext

Result:
case a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
this : f.comp (IsScalarTower.toAlgHom R ?m.92928 S) = g.comp (IsScalarTower.toAlgHom R ?m.92928 S)
x✝ : ↥(subalgebra R S)
⊢ (f.comp (algebraMap (↥(subalgebra R S)) S)) x✝ = (g.comp (algebraMap (↥(subalgebra R S)) S)) x✝

Proof state:
case h.h.mk.refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
x : S
hx : x ∈ subalgebra R S
a✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ∀ (x y : S) (hx : x ∈ adjoin R ↑(finset R S)) (hy : y ∈ adjoin R ↑(finset R S)),
    ⟨x, hx⟩ ∈ adjoin R {x | ↑x ∈ finset R S} →
      ⟨y, hy⟩ ∈ adjoin R {x | ↑x ∈ finset R S} → ⟨x + y, ⋯⟩ ∈ adjoin R {x | ↑x ∈ finset R S}

Tactic:
intro x y _ _ hx hy

Result:
case h.h.mk.refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
x✝ : S
hx✝¹ : x✝ ∈ subalgebra R S
a✝ : ⟨x✝, hx✝¹⟩ ∈ ⊤
x y : S
hx✝ : x ∈ adjoin R ↑(finset R S)
hy✝ : y ∈ adjoin R ↑(finset R S)
hx : ⟨x, hx✝⟩ ∈ adjoin R {x | ↑x ∈ finset R S}
hy : ⟨y, hy✝⟩ ∈ adjoin R {x | ↑x ∈ finset R S}
⊢ ⟨x + y, ⋯⟩ ∈ adjoin R {x | ↑x ∈ finset R S}

Proof state:
case H
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
this : f.toRingHom = g.toRingHom
x✝ : S
⊢ f x✝ = g x✝

Tactic:
exact RingHom.congr_fun this _

Result:
no goals

Proof state:
case h.h.mk.refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
x : S
hx : x ∈ subalgebra R S
a✝ : ⟨x, hx⟩ ∈ ⊤
r : R
⊢ ⟨(algebraMap R S) r, ⋯⟩ ∈ adjoin R {x | ↑x ∈ finset R S}

Tactic:
exact Subalgebra.algebraMap_mem _ _

Result:
no goals

Proof state:
case h.h.mk.refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
x : S
hx : x ∈ subalgebra R S
a✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ∀ (r : R), ⟨(algebraMap R S) r, ⋯⟩ ∈ adjoin R {x | ↑x ∈ finset R S}

Tactic:
intro r

Result:
case h.h.mk.refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
x : S
hx : x ∈ subalgebra R S
a✝ : ⟨x, hx⟩ ∈ ⊤
r : R
⊢ ⟨(algebraMap R S) r, ⋯⟩ ∈ adjoin R {x | ↑x ∈ finset R S}

Proof state:
case a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
this : f.comp (IsScalarTower.toAlgHom R ?m.92928 S) = g.comp (IsScalarTower.toAlgHom R ?m.92928 S)
x✝ : ↥(subalgebra R S)
⊢ (f.comp (algebraMap (↥(subalgebra R S)) S)) x✝ = (g.comp (algebraMap (↥(subalgebra R S)) S)) x✝

Tactic:
exact AlgHom.congr_fun this _

Result:
no goals

Proof state:
case h.h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
⊢ ⊤ ≤ adjoin R {x | ↑x ∈ finset R S}

Tactic:
rintro ⟨x, hx⟩ _

Result:
case h.h.mk
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
x : S
hx : x ∈ subalgebra R S
a✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ⟨x, hx⟩ ∈ adjoin R {x | ↑x ∈ finset R S}

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
⊢ f = g

Tactic:
suffices f.toRingHom = g.toRingHom by ext; exact RingHom.congr_fun this _

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
⊢ f.toRingHom = g.toRingHom

Proof state:
case h.h.mk.refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
x✝ : S
hx✝ : x✝ ∈ subalgebra R S
a✝ : ⟨x✝, hx✝⟩ ∈ ⊤
x : S
hx : x ∈ ↑(finset R S)
⊢ ⟨x, ⋯⟩ ∈ adjoin R {x | ↑x ∈ finset R S}

Tactic:
exact Algebra.subset_adjoin hx

Result:
no goals

Proof state:
case h.h.mk.refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
x✝ : S
hx✝¹ : x✝ ∈ subalgebra R S
a✝ : ⟨x✝, hx✝¹⟩ ∈ ⊤
x y : S
hx✝ : x ∈ adjoin R ↑(finset R S)
hy✝ : y ∈ adjoin R ↑(finset R S)
hx : ⟨x, hx✝⟩ ∈ adjoin R {x | ↑x ∈ finset R S}
hy : ⟨y, hy✝⟩ ∈ adjoin R {x | ↑x ∈ finset R S}
⊢ ⟨x + y, ⋯⟩ ∈ adjoin R {x | ↑x ∈ finset R S}

Tactic:
exact add_mem hx hy

Result:
no goals

Proof state:
case h.h.mk.refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
x : S
hx : x ∈ subalgebra R S
a✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ∀ (x y : S) (hx : x ∈ adjoin R ↑(finset R S)) (hy : y ∈ adjoin R ↑(finset R S)),
    ⟨x, hx⟩ ∈ adjoin R {x | ↑x ∈ finset R S} →
      ⟨y, hy⟩ ∈ adjoin R {x | ↑x ∈ finset R S} → ⟨x * y, ⋯⟩ ∈ adjoin R {x | ↑x ∈ finset R S}

Tactic:
intro x y _ _ hx hy

Result:
case h.h.mk.refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
x✝ : S
hx✝¹ : x✝ ∈ subalgebra R S
a✝ : ⟨x✝, hx✝¹⟩ ∈ ⊤
x y : S
hx✝ : x ∈ adjoin R ↑(finset R S)
hy✝ : y ∈ adjoin R ↑(finset R S)
hx : ⟨x, hx✝⟩ ∈ adjoin R {x | ↑x ∈ finset R S}
hy : ⟨y, hy✝⟩ ∈ adjoin R {x | ↑x ∈ finset R S}
⊢ ⟨x * y, ⋯⟩ ∈ adjoin R {x | ↑x ∈ finset R S}