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 : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
rw :
  Eq.{u + 1} (α := R) (Pi.single (M := fun (x : ℕ) ↦ R) n 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
    (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R)
rw₁ rw₂ : Eq.{u + 1} (α := R) (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R) (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R)
⊢ Eq.{u + 1} (α := R)
    (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
    (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R)

Tactic:
rw [Fin.val_mk, Fin.val_mk]

Premises used: Fin.val_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 : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
rw :
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
              ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
            Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
rw₁ :
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
              ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
            Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
rw₂ :
  Eq.{u + 1} (α := R)
    (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
    (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R)
⊢ Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)

Tactic:
calc
      h.basis.repr (h.root ^ n) ⟨i, _⟩ = h.basis.repr (h.basis ⟨n, hn⟩) ⟨i, hi⟩ := by
        rw [h.basis_apply, Fin.val_mk]
      _ = Pi.single (M := fun _ => R) ((⟨n, hn⟩ : Fin _) : ℕ) (1 : (fun _ => R) n)
        ↑(⟨i, _⟩ : Fin _) := by
        rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
      _ = Pi.single (M := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]

Premises used: IsAdjoinRootMonic.toIsAdjoinRoot, Fin.mk, Pi.single, IsAdjoinRoot.root, Module.Basis.repr, Fin.val, IsAdjoinRootMonic.basis, HPow.hPow, OfNat.ofNat, DFunLike.coe
-- 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 : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : ¬i < f.natDegree
neg : i ≠ n
⊢ Eq.{u + 1} (α := R) (0 : R) (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)

Tactic:
rw [Pi.single_eq_of_ne]

Premises used: Pi.single_eq_of_ne
-- 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 : IsAdjoinRootMonic S f
i : ℕ
hi : ¬i < f.natDegree
hn : i < f.natDegree
⊢ False

Tactic:
simp [hi] at hn
-- 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 : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
rw :
  Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) 1 : ℕ → R)
    ((h.coeff : (a : S) → ℕ → R) (HPow.hPow (β := ℕ) h.root 0) : ℕ → R)
rw₁ rw₂ : Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) 1 : ℕ → R) ((h.coeff : (a : S) → ℕ → R) 1 : ℕ → R)
⊢ Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) 1 : ℕ → R) (Pi.single (M := fun (j : ℕ) ↦ R) 0 1 : (j : ℕ) → R)

Tactic:
rw [← h.coeff_root_pow h.deg_pos, pow_zero]

Premises used: pow_zero, IsAdjoinRootMonic.deg_pos, IsAdjoinRootMonic.coeff_root_pow
-- 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 : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
rw :
  Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) h.root : ℕ → R)
    ((h.coeff : (a : S) → ℕ → R) (HPow.hPow (β := ℕ) h.root 1) : ℕ → R)
rw₁ rw₂ :
  Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) h.root : ℕ → R) ((h.coeff : (a : S) → ℕ → R) h.root : ℕ → R)
⊢ Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) h.root : ℕ → R)
    (Pi.single (M := fun (j : ℕ) ↦ R) 1 1 : (j : ℕ) → R)

Tactic:
rw [← h.coeff_root_pow hdeg, pow_one]

Premises used: pow_one, IsAdjoinRootMonic.coeff_root_pow
-- 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 : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
x : R
h₁ :
  ∀ (i : ℕ),
    Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) ((algebraMap R S : (a : R) → S) x : S) i : R)
      (Pi.single (M := fun (j : ℕ) ↦ R) 0 x i : R)
⊢ Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) ((algebraMap R S : (a : R) → S) x : S) : ℕ → R)
    (Pi.single (M := fun (j : ℕ) ↦ R) 0 x : (j : ℕ) → R)

Tactic:
ext i
-- 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 : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
x : R
i : ℕ
h₁ : HMul.hMul (β := R) x (Pi.single (M := fun (j : ℕ) ↦ R) 0 1 i : R) = Pi.single (M := fun (j : ℕ) ↦ R) 0 x i
⊢ Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) ((algebraMap R S : (a : R) → S) x : S) i : R)
    (Pi.single (M := fun (j : ℕ) ↦ R) 0 x i : R)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, map_smul, coeff_one, Pi.smul_apply, smul_eq_mul]

