awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
g_1 : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
g : K[X]
h :
  Eq (α := AdjoinRoot f) (Quot.mk (⇑(Submodule.quotientRel (span {f})) : K[X] → K[X] → Prop) g)
    ((aeval (root f) : (a : K[X]) → AdjoinRoot f) g)
⊢ ∃ (f_1 : K[X]),
    Eq (α := AdjoinRoot f) (Quot.mk (⇑(Submodule.quotientRel (span {f})) : K[X] → K[X] → Prop) g)
      ((aeval (root f) : (a : K[X]) → AdjoinRoot f) f_1)

Tactic:
use g
-- 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
g_1 : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
g : K[X]
h :
  Eq (α := AdjoinRoot f) (Quot.mk (⇑(Submodule.quotientRel (span {f})) : K[X] → K[X] → Prop) g)
    ((mk f : (a : K[X]) → AdjoinRoot f) g)
⊢ Eq (α := AdjoinRoot f) (Quot.mk (⇑(Submodule.quotientRel (span {f})) : K[X] → K[X] → Prop) g)
    ((aeval (root f) : (a : K[X]) → AdjoinRoot f) g)

Tactic:
rw [aeval_eq]

Premises used: AdjoinRoot.aeval_eq
-- 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
g_1 : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
g : K[X]
⊢ Eq (α := AdjoinRoot f) (Quot.mk (⇑(Submodule.quotientRel (span {f})) : K[X] → K[X] → Prop) g)
    ((mk f : (a : K[X]) → AdjoinRoot f) g)

Tactic:
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
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
⊢ ∀ (i : Fin f.natDegree), (powerBasisAux hf : (a : Fin f.natDegree) → AdjoinRoot f) i = root f ^ (↑i : ℕ)

Tactic:
simp [powerBasisAux]

Premises used: AdjoinRoot.powerBasisAux
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
rw : minpoly K (root f) = HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
rw₁ rw₂ :
  HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) =
    HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
⊢ minpoly K (powerBasis hf).gen = HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])

Tactic:
rw [powerBasis_gen, minpoly_root hf]

Premises used: AdjoinRoot.minpoly_root, AdjoinRoot.powerBasis_gen
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f.Monic
hf' : f ≠ 0
rw : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
rw₁ : f * (C : (a : K) → K[X]) 1⁻¹ = f
rw₂ : f * (C : (a : K) → K[X]) 1 = f
rw₃ : f * 1 = f
rw₄ rw₅ : f = f
⊢ minpoly K (powerBasis hf').gen = f

Tactic:
rw [minpoly_powerBasis_gen hf', hf.leadingCoeff, inv_one, C.map_one, mul_one]

Premises used: Polynomial.C, inv_one, RingHom.map_one, AdjoinRoot.minpoly_powerBasis_gen, Polynomial.Monic.leadingCoeff, mul_one
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
pos : ∀ (hf : f = 0), finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree
neg : ∀ (hf : ¬f = 0), finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree
⊢ finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f = 0
⊢ Eq (α := Submodule K[X] K[X]) (span {0}) ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f = 0
pos : finrank K K[X] = 0
⊢ finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree

Tactic:
rw [hf, natDegree_zero,
      ((Submodule.quotEquivOfEqBot _ (by simp)).restrictScalars K).finrank_eq]

Premises used: LinearEquiv.restrictScalars, Submodule.quotEquivOfEqBot, LinearEquiv.finrank_eq, Polynomial.natDegree_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f = 0
⊢ finrank K K[X] = 0

Tactic:
finrank_of_not_finite Polynomial.not_finite

Premises used: Module.finrank_of_not_finite, Polynomial.not_finite
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f = 0
⊢ finrank K K[X] = 0

Tactic:
exact finrank_of_not_finite Polynomial.not_finite

Premises used: Module.finrank_of_not_finite, Polynomial.not_finite
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : ¬f = 0
neg : (powerBasis hf).dim = f.natDegree
neg₁ : PowerBasis K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f}))
⊢ finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree

Tactic:
rw [PowerBasis.finrank]

Premises used: PowerBasis.finrank
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : ¬f = 0
⊢ (powerBasis hf).dim = f.natDegree

Tactic:
AdjoinRoot.powerBasis_dim hf

