awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) f : S) (0 : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
hX : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) X : S) ((h.map : (a : R[X]) → S) X : S)
⊢ aeval h.root = h.map

Tactic:
ext
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) X : S) ((h.map : (a : R[X]) → S) X : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) f : S) (0 : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
rw : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑h.map : (a : R[X]) → S)
⊢ Eq (α := Subalgebra R S) R[h.root] ⊤

Tactic:
rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top, aeval_root_eq_map]

Premises used: Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top, IsAdjoinRoot.aeval_root_eq_map
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑h.map : (a : R[X]) → S)

Tactic:
h.map_surjective

Premises used: IsAdjoinRoot.map_surjective
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑h.map : (a : R[X]) → S)

Tactic:
exact h.map_surjective

Premises used: IsAdjoinRoot.map_surjective
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h h' : IsAdjoinRoot S f
eq : ∀ (x : R[X]), Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) x : S) ((h'.map : (a : R[X]) → S) x : S)
mk :
  ∀ (map : R[X] →ₐ[R] S)
    (map_surjective : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map : (a : R[X]) → S))
    (ker_map : Eq (α := Ideal R[X]) (RingHom.ker map) (Ideal.span {f}))
    (eq :
      ∀ (x : R[X]),
        Eq.{v + 1} (α := S)
          (({ map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f }.map :
                (a : R[X]) → S)
              x :
            S)
          ((h'.map : (a : R[X]) → S) x : S)),
    { map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f } = h'
⊢ h = h'

Tactic:
cases h
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h' : IsAdjoinRoot S f
map : R[X] →ₐ[R] S
map_surjective : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map : (a : R[X]) → S)
ker_map : Eq (α := Ideal R[X]) (RingHom.ker map) (Ideal.span {f})
eq :
  ∀ (x : R[X]),
    Eq.{v + 1} (α := S)
      (({ map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f }.map : (a : R[X]) → S)
          x :
        S)
      ((h'.map : (a : R[X]) → S) x : S)
mk :
  ∀ (map_1 : R[X] →ₐ[R] S)
    (map_surjective_1 : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map_1 : (a : R[X]) → S))
    (ker_map_1 : Eq (α := Ideal R[X]) (RingHom.ker map_1) (Ideal.span {f}))
    (eq :
      ∀ (x : R[X]),
        Eq.{v + 1} (α := S)
          (({ map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f }.map :
                (a : R[X]) → S)
              x :
            S)
          (({ map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 : IsAdjoinRoot S f }.map :
                (a : R[X]) → S)
              x :
            S)),
    { map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f } =
      { map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 }
⊢ { map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f } = h'

Tactic:
cases h'
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
map : R[X] →ₐ[R] S
map_surjective : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map : (a : R[X]) → S)
ker_map : Eq (α := Ideal R[X]) (RingHom.ker map) (Ideal.span {f})
map_1 : R[X] →ₐ[R] S
map_surjective_1 : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map_1 : (a : R[X]) → S)
ker_map_1 : Eq (α := Ideal R[X]) (RingHom.ker map_1) (Ideal.span {f})
eq :
  ∀ (x : R[X]),
    Eq.{v + 1} (α := S)
      (({ map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f }.map : (a : R[X]) → S)
          x :
        S)
      (({ map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 : IsAdjoinRoot S f }.map :
            (a : R[X]) → S)
          x :
        S)
mk : map = map_1
⊢ { map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f } =
    { map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 }

Tactic:
congr
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
map : R[X] →ₐ[R] S
map_surjective : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map : (a : R[X]) → S)
ker_map : Eq (α := Ideal R[X]) (RingHom.ker map) (Ideal.span {f})
map_1 : R[X] →ₐ[R] S
map_surjective_1 : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map_1 : (a : R[X]) → S)
ker_map_1 : Eq (α := Ideal R[X]) (RingHom.ker map_1) (Ideal.span {f})
eq :
  ∀ (x : R[X]),
    Eq.{v + 1} (α := S)
      (({ map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f }.map : (a : R[X]) → S)
          x :
        S)
      (({ map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 : IsAdjoinRoot S f }.map :
            (a : R[X]) → S)
          x :
        S)
⊢ map = map_1

Tactic:
AlgHom.ext eq