Premises used: Algebra.algebraMap_eq_smul_one, IsAdjoinRootMonic.coeff_one, smul_eq_mul, map_smul, Pi.smul_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 : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
x : R
i : ℕ
⊢ Eq.{u + 1} (α := R) (Pi.single (M := fun (x : ℕ) ↦ R) 0 (x * 1) i : R) (Pi.single (M := fun (j : ℕ) ↦ R) 0 x i : R)

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 : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
x : R
i : ℕ
h₁ : ∀ (i : ℕ), Eq.{u + 1} (α := R) ((fun (x_1 : ℕ) (y : R) ↦ x * y) i 0) 0
⊢ HMul.hMul (β := R) x (Pi.single (M := fun (j : ℕ) ↦ R) 0 1 i : R) = Pi.single (M := fun (j : ℕ) ↦ R) 0 x i

Tactic:
refine (Pi.apply_single (fun _ y => x * y) ?_ 0 1 i).trans (by simp)

Premises used: HMul.hMul, Pi.apply_single, OfNat.ofNat, Eq.trans
-- 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 : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
x : R
i : ℕ
⊢ ∀ (i : ℕ), Eq.{u + 1} (α := R) ((fun (x_1 : ℕ) (y : R) ↦ x * y) i 0) 0

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 : IsAdjoinRootMonic S f
x y : S
hxy : ∀ i < f.natDegree, Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x i : R) ((h.coeff : (a : S) → ℕ → R) y i : R)
i : Fin f.natDegree
rw :
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) x : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R) i : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
rw₁ :
  Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
rw₂ :
  Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) y : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R) i : R)
rw₃ : Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R) ((h.coeff : (a : S) → ℕ → R) y (↑i : ℕ) : R)
rw₄ rw₅ : Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) y (↑i : ℕ) : R) ((h.coeff : (a : S) → ℕ → R) y (↑i : ℕ) : R)
⊢ Eq.{u + 1} (α := R) ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) x i : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)

Tactic:
rw [Basis.equivFun_apply, ← h.coeff_apply_coe, Basis.equivFun_apply, ← h.coeff_apply_coe,
        hxy i i.prop]

Premises used: Fin.prop, Fin.val, Module.Basis.equivFun_apply, IsAdjoinRootMonic.coeff_apply_coe
-- 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 : IsAdjoinRootMonic S f
x y : S
⊢ x = y ↔
    ∀ i < f.natDegree, Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x i : R) ((h.coeff : (a : S) → ℕ → R) y i : R)

Tactic:
⟨fun hxy _ _=> hxy ▸ rfl, fun hxy => h.ext_elem hxy⟩

Premises used: Eq.rec, Iff.intro, IsAdjoinRootMonic.ext_elem, 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 : IsAdjoinRootMonic S f
⊢ Function.Injective.{v + 1, u + 1} (α := S) (β := ℕ → R) (⇑h.coeff : (a : S) → ℕ → R)

Tactic:
fun _ _ hxy =>
  h.ext_elem fun _ _ => hxy ▸ rfl

Premises used: Eq.rec, IsAdjoinRootMonic.ext_elem, Function.Injective, 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 : IsAdjoinRootMonic S f
⊢ IsIntegral R h.root

Tactic:
⟨f, h.monic, h.aeval_root_self⟩

Premises used: IsAdjoinRootMonic.toIsAdjoinRoot, RingHom.IsIntegralElem, IsIntegral, And.intro, Exists.intro, IsAdjoinRoot.aeval_root_self, IsAdjoinRootMonic.monic
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
x : S
rw :
  Eq (α := S) ((h.lift (algebraMap R S) h.root ⋯ : (a : S) → S) ((h.map : (a : R[X]) → S) (h.repr x) : S) : S)
    ((h.map : (a : R[X]) → S) (h.repr x) : S)