Premises used: AdjoinRoot.powerBasis_dim
-- 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
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
change :
  Eq.{u_2 + 1} (α := ↥R[x])
    ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯) : (a : R[X]) → ↥R[x])
        (minpoly R x) :
      ↥R[x])
    (0 : ↥R[x])
⊢ eval₂ (↑(ofId R ↥R[x]) : R →+* ↥R[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯) (minpoly R x) =
    0

Tactic:
change aeval _ _ = _

Premises used: Polynomial.aeval, DFunLike.coe
-- 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
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
⊢ Eq.{u_2 + 1} (α := ↥R[x])
    ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯) : (a : R[X]) → ↥R[x])
        (minpoly R x) :
      ↥R[x])
    (0 : ↥R[x])

Tactic:
simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe]

Premises used: Polynomial.aeval_subalgebra_coe, Subalgebra.coe_eq_zero
-- 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
x : S
⊢ Eq (α := (a : AdjoinRoot (minpoly R x)) → ↥R[x]) (⇑(toAdjoin R x) : (a : AdjoinRoot (minpoly R x)) → ↥R[x])
    (⇑(liftAlgHom (minpoly R x) (ofId R ↥R[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯) ⋯) :
      (a : AdjoinRoot (minpoly R x)) → ↥R[x])

Tactic:
rfl

Premises used: rfl
-- 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
x : S
⊢ (↑(((toAdjoin R x : AlgHom.{u_1, u_1, u_2} R (AdjoinRoot (minpoly R x)) ↥R[x]) :
            (a : AdjoinRoot (minpoly R x)) → ↥R[x])
          ((mk (minpoly R x) : (a : R[X]) → AdjoinRoot (minpoly R x)) X)) :
      S) =
    x

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
x : S
rw :
  LE.le (α := Subalgebra R ↥R[x])
    (adjoin R (Subtype.val (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) ⁻¹' {x}))
    (AlgHom.range (toAdjoin R x))
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly R x)) (β := ↥R[x])
    (⇑(toAdjoin R x) : (a : AdjoinRoot (minpoly R x)) → ↥R[x])

Tactic:
rw [← AlgHom.range_eq_top, _root_.eq_top_iff, ← adjoin_adjoin_coe_preimage]

Premises used: eq_top_iff, AlgHom.range_eq_top, Algebra.adjoin_adjoin_coe_preimage
-- 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
x : S
x_1 : ↥R[x]
y₁ : S
y₂ : Membership.mem (γ := Subalgebra R S) R[x] y₁
h :
  Membership.mem (γ := Set ↥R[x])
    (Subtype.val (p := fun (x_2 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_2) ⁻¹' {x})
    (Subtype.mk (p := fun (x_2 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_2) y₁ y₂)
⊢ ((AlgHom.toRingHom (toAdjoin R x) : RingHom.{u_1, u_2} (AdjoinRoot (minpoly R x)) ↥R[x]) :
        (a : AdjoinRoot (minpoly R x)) → ↥R[x])
      ((mk (minpoly R x) : (a : R[X]) → AdjoinRoot (minpoly R x)) X) =
    Subtype.mk (p := fun (x_2 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_2) y₁ y₂

Tactic:
simpa using h.symm

Premises used: Eq.symm
-- 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
x : S
⊢ LE.le (α := Subalgebra R ↥R[x])
    (adjoin R (Subtype.val (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) ⁻¹' {x}))
    (AlgHom.range (toAdjoin R x))

Tactic:
exact adjoin_le fun ⟨y₁, y₂⟩ h ↦ ⟨mk (minpoly R x) X, by simpa using h.symm⟩

Premises used: Algebra.adjoin_le
-- 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
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
x_1 : AdjoinRoot g
x : R[X]
change :
  Eq.{u_1 + 1} (α := AdjoinRoot g)
    ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) x) : AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
⊢ Eq.{u_1 + 1} (α := AdjoinRoot g)
    ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g)
        ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
          ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)) :
      AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)

Tactic:
change pb.lift _ _ (aeval _ _) = _

Premises used: PowerBasis.lift, Polynomial.aeval, DFunLike.coe
-- 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
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
x_1 : AdjoinRoot g
x : R[X]
rw :
  Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
rw₁ rw₂ :
  Eq (α := AdjoinRoot g) ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
⊢ Eq.{u_1 + 1} (α := AdjoinRoot g)
    ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) x) : AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)

Tactic:
rw [pb.lift_aeval, aeval_eq]

