awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Adjoin.Tower
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
hyy :
  HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
⊢ (↑(Submonoid.closure (↑x : Set C)) : Set C) ⊆
    (↑(restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B)))
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))) :
      Set C)

Tactic:
fun r hr =>
    Submonoid.closure_induction (fun c hc => hxy c hc) (subset_span <| mem_insert_self _ _)
      (fun p q _ _ hp hq => hyy <| Submodule.mul_mem_mul hp hq) hr

Premises used: Set.Subset, Submonoid.closure_induction
-- Module: Mathlib.RingTheory.Adjoin.Tower
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
hyy :
  HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
⊢ (↑(Submonoid.closure (↑x : Set C)) : Set C) ⊆
    (↑(restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B)))
          (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))) :
      Set C)

Tactic:
refine fun r hr =>
    Submonoid.closure_induction (fun c hc => hxy c hc) (subset_span <| mem_insert_self _ _)
      (fun p q _ _ hp hq => hyy <| Submodule.mul_mem_mul hp hq) hr
-- Module: Mathlib.RingTheory.Adjoin.Tower
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
inst_7 : IsNoetherianRing A
hAC : Subalgebra.FG.{w, u_1} (R := A) (A := C) ⊤
hBC : Submodule.FG.{u₁, u_1} (R := B) (M := C) ⊤
hBCi : Function.Injective.{u₁ + 1, u_1 + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
⊢ Subalgebra.FG.{w, u₁} (R := A) (A := B) ⊤

Tactic:
let ⟨B₀, hAB₀, hB₀C⟩ := exists_subalgebra_of_fg A B C hAC hBC
  Algebra.fg_trans' (B₀.fg_top.2 hAB₀) <|
    Subalgebra.fg_of_submodule_fg <|
      have : IsNoetherianRing B₀ := isNoetherianRing_of_fg hAB₀
      have : Module.Finite B₀ C := ⟨hB₀C⟩
      fg_of_injective (IsScalarTower.toAlgHom B₀ B C).toLinearMap hBCi

Premises used: Iff.mpr, AlgHom.toLinearMap, Subalgebra.FG, IsScalarTower.toAlgHom, Subalgebra.fg_of_submodule_fg, Membership.mem, Subtype, Module.Finite.of_fg_top, exists_subalgebra_of_fg, Algebra.fg_trans', _private.0.fg_of_fg_of_fg.match_1, fg_of_injective, Subalgebra.fg_top, Top.top, isNoetherianRing_of_fg
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
h : f.degree ≠ 0
simp : ∀ (x : R), IsUnit x → ¬(C : (a : R) → R[X]) x = f
⊢ Nontrivial.{u_1} (AdjoinRoot f)

Tactic:
simp only [AdjoinRoot, Quotient.nontrivial_iff, Ne, span_singleton_eq_top,
    Polynomial.isUnit_iff, not_exists, not_and]

Premises used: AdjoinRoot, Polynomial.isUnit_iff, not_exists, Ideal.Quotient.nontrivial_iff, Ideal.span_singleton_eq_top, Ne, not_and
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x : R
hx : IsUnit x
h : degree.{u_1} (R := R) ((C : (a : R) → R[X]) x) ≠ 0
⊢ False

Tactic:
h (degree_C hx.ne_zero)

Premises used: Polynomial.degree_C, IsUnit.ne_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x : R
hx : IsUnit x
h : degree.{u_1} (R := R) ((C : (a : R) → R[X]) x) ≠ 0
⊢ False

Tactic:
exact h (degree_C hx.ne_zero)

Premises used: Polynomial.degree_C, IsUnit.ne_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
C : AdjoinRoot f → Prop
x : AdjoinRoot f
ih : ∀ (p : R[X]), C ((mk f : (a : R[X]) → AdjoinRoot f) p)
⊢ C x

Tactic:
Quotient.inductionOn' x ih

Premises used: Quotient.inductionOn'
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : DistribSMul S R
inst_2 : IsScalarTower S R R
a : S
x : R[X]
⊢ HSMul.hSMul (β := AdjoinRoot f) a ((mk f : (a : R[X]) → AdjoinRoot f) x : AdjoinRoot f) =
    (mk f : (a : R[X]) → AdjoinRoot f) (a • x)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, Quotient.map', rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : DistribSMul S R
inst_2 : IsScalarTower S R R
a : S
x : R
rw :
  HSMul.hSMul (β := AdjoinRoot f) a (((mk f).comp C : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
    ((mk f).comp C : (a : R) → AdjoinRoot f) (a • x)
rw₁ :
  HSMul.hSMul (β := AdjoinRoot f) a ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x) : AdjoinRoot f) =
    ((mk f).comp C : (a : R) → AdjoinRoot f) (a • x)
rw₂ :
  HSMul.hSMul (β := AdjoinRoot f) a ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x) : AdjoinRoot f) =
    (mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) (a • x))
