awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
S : Type u_6
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
f g : AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) →ₐ[R] S
rw :
  HMul.hMul (α := S) (β := S)
      ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          ((algebraMap R (AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S)
      ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S) =
    1
rw₁ :
  Eq.{u_6 + 1} (α := S)
    ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
        (HMul.hMul (α := AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          ((algebraMap R (AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))) :
      S)
    (1 : S)
rw₂ :
  Eq.{u_6 + 1} (α := S)
    ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
        (HMul.hMul (α := AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          ((of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))) :
      S)
    (1 : S)
rw₃ : Eq.{u_6 + 1} (α := S) ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S) 1 : S) (1 : S)
rw₄ rw₅ : Eq.{u_6 + 1} (α := S) 1 1
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r : S)
      ((g : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S) =
    1

Tactic:
rw [← g.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]

Premises used: AdjoinRoot.algebraMap_eq, AdjoinRoot.root_isInv, map_mul, map_one, AlgHom.commutes
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : Prime f
⊢ IsDomain.{u_1} (AdjoinRoot f)

Tactic:
(Ideal.Quotient.isDomain_iff_prime (span {f} : Ideal R[X])).mpr <|
    (Ideal.span_singleton_prime hf.ne_zero).mpr hf

Premises used: Iff.mpr, AdjoinRoot, Ideal.Quotient.isDomain_iff_prime, Prime.ne_zero, Ideal.span, Ideal.span_singleton_prime, Singleton.singleton
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : Prime f
hf' : f.degree ≠ 0
⊢ IsTorsionFree R (AdjoinRoot f)

Tactic:
haveI := isDomain_of_prime hf
  isTorsionFree_iff_algebraMap_injective.mpr (of.injective_of_degree_ne_zero hf')

Premises used: Iff.mpr, Module.isTorsionFree_iff_algebraMap_injective, AdjoinRoot.of.injective_of_degree_ne_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R →+* S
p : R[X]
q : S[X]
h : q ∣ Polynomial.map f p
⊢ eval₂ ((of q).comp f) (root q) p = 0

Tactic:
simpa [← Polynomial.eval₂_map, ← algebraMap_eq, ← aeval_def]

Premises used: AdjoinRoot.algebraMap_eq, Polynomial.eval₂_map, Polynomial.aeval_def
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
q : S[X]
h : q ∣ Polynomial.map f p
r : R
⊢ Eq.{u_2 + 1} (α := AdjoinRoot q)
    ((map f p q h : (a : AdjoinRoot p) → AdjoinRoot q) ((of p : (a : R) → AdjoinRoot p) r) : AdjoinRoot q)
    ((of q : (a : S) → AdjoinRoot q) ((f : (a : R) → S) r) : AdjoinRoot q)

Tactic:
simp [map]

Premises used: AdjoinRoot.map
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : R[X]
q : S[X]
h : q ∣ Polynomial.map f p
⊢ (map f p q h : (a : AdjoinRoot p) → AdjoinRoot q) (root p) = root q

Tactic:
simp [map]

Premises used: AdjoinRoot.map
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
⊢ Polynomial.map g q ∣ Polynomial.map (g.comp f) p

Tactic:
simpa [Polynomial.map_map] using Polynomial.map_dvd g hf

Premises used: Polynomial.map_dvd, Polynomial.map_map
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
hAlg :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := AdjoinRoot r)
      ((((map g q r hg).comp (map f p q hf)).comp (of p) : (a : R) → AdjoinRoot r) x : AdjoinRoot r)
      (((map (g.comp f) p r ⋯).comp (of p) : (a : R) → AdjoinRoot r) x : AdjoinRoot r)
hRoot :
  Eq.{u_3 + 1} (α := AdjoinRoot r)
    (((map g q r hg).comp (map f p q hf) : (a : AdjoinRoot p) → AdjoinRoot r) (root p) : AdjoinRoot r)
    ((map (g.comp f) p r ⋯ : (a : AdjoinRoot p) → AdjoinRoot r) (root p) : AdjoinRoot r)
⊢ (map g q r hg).comp (map f p q hf) = map (g.comp f) p r ⋯

Tactic:
ext
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
x : R
⊢ Eq.{u_3 + 1} (α := AdjoinRoot r)
    ((((map g q r hg).comp (map f p q hf)).comp (of p) : (a : R) → AdjoinRoot r) x : AdjoinRoot r)
    (((map (g.comp f) p r ⋯).comp (of p) : (a : R) → AdjoinRoot r) x : AdjoinRoot r)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
⊢ Eq.{u_3 + 1} (α := AdjoinRoot r)
    (((map g q r hg).comp (map f p q hf) : (a : AdjoinRoot p) → AdjoinRoot r) (root p) : AdjoinRoot r)
    ((map (g.comp f) p r ⋯ : (a : AdjoinRoot p) → AdjoinRoot r) (root p) : AdjoinRoot r)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
⊢ p ∣ Polynomial.map (↑f.symm : S →+* R) q

Tactic:
simpa [Polynomial.map_map] using map_dvd f.symm.toRingHom h.dvd

Premises used: Associated.dvd, Polynomial.map_dvd, RingEquiv.toRingHom, Polynomial.map_map, RingEquiv.symm
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
hAlg :
  ∀ (x : S),
    Eq (α := AdjoinRoot q)
      ((((map (↑f : R →+* S) p q ⋯).comp (map (↑f.symm : S →+* R) q p ⋯)).comp (of q) : (a : S) → AdjoinRoot q) x :
        AdjoinRoot q)
      ((RingHom.comp (RingHom.id (AdjoinRoot q)) (of q) : (a : S) → AdjoinRoot q) x : AdjoinRoot q)
hRoot :
  Eq (α := AdjoinRoot q)
    (((map (↑f : R →+* S) p q ⋯).comp (map (↑f.symm : S →+* R) q p ⋯) : (a : AdjoinRoot q) → AdjoinRoot q) (root q) :
      AdjoinRoot q)
    ((RingHom.id (AdjoinRoot q) : (a : AdjoinRoot q) → AdjoinRoot q) (root q) : AdjoinRoot q)
⊢ (map (↑f : R →+* S) p q ⋯).comp (map (↑f.symm : S →+* R) q p ⋯) = RingHom.id (AdjoinRoot q)

Tactic:
ext
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
x : S
⊢ Eq (α := AdjoinRoot q)
    ((((map (↑f : R →+* S) p q ⋯).comp (map (↑f.symm : S →+* R) q p ⋯)).comp (of q) : (a : S) → AdjoinRoot q) x :
      AdjoinRoot q)
    ((RingHom.comp (RingHom.id (AdjoinRoot q)) (of q) : (a : S) → AdjoinRoot q) x : AdjoinRoot q)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
⊢ Eq (α := AdjoinRoot q)
    (((map (↑f : R →+* S) p q ⋯).comp (map (↑f.symm : S →+* R) q p ⋯) : (a : AdjoinRoot q) → AdjoinRoot q) (root q) :
      AdjoinRoot q)
    ((RingHom.id (AdjoinRoot q) : (a : AdjoinRoot q) → AdjoinRoot q) (root q) : AdjoinRoot q)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
hAlg :
  ∀ (x : R),
    Eq (α := AdjoinRoot p)
      ((((map (↑f.symm : S →+* R) q p ⋯).comp (map (↑f : R →+* S) p q ⋯)).comp (of p) : (a : R) → AdjoinRoot p) x :
        AdjoinRoot p)
      ((RingHom.comp (RingHom.id (AdjoinRoot p)) (of p) : (a : R) → AdjoinRoot p) x : AdjoinRoot p)
hRoot :
  Eq (α := AdjoinRoot p)
    (((map (↑f.symm : S →+* R) q p ⋯).comp (map (↑f : R →+* S) p q ⋯) : (a : AdjoinRoot p) → AdjoinRoot p) (root p) :
      AdjoinRoot p)
    ((RingHom.id (AdjoinRoot p) : (a : AdjoinRoot p) → AdjoinRoot p) (root p) : AdjoinRoot p)
⊢ (map (↑f.symm : S →+* R) q p ⋯).comp (map (↑f : R →+* S) p q ⋯) = RingHom.id (AdjoinRoot p)

Tactic:
ext
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
x : R
⊢ Eq (α := AdjoinRoot p)
    ((((map (↑f.symm : S →+* R) q p ⋯).comp (map (↑f : R →+* S) p q ⋯)).comp (of p) : (a : R) → AdjoinRoot p) x :
      AdjoinRoot p)
    ((RingHom.comp (RingHom.id (AdjoinRoot p)) (of p) : (a : R) → AdjoinRoot p) x : AdjoinRoot p)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
⊢ Eq (α := AdjoinRoot p)
    (((map (↑f.symm : S →+* R) q p ⋯).comp (map (↑f : R →+* S) p q ⋯) : (a : AdjoinRoot p) → AdjoinRoot p) (root p) :
      AdjoinRoot p)
    ((RingHom.id (AdjoinRoot p) : (a : AdjoinRoot p) → AdjoinRoot p) (root p) : AdjoinRoot p)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
⊢ Eq (α := (a : AdjoinRoot p) → AdjoinRoot q) (⇑(mapRingEquiv f p q h) : (a : AdjoinRoot p) → AdjoinRoot q)
    (⇑(map (↑f : R →+* S) p q ⋯) : (a : AdjoinRoot p) → AdjoinRoot q)

Tactic:
rfl

Premises used: AdjoinRoot, Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
⊢ Associated (Polynomial.map (↑f.symm : S →+* R) q) p

Tactic:
simpa [Polynomial.map_map] using associated_map_map f.symm.toRingHom h.symm

Premises used: Polynomial.associated_map_map, Associated.symm, RingEquiv.toRingHom, Polynomial.map_map, RingEquiv.symm
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f : R →+* S) p) q
⊢ (mapRingEquiv f p q h).symm = mapRingEquiv f.symm q p ⋯

