-- Mathlib/NumberTheory/KummerDedekind.lean
private lemma f_symm_aux (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤)
    (hx' : IsIntegral R x) (Q : R[X]) :
    (f hx hx').symm (Q.map (Ideal.Quotient.mk I)) = Q.aeval x

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ ((↑((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I)).trans (quotEquivOfEq ⋯))
      ((↑((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I)).symm
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}))
          (Polynomial.map (Ideal.Quotient.mk I) Q))) =
    (⇑((↑((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I)).trans (quotEquivOfEq ⋯)) ∘
        ⇑(quotAdjoinEquivQuotMap hx ⋯).symm)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))

Tactic:
congr

Result:
case a.h.e_6.h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (↑((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I)).symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}))
        (Polynomial.map (Ideal.Quotient.mk I) Q)) =
    (quotAdjoinEquivQuotMap hx ⋯).symm ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))

Proof state:
case h.e'_3.a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (quotAdjoinEquivQuotMap hx ⋯)
      ((quotAdjoinEquivQuotMap hx ⋯).symm ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))) =
    (quotAdjoinEquivQuotMap hx ⋯)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↥(adjoin R {x})) I)) ((aeval (adjoin.powerBasis' hx').gen) Q))

Tactic:
simp only [RingEquiv.apply_symm_apply, adjoin.powerBasis'_gen, quotAdjoinEquivQuotMap_apply_mk,
  coe_aeval_mk_apply]

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (quotAdjoinEquivQuotMap hx ⋯).symm ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q)) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R ↥(adjoin R {x})) I)) ((aeval (adjoin.powerBasis' hx').gen) Q)

Tactic:
apply (quotAdjoinEquivQuotMap hx
  (FaithfulSMul.algebraMap_injective ((adjoin R {x})) S)).injective

Result:
case h.e'_3.a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (quotAdjoinEquivQuotMap hx ⋯)
      ((quotAdjoinEquivQuotMap hx ⋯).symm ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))) =
    (quotAdjoinEquivQuotMap hx ⋯)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↥(adjoin R {x})) I)) ((aeval (adjoin.powerBasis' hx').gen) Q))

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (KummerDedekind.f hx hx').symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
        (Polynomial.map (Ideal.Quotient.mk I) Q)) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q)

Tactic:
apply (f hx hx').injective

Result:
case a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (KummerDedekind.f hx hx')
      ((KummerDedekind.f hx hx').symm
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (Polynomial.map (Ideal.Quotient.mk I) Q))) =
    (KummerDedekind.f hx hx') ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))

Proof state:
case a.h.e_6.h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (↑((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I)).symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}))
        (Polynomial.map (Ideal.Quotient.mk I) Q)) =
    (quotAdjoinEquivQuotMap hx ⋯).symm ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))

Tactic:
convert (adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap_symm_apply_mk I Q

Result:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (quotAdjoinEquivQuotMap hx ⋯).symm ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q)) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R ↥(adjoin R {x})) I)) ((aeval (adjoin.powerBasis' hx').gen) Q)