rw₃ :
  Eq (α := AdjoinRoot f)
    ((mk f : (a : R[X]) → AdjoinRoot f) (HSMul.hSMul (β := R[X]) a ((C : (a : R) → R[X]) x : R[X])) : AdjoinRoot f)
    ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) (a • x)) : AdjoinRoot f)
rw₄ rw₅ :
  Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) (a • x)) : AdjoinRoot f)
    ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) (a • x)) : AdjoinRoot f)
⊢ HSMul.hSMul (β := AdjoinRoot f) a ((of f : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
    (of f : (a : R) → AdjoinRoot f) (a • x)

Tactic:
rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]

Premises used: AdjoinRoot.smul_mk, Polynomial.smul_C, RingHom.comp_apply, AdjoinRoot.of
-- 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]
R₁ : Type u_6
R₂ : Type u_7
inst_1 : SMul R₁ R₂
inst_2 : DistribSMul R₁ R
inst_3 : DistribSMul R₂ R
inst_4 : IsScalarTower R₁ R R
inst_5 : IsScalarTower R₂ R R
inst_6 : IsScalarTower R₁ R₂ R
f : R[X]
⊢ IsScalarTower.{u_6, u_7, u_1} R₁ R₂ (AdjoinRoot f)

Tactic:
inferInstanceAs <| IsScalarTower R₁ R₂ (_ ⧸ _)

Premises used: _private.0.AdjoinRoot.instIsScalarTower._proof_1
-- 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]
R₁ : Type u_6
R₂ : Type u_7
inst_1 : DistribSMul R₁ R
inst_2 : DistribSMul R₂ R
inst_3 : IsScalarTower R₁ R R
inst_4 : IsScalarTower R₂ R R
inst_5 : SMulCommClass R₁ R₂ R
f : R[X]
⊢ SMulCommClass.{u_6, u_7, u_1} R₁ R₂ (AdjoinRoot f)

Tactic:
inferInstanceAs <| SMulCommClass R₁ R₂ (_ ⧸ _)

Premises used: _private.0.AdjoinRoot.instSMulCommClass._proof_1
-- 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 g : R[X]
inst_1 : DistribSMul S R
inst_2 : IsScalarTower S R R
⊢ IsScalarTower.{u_2, u_1, u_1} S (AdjoinRoot f) (AdjoinRoot f)

Tactic:
inferInstanceAs <| IsScalarTower S (_ ⧸ _) (_ ⧸ _)

Premises used: _private.0.AdjoinRoot.isScalarTower_right._proof_1
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ (↑(mkₐ f) : R[X] →+* AdjoinRoot f) = mk f

Tactic:
rfl