Tactic:
rfl

Premises used: RingEquiv.ofRingHom, AdjoinRoot.mapRingEquiv, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S →ₐ[R] T
p : S[X]
q : T[X]
h : q ∣ Polynomial.map (↑f : S →+* T) p
r : R
⊢ (↑(↑(map (↑f : S →+* T) p q h) : AdjoinRoot p →* AdjoinRoot q) : OneHom (AdjoinRoot p) (AdjoinRoot q)).toFun
      ((algebraMap R (AdjoinRoot p) : (a : R) → AdjoinRoot p) r) =
    (algebraMap R (AdjoinRoot q) : (a : R) → AdjoinRoot q) r

Tactic:
simp [map, AdjoinRoot.algebraMap_eq']

Premises used: AdjoinRoot.map, AdjoinRoot.algebraMap_eq'
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
f : S →ₐ[R] T
p : S[X]
q : T[X]
h : q ∣ Polynomial.map (↑f : S →+* T) p
⊢ Eq (α := (a : AdjoinRoot p) → AdjoinRoot q) (⇑(mapAlgHom f p q h) : (a : AdjoinRoot p) → AdjoinRoot q)
    (⇑(map (↑f : S →+* T) p q h) : (a : AdjoinRoot p) → AdjoinRoot q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S →ₐ[R] T
g : T →ₐ[R] U
p : S[X]
q : T[X]
r : U[X]
hf : q ∣ Polynomial.map (↑f : S →+* T) p
hg : r ∣ Polynomial.map (↑g : T →+* U) q
⊢ Dvd.dvd (α := U[X]) (Polynomial.map (↑g : T →+* U) q) (Polynomial.map (↑(g.comp f) : S →+* U) p)

Tactic:
simpa [Polynomial.map_map] using Polynomial.map_dvd g.toRingHom hf

Premises used: Polynomial.map_dvd, AlgHom.toRingHom, Polynomial.map_map
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S →ₐ[R] T
g : T →ₐ[R] U
p : S[X]
q : T[X]
r : U[X]
hf : q ∣ Polynomial.map (↑f : S →+* T) p
hg : r ∣ Polynomial.map (↑g : T →+* U) q
⊢ (mapAlgHom g q r hg).comp (mapAlgHom f p q hf) = mapAlgHom (g.comp f) p r ⋯

Tactic:
aesop
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
a₁ :
  ∀ (x : S),
    Eq (α := S)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.toRingEquiv.symm : T →+* S) (↑f : S →+* T) :
            (a : S) → S)
          x :
        S)
      ((RingHom.id S : (a : S) → S) x : S)