Premises used: AlgHom.ext
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
map : R[X] →ₐ[R] S
map_surjective : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map : (a : R[X]) → S)
ker_map : Eq (α := Ideal R[X]) (RingHom.ker map) (Ideal.span {f})
map_1 : R[X] →ₐ[R] S
map_surjective_1 : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map_1 : (a : R[X]) → S)
ker_map_1 : Eq (α := Ideal R[X]) (RingHom.ker map_1) (Ideal.span {f})
eq :
  ∀ (x : R[X]),
    Eq.{v + 1} (α := S)
      (({ map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f }.map : (a : R[X]) → S)
          x :
        S)
      (({ map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 : IsAdjoinRoot S f }.map :
            (a : R[X]) → S)
          x :
        S)
⊢ map = map_1

Tactic:
exact AlgHom.ext eq

Premises used: AlgHom.ext
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h h' : IsAdjoinRoot S f
eq : h.root = h'.root
x : R[X]
rw : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) x : S) ((h'.map : (a : R[X]) → S) x : S)
rw₁ : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) x : S) ((aeval h'.root : (a : R[X]) → S) x : S)
rw₂ rw₃ : Eq.{v + 1} (α := S) ((aeval h'.root : (a : R[X]) → S) x : S) ((aeval h'.root : (a : R[X]) → S) x : S)
⊢ Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) x : S) ((h'.map : (a : R[X]) → S) x : S)

Tactic:
rw [← h.aeval_root_eq_map, ← h'.aeval_root_eq_map, eq]

Premises used: IsAdjoinRoot.aeval_root_eq_map
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
x : S
⊢ (h.map : (a : R[X]) → S) (h.repr x) = x

Tactic:
(h.map_surjective x).choose_spec

Premises used: Exists.choose_spec, IsAdjoinRoot.map_surjective, IsAdjoinRoot.repr
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span {f}) (h.repr 0)

Tactic:
simp [← h.ker_map]

Premises used: IsAdjoinRoot.ker_map
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
x y : S
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span {f}) (h.repr (x + y) - (h.repr x + h.repr y))

Tactic:
simp [← h.ker_map]

Premises used: IsAdjoinRoot.ker_map
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
g : R[X]
⊢ Eq.{v + 1} (α := S)
    ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S) ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) g : AdjoinRoot f) :
      S)
    ((h.map : (a : R[X]) → S) g : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
a : AdjoinRoot f
rw :
  Eq.{v + 1} (α := S)
    ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
        ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f)
            (⋯.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
          AdjoinRoot f) :
      S)
    ((h.map : (a : R[X]) → S)
        (⋯.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
      S)
rw₁ rw₂ :
  Eq.{v + 1} (α := S)
    ((h.map : (a : R[X]) → S)
        (⋯.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
      S)
    ((h.map : (a : R[X]) → S)
        (⋯.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
      S)
⊢ Eq.{v + 1} (α := S) ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S) a : S)
    ((h.map : (a : R[X]) → S)
        (⋯.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
      S)

Tactic:
rw (occs := [1]) [← (AdjoinRoot.mk_surjective a).choose_spec, adjoinRootAlgEquiv_apply_mk]

Premises used: Exists.choose_spec, AdjoinRoot.mk_surjective, IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
a : S
rw :
  a =
    (h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
      ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) (h.repr a) : AdjoinRoot f)
rw₁ :
  Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (h.repr a) : S)
    ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
        ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) (h.repr a) : AdjoinRoot f) :
      S)
rw₂ rw₃ : Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (h.repr a) : S) ((h.map : (a : R[X]) → S) (h.repr a) : S)
⊢ Eq.{u + 1} (α := AdjoinRoot f) ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) a : AdjoinRoot f)
    ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) (h.repr a) : AdjoinRoot f)

Tactic:
rw (occs := [1]) [AlgEquiv.symm_apply_eq, ← h.map_repr a, adjoinRootAlgEquiv_apply_mk]

Premises used: AlgEquiv.symm_apply_eq, IsAdjoinRoot.map_repr, IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ (h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S) (AdjoinRoot.root f) = h.root

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, IsAdjoinRoot.root, Polynomial.X, rfl
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ (h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) h.root = AdjoinRoot.root f

Tactic:
(AlgEquiv.symm_apply_eq h.adjoinRootAlgEquiv).mpr rfl