Premises used: AdjoinRoot, Ideal.Quotient.mk, Submodule.Quotient.mk, MonoidHomClass.toMonoidHom, AdjoinRoot.mk, RingHomClass.toRingHom, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ Eq (α := (a : R[X]) → AdjoinRoot f) (⇑(mkₐ f) : (a : R[X]) → AdjoinRoot f) (⇑(mk f) : (a : R[X]) → AdjoinRoot f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ algebraMap R (AdjoinRoot f) = of f

Tactic:
rfl

Premises used: AdjoinRoot, AdjoinRoot.of, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : CommSemiring S
inst_2 : Algebra S R
⊢ Eq (α := RingHom.{u_2, u_1} S (AdjoinRoot f)) (algebraMap S (AdjoinRoot f)) ((of f).comp (algebraMap S R))

Tactic:
rfl

Premises used: AdjoinRoot, Submodule.Quotient.mk, 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 g : R[X]
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : FiniteType S R
⊢ FiniteType.{u_2, u_1} S (AdjoinRoot f)

Tactic:
inferInstanceAs <| FiniteType S (_ ⧸ (_ : Ideal R[X]))

Premises used: _private.0.AdjoinRoot.finiteType._proof_1
-- 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 g : R[X]
inst_1 : CommRing S
inst_2 : Algebra S R
inst_3 : FinitePresentation S R
⊢ FinitePresentation.{u_2, u_1} S (AdjoinRoot f)

Tactic:
.quotient (Submodule.fg_span_singleton f)

Premises used: AdjoinRoot, Submodule.fg_span_singleton, Algebra.FinitePresentation.quotient
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
p : R[X]
⊢ (↑(ofAlgHom S p) : R →+* AdjoinRoot p) = of p

Tactic:
rfl

Premises used: Submodule.Quotient.mk, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, AdjoinRoot.of, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
p : R[X]
⊢ Eq (α := (a : R) → AdjoinRoot p) (⇑(ofAlgHom S p) : (a : R) → AdjoinRoot p) (⇑(of p) : (a : R) → AdjoinRoot p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
T : Type u_3
inst : CommRing R
inst_1 : Semiring T
p : R[X]
f g : RingHom.{u_1, u_3} (AdjoinRoot p) T
hAlg : f.comp (of p) = g.comp (of p)
hRoot : Eq.{u_3 + 1} (α := T) ((f : (a : AdjoinRoot p) → T) (root p) : T) ((g : (a : AdjoinRoot p) → T) (root p) : T)
h : f.comp (Ideal.Quotient.mk (span {p})) = g.comp (Ideal.Quotient.mk (span {p}))
⊢ f = g

Tactic:
apply Ideal.Quotient.ringHom_ext

Premises used: Ideal.Quotient.ringHom_ext
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
T : Type u_3
inst : CommRing R
inst_1 : Semiring T
p : R[X]
f g : RingHom.{u_1, u_3} (AdjoinRoot p) T
hAlg : f.comp (of p) = g.comp (of p)
hRoot : Eq.{u_3 + 1} (α := T) ((f : (a : AdjoinRoot p) → T) (root p) : T) ((g : (a : AdjoinRoot p) → T) (root p) : T)
h :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := T) (((f.comp (Ideal.Quotient.mk (span {p}))).comp C : (a : R) → T) x : T)
      (((g.comp (Ideal.Quotient.mk (span {p}))).comp C : (a : R) → T) x : T)
h₁ :
  Eq.{u_3 + 1} (α := T) ((f.comp (Ideal.Quotient.mk (span {p})) : (a : R[X]) → T) X : T)
    ((g.comp (Ideal.Quotient.mk (span {p})) : (a : R[X]) → T) X : T)
⊢ f.comp (Ideal.Quotient.mk (span {p})) = g.comp (Ideal.Quotient.mk (span {p}))

Tactic:
ext x
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
T : Type u_3
inst : CommRing R
inst_1 : Semiring T
p : R[X]
f g : RingHom.{u_1, u_3} (AdjoinRoot p) T
hAlg : f.comp (of p) = g.comp (of p)
hRoot : Eq.{u_3 + 1} (α := T) ((f : (a : AdjoinRoot p) → T) (root p) : T) ((g : (a : AdjoinRoot p) → T) (root p) : T)
x : R
⊢ Eq.{u_3 + 1} (α := T) (((f.comp (Ideal.Quotient.mk (span {p}))).comp C : (a : R) → T) x : T)
    (((g.comp (Ideal.Quotient.mk (span {p}))).comp C : (a : R) → T) x : T)

Tactic:
simpa using congr($(hAlg) x)
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
T : Type u_3
inst : CommRing R
inst_1 : Semiring T
p : R[X]
f g : RingHom.{u_1, u_3} (AdjoinRoot p) T
hAlg : f.comp (of p) = g.comp (of p)
hRoot : Eq.{u_3 + 1} (α := T) ((f : (a : AdjoinRoot p) → T) (root p) : T) ((g : (a : AdjoinRoot p) → T) (root p) : T)
⊢ Eq.{u_3 + 1} (α := T) ((f.comp (Ideal.Quotient.mk (span {p})) : (a : R[X]) → T) X : T)
    ((g.comp (Ideal.Quotient.mk (span {p})) : (a : R[X]) → T) X : T)

Tactic:
simpa
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra S R
inst_4 : Algebra S T
p : R[X]
f g : AlgHom.{u_2, u_1, u_3} S (AdjoinRoot p) T
hAlg : f.comp (ofAlgHom S p) = g.comp (ofAlgHom S p)
hRoot : Eq.{u_3 + 1} (α := T) ((f : (a : AdjoinRoot p) → T) (root p) : T) ((g : (a : AdjoinRoot p) → T) (root p) : T)
a : Eq (α := RingHom.{u_1, u_3} (AdjoinRoot p) T) (↑f : AdjoinRoot p →+* T) (↑g : AdjoinRoot p →+* T)
⊢ f = g

Tactic:
apply AlgHom.coe_ringHom_injective

Premises used: AlgHom.coe_ringHom_injective
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra S R
inst_4 : Algebra S T
p : R[X]
f g : AlgHom.{u_2, u_1, u_3} S (AdjoinRoot p) T
hAlg : f.comp (ofAlgHom S p) = g.comp (ofAlgHom S p)
hRoot : Eq.{u_3 + 1} (α := T) ((f : (a : AdjoinRoot p) → T) (root p) : T) ((g : (a : AdjoinRoot p) → T) (root p) : T)
⊢ Eq (α := RingHom.{u_1, u_3} (AdjoinRoot p) T) (↑f : AdjoinRoot p →+* T) (↑g : AdjoinRoot p →+* T)

Tactic:
ringHom_ext congr(($hAlg).toRingHom) hRoot

Premises used: congrArg, id, AdjoinRoot.ringHom_ext, AlgHom.toRingHom
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra S R
inst_4 : Algebra S T
p : R[X]
f g : AlgHom.{u_2, u_1, u_3} S (AdjoinRoot p) T
hAlg : f.comp (ofAlgHom S p) = g.comp (ofAlgHom S p)
hRoot : Eq.{u_3 + 1} (α := T) ((f : (a : AdjoinRoot p) → T) (root p) : T) ((g : (a : AdjoinRoot p) → T) (root p) : T)
⊢ Eq (α := RingHom.{u_1, u_3} (AdjoinRoot p) T) (↑f : AdjoinRoot p →+* T) (↑g : AdjoinRoot p →+* T)

Tactic:
exact ringHom_ext congr(($hAlg).toRingHom) hRoot

Premises used: congrArg, id, AdjoinRoot.ringHom_ext, AlgHom.toRingHom
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : Semiring S
inst_2 : Algebra R S
g₁ g₂ : AdjoinRoot f →ₐ[R] S
h : Eq.{u_2 + 1} (α := S) ((g₁ : (a : AdjoinRoot f) → S) (root f) : S) ((g₂ : (a : AdjoinRoot f) → S) (root f) : S)
⊢ g₁ = g₂

Tactic:
Ideal.Quotient.algHom_ext R <| Polynomial.algHom_ext h

Premises used: AdjoinRoot, Polynomial.algHom_ext, Ideal.Quotient.algHom_ext
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f g h : R[X]
⊢ Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) g : AdjoinRoot f)
      ((mk f : (a : R[X]) → AdjoinRoot f) h : AdjoinRoot f) ↔
    f ∣ g - h