rw₁ : eval₂ (algebraMap R S) h.root (h.repr x) = (h.map : (a : R[X]) → S) (h.repr x)
rw₂ : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) (h.repr x) : S) ((h.map : (a : R[X]) → S) (h.repr x) : S)
rw₃ rw₄ : Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (h.repr x) : S) ((h.map : (a : R[X]) → S) (h.repr x) : S)
⊢ (h.lift (algebraMap R S) h.root ⋯ : (a : S) → S) x = x

Tactic:
rw [← h.map_repr x, lift_map, ← aeval_def, h.aeval_root_eq_map]

Premises used: IsAdjoinRoot.map_repr, Polynomial.aeval_def, IsAdjoinRoot.lift_map, IsAdjoinRoot.aeval_root_eq_map
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
⊢ h.lift (algebraMap R S) h.root ⋯ = RingHom.id S

Tactic:
RingHom.ext h.lift_self_apply

Premises used: RingHom.ext, IsAdjoinRoot.lift_self_apply
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : Eq (α := Subalgebra R S) R[α] ⊤
rw : Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R[X]) (⇑(aeval α) : (a : R[X]) → S)) Set.univ
rw₁ : (↑(AlgHom.range (aeval α)) : Set S) = Set.univ
rw₂ : (↑R[α] : Set S) = Set.univ
rw₃ : (↑⊤ : Set S) = Set.univ
rw₄ rw₅ : Eq.{v + 1} (α := Set S) Set.univ Set.univ
⊢ Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)

Tactic:
rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← Algebra.adjoin_singleton_eq_range_aeval,
      hα₂, Algebra.coe_top]

Premises used: Set.range_eq_univ, AlgHom.coe_range, Algebra.coe_top, Algebra.adjoin_singleton_eq_range_aeval
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : Eq (α := Subalgebra R S) R[α] ⊤
h₁ :
  ∀ (x : R[X]),
    Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] S) (aeval α)) x ↔
      Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R α}) x
⊢ Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] S) (aeval α)) (Ideal.span {minpoly R α})

Tactic:
ext
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : Eq (α := Subalgebra R S) R[α] ⊤
x : R[X]
⊢ Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] S) (aeval α)) x ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R α}) x

Tactic:
simpa [Ideal.mem_span_singleton] using minpoly.isIntegrallyClosed_dvd_iff hα _

Premises used: minpoly.isIntegrallyClosed_dvd_iff, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : Eq (α := Subalgebra R S) R[α] ⊤
⊢ (mkOfAdjoinEqTop hα hα₂).root = α

Tactic:
simp [IsAdjoinRoot.root]

Premises used: IsAdjoinRoot.root
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst_5 : CommRing U
i : R →+* U
x : U
hx : eval₂ i x f = 0
z : S
rw :
  Eq.{u_2 + 1} (α := U)
    ((h'.lift i x hx : (a : T) → U) ((h.algEquiv h' : (a : S) → T) ((h.map : (a : R[X]) → S) (h.repr z) : S) : T) : U)
    ((h.lift i x hx : (a : S) → U) ((h.map : (a : R[X]) → S) (h.repr z) : S) : U)
⊢ Eq.{u_2 + 1} (α := U) ((h'.lift i x hx : (a : T) → U) ((h.algEquiv h' : (a : S) → T) z : T) : U)
    ((h.lift i x hx : (a : S) → U) z : U)

Tactic:
rw [← h.map_repr z]

Premises used: IsAdjoinRoot.map_repr
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst_5 : CommRing U
i : R →+* U
x : U
hx : eval₂ i x f = 0
z : S
⊢ Eq.{u_2 + 1} (α := U)
    ((h'.lift i x hx : (a : T) → U) ((h.algEquiv h' : (a : S) → T) ((h.map : (a : R[X]) → S) (h.repr z) : S) : T) : U)
    ((h.lift i x hx : (a : S) → U) ((h.map : (a : R[X]) → S) (h.repr z) : S) : U)

Tactic:
simp [-map_repr]