⊢ Eq (α := S →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.toRingEquiv.symm : T →+* S) (↑f : S →+* T))
    (RingHom.id S)

Tactic:
ext
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
x : S
⊢ Eq (α := S)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.toRingEquiv.symm : T →+* S) (↑f : S →+* T) : (a : S) → S)
        x :
      S)
    ((RingHom.id S : (a : S) → S) x : S)

Tactic:
f.symm_apply_apply _

Premises used: AlgEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
x : S
⊢ Eq (α := S)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.toRingEquiv.symm : T →+* S) (↑f : S →+* T) : (a : S) → S)
        x :
      S)
    ((RingHom.id S : (a : S) → S) x : S)

Tactic:
exact f.symm_apply_apply _

Premises used: AlgEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
⊢ Eq (α := S →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.toRingEquiv.symm : T →+* S) (↑f : S →+* T))
    (RingHom.id S)

Tactic:
have : (RingHomClass.toRingHom f.toRingEquiv.symm).comp (RingHomClass.toRingHom f) =
        .id S := by ext; exact f.symm_apply_apply _
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
this :
  Eq (α := S →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.toRingEquiv.symm : T →+* S) (↑f : S →+* T))
    (RingHom.id S)
⊢ p ∣ Polynomial.map (↑(↑f.symm : T →ₐ[R] S) : T →+* S) q