Tactic:
Ideal.Quotient.eq.trans Ideal.mem_span_singleton

Premises used: AdjoinRoot, Ideal.Quotient.eq, Iff.trans, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
rw rw₁ : f ∣ g ↔ f ∣ g
⊢ f ∣ g - 0 ↔ f ∣ g

Tactic:
rw [sub_zero]

Premises used: sub_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ f ∣ -f + 0

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : R
⊢ Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x) : AdjoinRoot f)
    ((of f : (a : R) → AdjoinRoot f) x : AdjoinRoot f)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ (mk f : (a : R[X]) → AdjoinRoot f) X = root f

Tactic:
rfl

Premises used: AdjoinRoot.root, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Monic
g : R[X]
h0 : g ≠ 0
hd : g.degree < f.degree
⊢ Ne (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) g : AdjoinRoot f) (0 : AdjoinRoot f)

Tactic:
mk_eq_zero.not.2 <| hf.not_dvd_of_degree_lt h0 hd

Premises used: Iff.mpr, AdjoinRoot.mk_eq_zero, Polynomial.Monic.not_dvd_of_degree_lt, Iff.not
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Monic
g : R[X]
h0 : g ≠ 0
hd : g.natDegree < f.natDegree
⊢ Ne (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) g : AdjoinRoot f) (0 : AdjoinRoot f)

Tactic:
mk_eq_zero.not.2 <| hf.not_dvd_of_natDegree_lt h0 hd

Premises used: Iff.mpr, Polynomial.Monic.not_dvd_of_natDegree_lt, AdjoinRoot.mk_eq_zero, Iff.not
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
a : R
C :
  Eq.{u_2 + 1} (α := AdjoinRoot f) ((algebraMap R (AdjoinRoot f) : (a : R) → AdjoinRoot f) a : AdjoinRoot f)
    ((of f : (a : S) → AdjoinRoot f) ((algebraMap R S : (a : R) → S) a) : AdjoinRoot f)