Premises used: PowerBasis.lift_aeval, AdjoinRoot.aeval_eq
-- 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
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
x : S
⊢ Nontrivial S

Tactic:
nontriviality S
-- 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
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
x : S
h : Nontrivial S
obtain :
  ∀ (f : R[X]) (_hf : f.natDegree < pb.dim),
    Eq.{u_2 + 1} (α := S)
      ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
          ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) f) : AdjoinRoot g) :
        S)
      ((aeval pb.gen : (a : R[X]) → S) f : S)
⊢ (liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
      ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) x : AdjoinRoot g) =
    x

Tactic:
obtain ⟨f, _hf, rfl⟩ := pb.exists_eq_aeval x

Premises used: PowerBasis.exists_eq_aeval, 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
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
h : Nontrivial S
f : R[X]
_hf : f.natDegree < pb.dim
rw :
  Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((aeval (root g) : (a : R[X]) → AdjoinRoot g) f : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
rw₁ :
  Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((mk g : (a : R[X]) → AdjoinRoot g) f : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
rw₂ : eval₂ (↑(Algebra.ofId R S) : R →+* S) pb.gen f = (aeval pb.gen : (a : R[X]) → S) f
rw₃ : eval₂ (↑(Algebra.ofId R S) : R →+* S) pb.gen f = eval₂ (algebraMap R S) pb.gen f
rw₄ rw₅ : eval₂ (algebraMap R S) pb.gen f = eval₂ (algebraMap R S) pb.gen f
⊢ Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) f) : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)

Tactic:
rw [pb.lift_aeval, aeval_eq, liftAlgHom_mk, Polynomial.aeval_def, Algebra.toRingHom_ofId]

Premises used: PowerBasis.lift_aeval, Algebra.toRingHom_ofId, Polynomial.aeval_def, AdjoinRoot.liftAlgHom_mk, AdjoinRoot.aeval_eq
-- 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
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
⊢ (↑(equiv' g pb h₁ h₂) : AdjoinRoot g →ₐ[R] S) = liftAlgHom g (Algebra.ofId R S) pb.gen h₂

Tactic:
rfl

Premises used: AdjoinRoot, AlgEquiv.toAlgHom, Quotient.liftOn', Set.Mem, AddCon.liftOn, AdjoinRoot.liftAlgHom, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AdjoinRoot.lift, AddCon.Quotient, rfl
-- 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
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
⊢ (↑(equiv' g pb h₁ h₂).symm : S →ₐ[R] AdjoinRoot g) = pb.lift (root g) h₁

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, AlgEquiv.toAlgHom, Finsupp.sum, PowerBasis.lift, Finset.sum, 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
L : Type u_6
F : Type u_7
inst : Field F
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
rw : HMul.hMul (β := F[X]) f ((C : (a : F) → F[X]) f.leadingCoeff⁻¹ : F[X]) ≠ 0
⊢ x ∈ aroots (minpoly F (powerBasis hf).gen) L ↔
    Membership.mem (α := L) (f.aroots L) ((Equiv.refl L : (a : L) → L) x : L)

Tactic:
rw [powerBasis_gen, minpoly_root hf, aroots_mul, aroots_C, add_zero, Equiv.refl_apply]

Premises used: AdjoinRoot.minpoly_root, Equiv.refl_apply, Polynomial.aroots_mul, add_zero, Polynomial.aroots_C, AdjoinRoot.powerBasis_gen
-- 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
L : Type u_6
F : Type u_7
inst : Field F
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ HMul.hMul (β := F[X]) f ((C : (a : F) → F[X]) f.leadingCoeff⁻¹ : F[X]) ≠ 0

Tactic:
(monic_mul_leadingCoeff_inv hf).ne_zero

Premises used: Polynomial.monic_mul_leadingCoeff_inv, Polynomial.Monic.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
L : Type u_6
F : Type u_7
inst : Field F
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ HMul.hMul (β := F[X]) f ((C : (a : F) → F[X]) f.leadingCoeff⁻¹ : F[X]) ≠ 0

Tactic:
exact (monic_mul_leadingCoeff_inv hf).ne_zero

Premises used: Polynomial.monic_mul_leadingCoeff_inv, Polynomial.Monic.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
I : Ideal R
f : R[X]
rw :
  Eq (α := Ideal (AdjoinRoot f)) (Ideal.map ((mk f).comp C) I)
    (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I))
rw₁ :
  Eq (α := Ideal (AdjoinRoot f)) (Ideal.map (F := R →+* AdjoinRoot f) (RingHom.comp (Ideal.Quotient.mk (span {f})) C) I)
    (Ideal.map (R := R[X]) (F := R[X] →+* AdjoinRoot f) (Ideal.Quotient.mk (span {f}))
      (Ideal.map (F := R →+* R[X]) C I))
rw₂ rw₃ :
  Eq (α := Ideal (AdjoinRoot f)) (Ideal.map (F := R →+* AdjoinRoot f) (RingHom.comp (Ideal.Quotient.mk (span {f})) C) I)
    (Ideal.map (F := R →+* AdjoinRoot f) (RingHom.comp (Ideal.Quotient.mk (span {f})) C) I)
⊢ Eq (α := Ideal (AdjoinRoot f)) (Ideal.map (of f) I) (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I))

Tactic:
rw [of, AdjoinRoot.mk, Ideal.map_map]

Premises used: AdjoinRoot.mk, Ideal.map_map, AdjoinRoot.of
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ Eq (α :=
    HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f))
      (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I)))
    ((quotMapOfEquivQuotMapCMapMk I f :
          (a : AdjoinRoot f ⧸ Ideal.map (of f) I) → AdjoinRoot f ⧸ Ideal.map (mk f) (Ideal.map C I))
        ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I) x) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f))
        (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I)))
    ((Ideal.Quotient.mk
            (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f}))
              (Ideal.Quotient.mk (span {f})) (Ideal.map (F := R →+* R[X]) C I)) :
          (a : R[X] ⧸ span {f}) → (R[X] ⧸ span {f}) ⧸ Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))
        x :
      HasQuotient.Quotient (HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f})) (B :=
        Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f})))
        (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f}))
          (Ideal.Quotient.mk (span {f})) (Ideal.map (F := R →+* R[X]) C I)))

