-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem ext_map (h h' : IsAdjoinRoot S f) (eq : ∀ x, h.map x = h'.map x) : h = h'

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h h' : IsAdjoinRoot S f
eq : ∀ (x : R[X]), h.map x = h'.map x
⊢ h = h'

Tactic:
cases h

Result:
case mk
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h' : IsAdjoinRoot S f
map✝ : R[X] →+* S
map_surjective✝ : Function.Surjective ⇑map✝
ker_map✝ : RingHom.ker map✝ = Ideal.span {f}
algebraMap_eq✝ : algebraMap R S = map✝.comp C
eq :
  ∀ (x : R[X]),
    { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝, algebraMap_eq := algebraMap_eq✝ }.map x =
      h'.map x
⊢ { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝, algebraMap_eq := algebraMap_eq✝ } = h'

Proof state:
case mk.mk
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
map✝¹ : R[X] →+* S
map_surjective✝¹ : Function.Surjective ⇑map✝¹
ker_map✝¹ : RingHom.ker map✝¹ = Ideal.span {f}
algebraMap_eq✝¹ : algebraMap R S = map✝¹.comp C
map✝ : R[X] →+* S
map_surjective✝ : Function.Surjective ⇑map✝
ker_map✝ : RingHom.ker map✝ = Ideal.span {f}
algebraMap_eq✝ : algebraMap R S = map✝.comp C
eq :
  ∀ (x : R[X]),
    { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹, algebraMap_eq := algebraMap_eq✝¹ }.map x =
      { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝, algebraMap_eq := algebraMap_eq✝ }.map x
⊢ { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹, algebraMap_eq := algebraMap_eq✝¹ } =
    { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝, algebraMap_eq := algebraMap_eq✝ }

Tactic:
congr

Result:
case mk.mk.e_map
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
map✝¹ : R[X] →+* S
map_surjective✝¹ : Function.Surjective ⇑map✝¹
ker_map✝¹ : RingHom.ker map✝¹ = Ideal.span {f}
algebraMap_eq✝¹ : algebraMap R S = map✝¹.comp C
map✝ : R[X] →+* S
map_surjective✝ : Function.Surjective ⇑map✝
ker_map✝ : RingHom.ker map✝ = Ideal.span {f}
algebraMap_eq✝ : algebraMap R S = map✝.comp C
eq :
  ∀ (x : R[X]),
    { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹, algebraMap_eq := algebraMap_eq✝¹ }.map x =
      { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝, algebraMap_eq := algebraMap_eq✝ }.map x
⊢ map✝¹ = map✝

Proof state:
case mk.mk.e_map
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
map✝¹ : R[X] →+* S
map_surjective✝¹ : Function.Surjective ⇑map✝¹
ker_map✝¹ : RingHom.ker map✝¹ = Ideal.span {f}
algebraMap_eq✝¹ : algebraMap R S = map✝¹.comp C
map✝ : R[X] →+* S
map_surjective✝ : Function.Surjective ⇑map✝
ker_map✝ : RingHom.ker map✝ = Ideal.span {f}
algebraMap_eq✝ : algebraMap R S = map✝.comp C
eq :
  ∀ (x : R[X]),
    { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹, algebraMap_eq := algebraMap_eq✝¹ }.map x =
      { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝, algebraMap_eq := algebraMap_eq✝ }.map x
⊢ map✝¹ = map✝

Tactic:
exact RingHom.ext eq

Result:
no goals

Proof state:
case mk
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h' : IsAdjoinRoot S f
map✝ : R[X] →+* S
map_surjective✝ : Function.Surjective ⇑map✝
ker_map✝ : RingHom.ker map✝ = Ideal.span {f}
algebraMap_eq✝ : algebraMap R S = map✝.comp C
eq :
  ∀ (x : R[X]),
    { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝, algebraMap_eq := algebraMap_eq✝ }.map x =
      h'.map x
⊢ { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝, algebraMap_eq := algebraMap_eq✝ } = h'

Tactic:
cases h'

Result:
case mk.mk
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
map✝¹ : R[X] →+* S
map_surjective✝¹ : Function.Surjective ⇑map✝¹
ker_map✝¹ : RingHom.ker map✝¹ = Ideal.span {f}
algebraMap_eq✝¹ : algebraMap R S = map✝¹.comp C
map✝ : R[X] →+* S
map_surjective✝ : Function.Surjective ⇑map✝
ker_map✝ : RingHom.ker map✝ = Ideal.span {f}
algebraMap_eq✝ : algebraMap R S = map✝.comp C
eq :
  ∀ (x : R[X]),
    { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹, algebraMap_eq := algebraMap_eq✝¹ }.map x =
      { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝, algebraMap_eq := algebraMap_eq✝ }.map x
⊢ { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹, algebraMap_eq := algebraMap_eq✝¹ } =
    { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝, algebraMap_eq := algebraMap_eq✝ }