Premises used: Iff.mpr, AlgEquiv.symm_apply_eq, IsAdjoinRoot.adjoinRootAlgEquiv, rfl
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
⊢ h.algEquiv h' = h.adjoinRootAlgEquiv.symm.trans h'.adjoinRootAlgEquiv

Tactic:
rfl

Premises used: rfl, IsAdjoinRoot.algEquiv
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
⊢ (h.algEquiv h' : (a : S) → T) h.root = h'.root

Tactic:
simp [algEquiv_def]

Premises used: IsAdjoinRoot.algEquiv_def
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
hX :
  Eq.{u_1 + 1} (α := T) (((↑(h.algEquiv h') : S →ₐ[R] T).comp h.map : (a : R[X]) → T) X : T)
    ((h'.map : (a : R[X]) → T) X : T)
⊢ (↑(h.algEquiv h') : S →ₐ[R] T).comp h.map = h'.map

Tactic:
ext
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
⊢ Eq.{u_1 + 1} (α := T) (((↑(h.algEquiv h') : S →ₐ[R] T).comp h.map : (a : R[X]) → T) X : T)
    ((h'.map : (a : R[X]) → T) X : T)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
z : R[X]
rw :
  Eq.{u_1 + 1} (α := T) ((h.algEquiv h' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
    (((↑(h.algEquiv h') : S →ₐ[R] T).comp h.map : (a : R[X]) → T) z : T)
⊢ Eq.{u_1 + 1} (α := T) ((h.algEquiv h' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
    ((h'.map : (a : R[X]) → T) z : T)

Tactic:
rw [← h.algEquiv_map h']

Premises used: IsAdjoinRoot.algEquiv_map
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
z : R[X]
⊢ Eq.{u_1 + 1} (α := T) ((h.algEquiv h' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
    (((↑(h.algEquiv h') : S →ₐ[R] T).comp h.map : (a : R[X]) → T) z : T)

Tactic:
simp [-algEquiv_map]

Premises used: IsAdjoinRoot.algEquiv_map
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
h₁ : ∀ (a : S), Eq (α := S) ((h.algEquiv h : (a : S) → S) a : S) ((AlgEquiv.refl : (a : S) → S) a : S)
⊢ h.algEquiv h = AlgEquiv.refl

Tactic:
ext
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
a : S
⊢ Eq (α := S) ((h.algEquiv h : (a : S) → S) a : S) ((AlgEquiv.refl : (a : S) → S) a : S)

Tactic:
simp [algEquiv_def]

Premises used: IsAdjoinRoot.algEquiv_def
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
⊢ (h.algEquiv h').symm = h'.algEquiv h

Tactic:
rfl

Premises used: AlgEquiv.symm, Quotient.liftOn', Equiv.trans, AddCon.liftOn, AlgEquiv.trans, Equiv.symm, rfl, IsAdjoinRoot.algEquiv
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
x : S
⊢ Eq.{u_2 + 1} (α := U) ((h'.algEquiv h'' : (a : T) → U) ((h.algEquiv h' : (a : S) → T) x : T) : U)
    ((h.algEquiv h'' : (a : S) → U) x : U)

Tactic:
simp [algEquiv_def]

Premises used: IsAdjoinRoot.algEquiv_def
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
h₁ :
  ∀ (a : S),
    Eq.{u_2 + 1} (α := U) (((h.algEquiv h').trans (h'.algEquiv h'') : (a : S) → U) a : U)
      ((h.algEquiv h'' : (a : S) → U) a : U)
⊢ (h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h''

Tactic:
ext
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
a : S
⊢ Eq.{u_2 + 1} (α := U) (((h.algEquiv h').trans (h'.algEquiv h'') : (a : S) → U) a : U)
    ((h.algEquiv h'' : (a : S) → U) a : U)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
e : S ≃ₐ[R] T
h₁ :
  ∀ (x : R[X]),
    Membership.mem (γ := Ideal R[X]) (RingHom.ker ((↑e : S →ₐ[R] T).comp h.map)) x ↔
      Membership.mem (γ := Ideal R[X]) (Ideal.span {f}) x
⊢ Eq (α := Ideal R[X]) (RingHom.ker ((↑e : S →ₐ[R] T).comp h.map)) (Ideal.span {f})

Tactic:
ext
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
e : S ≃ₐ[R] T
x : R[X]
⊢ Membership.mem (γ := Ideal R[X]) (RingHom.ker ((↑e : S →ₐ[R] T).comp h.map)) x ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {f}) x

Tactic:
simp [Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
⊢ (h.ofAlgEquiv e).root = (e : (a : S) → T) h.root

Tactic:
rfl

Premises used: IsAdjoinRoot.root, rfl
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
e : T ≃ₐ[R] U
h₁ :
  ∀ (a : S),
    Eq.{u_2 + 1} (α := U) ((h.algEquiv (h'.ofAlgEquiv e) : (a : S) → U) a : U)
      (((h.algEquiv h').trans e : (a : S) → U) a : U)
⊢ h.algEquiv (h'.ofAlgEquiv e) = (h.algEquiv h').trans e

Tactic:
ext a
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
e : T ≃ₐ[R] U
a : S
⊢ Eq.{u_2 + 1} (α := U) ((h.algEquiv (h'.ofAlgEquiv e) : (a : S) → U) a : U)
    (((h.algEquiv h').trans e : (a : S) → U) a : U)

Tactic:
simp [algEquiv_def, AlgEquiv.trans_apply, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply]

Premises used: IsAdjoinRoot.algEquiv_def, IsAdjoinRoot.adjoinRootAlgEquiv_apply_eq_map, IsAdjoinRoot.ofAlgEquiv_map_apply, AlgEquiv.trans_apply
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
h₁ :
  ∀ (a : T),
    Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).algEquiv h'' : (a : T) → U) a : U)
      ((e.symm.trans (h.algEquiv h'') : (a : T) → U) a : U)
⊢ (h.ofAlgEquiv e).algEquiv h'' = e.symm.trans (h.algEquiv h'')

Tactic:
ext a
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
h₁ :
  Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv : (a : T) → U) a : U)
    ((e.symm.trans (h.adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv) : (a : T) → U) a : U)
h₂ :
  Eq.{u_2 + 1} (α := U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f) :
      U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f) :
      U)
h₃ :
  Eq.{u + 1} (α := AdjoinRoot f) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f)
    ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f)
h₄ :
  a =
    ((h.ofAlgEquiv e).adjoinRootAlgEquiv : (a : AdjoinRoot f) → T)
      ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f)
h₅ :
  a =
    ((h.ofAlgEquiv e).map : (a : R[X]) → T)
      (Exists.choose (p := fun (a_1 : R[X]) ↦
        Eq (α := AdjoinRoot f) ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 : AdjoinRoot f)
          ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f))
        ⋯)
h₆ :
  a =
    (e : (a : S) → T)
      ((h.map : (a : R[X]) → S)
          (Exists.choose (p := fun (a_1 : R[X]) ↦
            Eq (α := AdjoinRoot f) ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 : AdjoinRoot f)
              ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f))
            ⋯) :
        S)
h₇ :
  a =
    (e : (a : S) → T)
      ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
          ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f) :
        S)
⊢ Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).algEquiv h'' : (a : T) → U) a : U)
    ((e.symm.trans (h.algEquiv h'') : (a : T) → U) a : U)

Tactic:
simp_rw [algEquiv_def, AlgEquiv.trans_apply, EmbeddingLike.apply_eq_iff_eq,
           AlgEquiv.symm_apply_eq, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply,
           ← adjoinRootAlgEquiv_apply_eq_map, AlgEquiv.apply_symm_apply]

Premises used: AlgEquiv.symm_apply_eq, AlgEquiv.apply_symm_apply, EmbeddingLike.apply_eq_iff_eq, IsAdjoinRoot.algEquiv_def, IsAdjoinRoot.adjoinRootAlgEquiv_apply_eq_map, IsAdjoinRoot.ofAlgEquiv_map_apply, AlgEquiv.trans_apply
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w : R[X]
hzw : (h.map : (a : R[X]) → S) w = z
⊢ f ∣ h.repr z - w

Tactic:
rw [eq_comm, ← sub_eq_zero, ← h.map_repr z, ← map_sub, h.map_eq_zero_iff] at hzw

Premises used: map_sub, sub_eq_zero, IsAdjoinRoot.map_repr, eq_comm, IsAdjoinRoot.map_eq_zero_iff
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w : R[X]
hzw : f ∣ h.repr z - w
obtain : ∀ (y : R[X]) (hy : h.repr z - w = f * y), eval₂ i x (h.repr z) = eval₂ i x w
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Tactic:
obtain ⟨y, hy⟩ := hzw