Tactic:
rfl

Premises used: AdjoinRoot, Submodule.Quotient.mk, AdjoinRoot.mk, Quot.map, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
rw :
  Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((quotEquivOfEq ⋯ : (a : AdjoinRoot f ⧸ Ideal.map (mk f) (Ideal.map C I)) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((Ideal.Quotient.mk
              (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f}))
                (Ideal.Quotient.mk (span {f})) (Ideal.map (F := R →+* R[X]) C I)) :
            (a : R[X] ⧸ span {f}) → (R[X] ⧸ span {f}) ⧸ Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))
          x) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I) x :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
⊢ Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    (((quotMapOfEquivQuotMapCMapMk I f).symm :
          (a : AdjoinRoot f ⧸ Ideal.map (mk f) (Ideal.map C I)) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((Ideal.Quotient.mk
              (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f}))
                (Ideal.Quotient.mk (span {f})) (Ideal.map (F := R →+* R[X]) C I)) :
            (a : R[X] ⧸ span {f}) → (R[X] ⧸ span {f}) ⧸ Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))
          x) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I) x :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))

Tactic:
rw [quotMapOfEquivQuotMapCMapMk, Ideal.quotEquivOfEq_symm]

Premises used: Ideal.quotEquivOfEq_symm, AdjoinRoot.quotMapOfEquivQuotMapCMapMk
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((quotEquivOfEq ⋯ : (a : AdjoinRoot f ⧸ Ideal.map (mk f) (Ideal.map C I)) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((Ideal.Quotient.mk
              (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f}))
                (Ideal.Quotient.mk (span {f})) (Ideal.map (F := R →+* R[X]) C I)) :
            (a : R[X] ⧸ span {f}) → (R[X] ⧸ span {f}) ⧸ Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))
          x) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I) x :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))

Tactic:
Ideal.quotEquivOfEq_mk _ _

Premises used: AdjoinRoot, Ideal.quotEquivOfEq_mk, AdjoinRoot.mk
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((quotEquivOfEq ⋯ : (a : AdjoinRoot f ⧸ Ideal.map (mk f) (Ideal.map C I)) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((Ideal.Quotient.mk
              (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f}))
                (Ideal.Quotient.mk (span {f})) (Ideal.map (F := R →+* R[X]) C I)) :
            (a : R[X] ⧸ span {f}) → (R[X] ⧸ span {f}) ⧸ Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))
          x) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I) x :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))

Tactic:
exact Ideal.quotEquivOfEq_mk _ _

Premises used: Ideal.quotEquivOfEq_mk