⊢ Eq.{u_2 + 1} (α := AdjoinRoot f)
    ((aeval (root f) : (a : R[X]) → AdjoinRoot f) ((Polynomial.C : (a : R) → R[X]) a) : AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) ((Polynomial.C : (a : R) → R[X]) a)) :
      AdjoinRoot f)

Tactic:
simp only [Polynomial.aeval_C, Polynomial.map_C, mk_C]

Premises used: Polynomial.aeval_C, Polynomial.map_C, AdjoinRoot.mk_C
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
a : R
C :
  Eq (α := AdjoinRoot f)
    ((algebraMap S (AdjoinRoot f) : (a : S) → AdjoinRoot f) ((algebraMap R S : (a : R) → S) a) : AdjoinRoot f)
    ((of f : (a : S) → AdjoinRoot f) ((algebraMap R S : (a : R) → S) a) : AdjoinRoot f)
⊢ Eq.{u_2 + 1} (α := AdjoinRoot f) ((algebraMap R (AdjoinRoot f) : (a : R) → AdjoinRoot f) a : AdjoinRoot f)
    ((of f : (a : S) → AdjoinRoot f) ((algebraMap R S : (a : R) → S) a) : AdjoinRoot f)

Tactic:
rw [IsScalarTower.algebraMap_apply R S]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
a : R
⊢ Eq (α := AdjoinRoot f)
    ((algebraMap S (AdjoinRoot f) : (a : S) → AdjoinRoot f) ((algebraMap R S : (a : R) → S) a) : AdjoinRoot f)
    ((of f : (a : S) → AdjoinRoot f) ((algebraMap R S : (a : R) → S) a) : AdjoinRoot f)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
p q : R[X]
h :
  Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) p) : AdjoinRoot f)
h_1 :
  Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) q : AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) q) : AdjoinRoot f)
⊢ Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) (p + q) : AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) (p + q)) : AdjoinRoot f)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
n : ℕ
a : R
h :
  Eq.{u_2 + 1} (α := AdjoinRoot f)
    ((aeval (root f) : (a : R[X]) → AdjoinRoot f)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
      AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f)
        (Polynomial.map (algebraMap R S)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))) :
      AdjoinRoot f)
⊢ Eq.{u_2 + 1} (α := AdjoinRoot f)
    ((aeval (root f) : (a : R[X]) → AdjoinRoot f)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
      AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f)
        (Polynomial.map (algebraMap R S)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) :
      AdjoinRoot f)

Tactic:
simp_all [pow_add, ← mul_assoc]

Premises used: mul_assoc, pow_add
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
p : R[X]
C :
  ∀ (a : R),
    Eq.{u_2 + 1} (α := AdjoinRoot f)
      ((aeval (root f) : (a : R[X]) → AdjoinRoot f) ((Polynomial.C : (a : R) → R[X]) a) : AdjoinRoot f)
      ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) ((Polynomial.C : (a : R) → R[X]) a)) :
        AdjoinRoot f)
add :
  ∀ (p q : R[X]),
    Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
        ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) p) : AdjoinRoot f) →
      Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) q : AdjoinRoot f)
          ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) q) : AdjoinRoot f) →
        Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) (p + q) : AdjoinRoot f)
          ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) (p + q)) : AdjoinRoot f)
monomial :
  ∀ (n : ℕ) (a : R),
    Eq.{u_2 + 1} (α := AdjoinRoot f)
        ((aeval (root f) : (a : R[X]) → AdjoinRoot f)
            (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
          AdjoinRoot f)
        ((mk f : (a : S[X]) → AdjoinRoot f)
            (Polynomial.map (algebraMap R S)
              (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))) :
          AdjoinRoot f) →
      Eq.{u_2 + 1} (α := AdjoinRoot f)
        ((aeval (root f) : (a : R[X]) → AdjoinRoot f)
            (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
          AdjoinRoot f)
        ((mk f : (a : S[X]) → AdjoinRoot f)
            (Polynomial.map (algebraMap R S)
              (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) :
          AdjoinRoot f)
⊢ Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) p) : AdjoinRoot f)

Tactic:
induction p using Polynomial.induction_on with
  | C a =>
    simp only [Polynomial.aeval_C, Polynomial.map_C, mk_C]
    rw [IsScalarTower.algebraMap_apply R S]
    simp
  | add p q _ _ => simp_all
  | monomial n a _ => simp_all [pow_add, ← mul_assoc]

Premises used: Polynomial.C, mul_assoc, pow_add, Polynomial.monomial, Polynomial.aeval_C, Polynomial.map_C, IsScalarTower.algebraMap_apply, AdjoinRoot.mk_C