Tactic:
simpa [Polynomial.map_map, -RingEquiv.symm_mk, this] using map_dvd f.symm.toRingHom h.dvd

Premises used: RingEquiv.symm_mk, Associated.dvd, Polynomial.map_dvd, AlgEquiv.symm, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, Polynomial.map_map
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
hAlg :
  ∀ (x : T),
    Eq (α := AdjoinRoot q)
      ((((mapAlgHom (↑f : S →ₐ[R] T) p q ⋯).comp (mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯)).comp (ofAlgHom R q) :
            (a : T) → AdjoinRoot q)
          x :
        AdjoinRoot q)
      ((AlgHom.comp (AlgHom.id R (AdjoinRoot q)) (ofAlgHom R q) : (a : T) → AdjoinRoot q) x : AdjoinRoot q)
hRoot :
  Eq (α := AdjoinRoot q)
    (((mapAlgHom (↑f : S →ₐ[R] T) p q ⋯).comp (mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯) :
          (a : AdjoinRoot q) → AdjoinRoot q)
        (root q) :
      AdjoinRoot q)
    ((AlgHom.id R (AdjoinRoot q) : (a : AdjoinRoot q) → AdjoinRoot q) (root q) : AdjoinRoot q)
⊢ (mapAlgHom (↑f : S →ₐ[R] T) p q ⋯).comp (mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯) = AlgHom.id R (AdjoinRoot q)

Tactic:
ext
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
x : T
⊢ Eq (α := AdjoinRoot q)
    ((((mapAlgHom (↑f : S →ₐ[R] T) p q ⋯).comp (mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯)).comp (ofAlgHom R q) :
          (a : T) → AdjoinRoot q)
        x :
      AdjoinRoot q)
    ((AlgHom.comp (AlgHom.id R (AdjoinRoot q)) (ofAlgHom R q) : (a : T) → AdjoinRoot q) x : AdjoinRoot q)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
⊢ Eq (α := AdjoinRoot q)
    (((mapAlgHom (↑f : S →ₐ[R] T) p q ⋯).comp (mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯) :
          (a : AdjoinRoot q) → AdjoinRoot q)
        (root q) :
      AdjoinRoot q)
    ((AlgHom.id R (AdjoinRoot q) : (a : AdjoinRoot q) → AdjoinRoot q) (root q) : AdjoinRoot q)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
hAlg :
  ∀ (x : S),
    Eq (α := AdjoinRoot p)
      ((((mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯).comp (mapAlgHom (↑f : S →ₐ[R] T) p q ⋯)).comp (ofAlgHom R p) :
            (a : S) → AdjoinRoot p)
          x :
        AdjoinRoot p)
      ((AlgHom.comp (AlgHom.id R (AdjoinRoot p)) (ofAlgHom R p) : (a : S) → AdjoinRoot p) x : AdjoinRoot p)
hRoot :
  Eq (α := AdjoinRoot p)
    (((mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯).comp (mapAlgHom (↑f : S →ₐ[R] T) p q ⋯) :
          (a : AdjoinRoot p) → AdjoinRoot p)
        (root p) :
      AdjoinRoot p)
    ((AlgHom.id R (AdjoinRoot p) : (a : AdjoinRoot p) → AdjoinRoot p) (root p) : AdjoinRoot p)
⊢ (mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯).comp (mapAlgHom (↑f : S →ₐ[R] T) p q ⋯) = AlgHom.id R (AdjoinRoot p)

Tactic:
ext
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
x : S
⊢ Eq (α := AdjoinRoot p)
    ((((mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯).comp (mapAlgHom (↑f : S →ₐ[R] T) p q ⋯)).comp (ofAlgHom R p) :
          (a : S) → AdjoinRoot p)
        x :
      AdjoinRoot p)
    ((AlgHom.comp (AlgHom.id R (AdjoinRoot p)) (ofAlgHom R p) : (a : S) → AdjoinRoot p) x : AdjoinRoot p)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
⊢ Eq (α := AdjoinRoot p)
    (((mapAlgHom (↑f.symm : T →ₐ[R] S) q p ⋯).comp (mapAlgHom (↑f : S →ₐ[R] T) p q ⋯) :
          (a : AdjoinRoot p) → AdjoinRoot p)
        (root p) :
      AdjoinRoot p)
    ((AlgHom.id R (AdjoinRoot p) : (a : AdjoinRoot p) → AdjoinRoot p) (root p) : AdjoinRoot p)

Tactic:
simp