-- 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:
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}

Tactic:
refine Algebra.adjoin_induction ?_ ?_ ?_ ?_ hx

Result:
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}

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}

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}

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}

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
⊢ f.comp (algebraMap (↥(subalgebra R S)) S) = g.comp (algebraMap (↥(subalgebra R S)) S)

Tactic:
suffices f.comp (IsScalarTower.toAlgHom R _ S) = g.comp (IsScalarTower.toAlgHom R _ S) by
  ext; exact AlgHom.congr_fun this _

Result:
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
⊢ f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S) = g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)

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:
rw [← top_le_iff]

Result:
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}

Proof state:
case h.hs
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
⊢ Set.EqOn ⇑(f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
    ⇑(g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) {x | ↑x ∈ finset R S}

Tactic:
rintro ⟨x, hx⟩ hx'

Result:
case h.hs.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
hx' : ⟨x, hx⟩ ∈ {x | ↑x ∈ finset R S}
⊢ (f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) ⟨x, hx⟩ =
    (g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) ⟨x, hx⟩

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:
intro x hx

Result:
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}

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.toRingHom = g.toRingHom

Tactic:
apply IsLocalization.ringHom_ext (EssFiniteType.submonoid R S)

Result:
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
⊢ f.comp (algebraMap (↥(subalgebra R S)) S) = g.comp (algebraMap (↥(subalgebra R S)) S)

Proof state:
case h.hs.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
hx' : ⟨x, hx⟩ ∈ {x | ↑x ∈ finset R S}
⊢ (f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) ⟨x, hx⟩ =
    (g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) ⟨x, hx⟩

Tactic:
exact H x hx'

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)
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 mul_mem hx hy

Result:
no goals

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.toRingHom = g.toRingHom
⊢ f = g

Tactic:
ext

Result:
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✝