Premises used: IsAdjoinRoot.map_repr
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst_5 : CommRing U
inst_6 : Algebra R U
x : U
hx : Eq.{u_2 + 1} (α := U) ((aeval x : (a : R[X]) → U) f : U) (0 : U)
z : S
⊢ Eq.{u_2 + 1} (α := U) ((h'.liftHom x hx : (a : T) → U) ((h.algEquiv h' : (a : S) → T) z : T) : U)
    ((h.liftHom x hx : (a : S) → U) z : U)

Tactic:
h.lift_algEquiv h' _ _ hx _

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, IsAdjoinRoot.lift_algEquiv
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
hirr : Irreducible f
q : R[X]
hq : f = minpoly R h.root * q
⊢ Associated (minpoly R h.root * q) (HMul.hMul (α := R[X]) (minpoly R h.root) 1)

Tactic:
Associated.mul_left (minpoly R h.root) <|
          associated_one_iff_isUnit.2 <|
            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root

Premises used: Iff.mpr, IsAdjoinRootMonic.toIsAdjoinRoot, associated_one_iff_isUnit, Or.resolve_left, IsAdjoinRoot.root, minpoly, Irreducible.isUnit_or_isUnit, minpoly.not_isUnit, Associated.mul_left
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
hirr : Irreducible f
q : R[X]
hq : f = minpoly R h.root * q
h₁ : minpoly R h.root = HMul.hMul (α := R[X]) (minpoly R h.root) 1
⊢ Associated f (minpoly R h.root)

Tactic:
convert!
        Associated.mul_left (minpoly R h.root) <|
          associated_one_iff_isUnit.2 <|
            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root

Premises used: Iff.mpr, IsAdjoinRootMonic.toIsAdjoinRoot, associated_one_iff_isUnit, Or.resolve_left, IsAdjoinRoot.root, minpoly, Irreducible.isUnit_or_isUnit, minpoly.not_isUnit, Associated.mul_left
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
hirr : Irreducible f
q : R[X]
hq : f = minpoly R h.root * q
h₁ h₂ : Eq (α := R[X]) (minpoly R h.root) (minpoly R h.root)
⊢ minpoly R h.root = HMul.hMul (α := R[X]) (minpoly R h.root) 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
rw :
  ∀ (hα : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)),
    let f : R[X] := minpoly R α;
    ∀ (hf : Monic (minpoly R α)),
      let φ := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯;
      Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
⊢ Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)

Tactic:
rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα

Premises used: Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
s : S
obtain : ∀ (p : R[X]) (hp : (aeval α : (a : R[X]) → S) p = s), ∃ (a : AdjoinRoot f), (φ : (a : AdjoinRoot f) → S) a = s
⊢ ∃ (a : AdjoinRoot f), (φ : (a : AdjoinRoot f) → S) a = s

Tactic:
obtain ⟨p, hp⟩ := hα s
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
s : S
p : R[X]
hp : (aeval α : (a : R[X]) → S) p = s
⊢ (φ : (a : AdjoinRoot f) → S) ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f) = s

Tactic:
simp [φ, ← aeval_def, hp]

Premises used: Polynomial.aeval_def
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
s : S
p : R[X]
hp : (aeval α : (a : R[X]) → S) p = s
⊢ ∃ (a : AdjoinRoot f), (φ : (a : AdjoinRoot f) → S) a = s

Tactic:
exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
⊢ Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)

Tactic:
have hφ : Function.Surjective φ := by
        rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
        intro s; obtain ⟨p, hp⟩ := hα s
        exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
⊢ Free R (AdjoinRoot (minpoly R α))

Tactic:
haveI := hf.free_adjoinRoot
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this : Free R (AdjoinRoot (minpoly R α))
⊢ Module.Finite R (AdjoinRoot (minpoly R α))

Tactic:
haveI := hf.finite_adjoinRoot
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this_1 : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
pos :
  ∀ (h : Nontrivial R),
    Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
neg :
  ∀ (h : ¬Nontrivial R),
    Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)

Tactic:
by_cases h : Nontrivial R

Premises used: Nontrivial