mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) +
          (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) +
        (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) +
      (2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆) =
    2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.span {C x, X - C y} = Ideal.span {X - C y} ⊔ Ideal.span {C x}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 = ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.map (↑(quotientSpanXSubCAlgEquiv y))
      (Ideal.map (Ideal.Quotient.mkₐ R (Ideal.span {X - C y})) (Ideal.span {C x})) =
    Ideal.span {x}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ p %ₘ q = 0 ↔ (Ideal.Quotient.mk (Ideal.span {q})) p = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst✝ : Invertible x
h✝ : ∃ i ∈ Ideal.map (algebraMap R ↥R[x]) I, ∃ j ∈ Ideal.span {⟨x, ⋯⟩}, i + j = 1
y : ↥R[x]
hy : y ∈ Ideal.map (algebraMap R ↥R[x]) I
z : ↥R[x]
hz : z ∈ Ideal.span {⟨x, ⋯⟩}
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
w : ↥R[x]
q : R[X]
hq : (aeval x) q = ↑w
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq : ↑y + ↑z = 1
hw : ↑z = ↑(⟨x, ⋯⟩ * w)
h : (1 - p - X * q).coeff 0 = 0
⊢ I = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ a ∈ I, ((Quotient.mk (map C I)).comp C) a = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst✝ : Invertible x
h : Ideal.map (algebraMap R ↥R[x]) I ⊔ Ideal.span {⟨x, ⋯⟩} = ⊤
⊢ ∃ p, p.leadingCoeff - 1 ∈ I ∧ (aeval ⅟x) p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆ = 2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ f ∈ map C I, (eval₂RingHom (C.comp (Quotient.mk I)) X) f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆) = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : CommSemiring K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
u : V₁ →ₗ[K] V₂
⊢ (toMatrix B₂.dualBasis B₁.dualBasis) (Dual.transpose u) = ((toMatrix B₁ B₂) u)ᵀ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : CommSemiring K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ (toLin B₁.dualBasis B₂.dualBasis) Mᵀ = Dual.transpose ((toLin B₂ B₁) M)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v w : n → R
⊢ { toFun := dotProduct (v + w), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ } + { toFun := dotProduct w, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
t : R
v : n → R
⊢ { toFun := dotProduct (t • v), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) t • { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
⊢ (fun f i ↦ f ((LinearMap.single R (fun a ↦ R) i) 1))
      ((fun v ↦ { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ }) v) =
    v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Dual R (n → R)
⊢ (fun v ↦ { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ })
      ((fun f i ↦ f ((LinearMap.single R (fun a ↦ R) i) 1)) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ pb.gen ∈ {pb.gen}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
⊢ ∃ a, b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
⊢ ∃ a, pb.gen ∣ b - (algebraMap A B) a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (aeval pb.gen) pb.minpolyGen = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ pb.minpolyGen.Monic

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
⊢ pb.dim ≤ p.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
h : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval h.gen) p = 0
⊢ ↑h.dim ≤ p.degree

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Function.LeftInverse ⇑(Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
    ⇑(eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ pb.minpolyGen.degree = ↑pb.dim

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ pb.minpolyGen = minpoly A pb.gen

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ (minpoly A pb.gen).degree = ↑pb.dim

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ (minpoly A pb.gen).natDegree = pb.dim

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x, -pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x

pp: case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x, (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x

Tactic:
· simp_rw [h, neg_smul, Finset.sum_neg_distrib, eq_neg_iff_add_eq_zero]
    convert! pb.aeval_minpolyGen
    rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, Finset.sum_range]

Goal state after:
case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x, (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Function.RightInverse ⇑(Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
    ⇑(eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f g : (R ⧸ I)[X]
⊢ (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) (f * g) =
    (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) f *
      (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f g : (R ⧸ I)[X]
⊢ (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) (f + g) =
    (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) f +
      (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ I.polynomialQuotientEquivQuotientPolynomial.symm ((Quotient.mk (map C I)) f) = Polynomial.map (Quotient.mk I) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ I.polynomialQuotientEquivQuotientPolynomial (Polynomial.map (Quotient.mk I) f) = (Quotient.mk (map C I)) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j ↦ if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : ↥((Quotient.mk I).comp C).range
hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
f : R[X]
n : ℕ
hf : i (f.coeff n) = 0
⊢ ((Quotient.mk I).comp C) (f.coeff n) = 0

Tactic:
rwa [Subtype.ext_iff, RingHom.coe_rangeRestrict] at hf

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : ↥((Quotient.mk I).comp C).range
hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
⊢ RingHom.ker (mapRingHom i) ≤ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ (f %ₘ minpoly A pb.gen).natDegree < pb.dim

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ((Quotient.mk I).comp C) y ∈ ((Quotient.mk I).comp C).range
hx : C ⟨((Quotient.mk I).comp C) y, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
this : C (i y) ∈ map (mapRingHom i) I
⊢ C y ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : ↥((Quotient.mk I).comp C).range
hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
⊢ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) f) = (aeval y) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R[X]
⊢ IsField R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
i : R
hi : i ∈ I
⊢ ((Ideal.Quotient.mk (Ideal.map C I)).comp C) i = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) pb.gen = y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) pb.gen = y

Tactic:
by
  convert! pb.constr_pow_aeval hy X <;> rw [aeval_X]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ a.support
this : coeff n a ∈ I
⊢ C ((Ideal.Quotient.mk I) (coeff n a)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) a = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
x : A
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((algebraMap A S) x) = (algebraMap A S') x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
x x' : S
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) (x * x') =
    ((pb.basis.constr A) fun i ↦ y ^ ↑i) x * ((pb.basis.constr A) fun i ↦ y ^ ↑i) x'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (a : R ⧸ I),
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (C a)) =
      C a

Tactic:
intro r
    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
    simp

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i).toFun 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i).toFun 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
f : S →ₐ[A] S'
⊢ (aeval (f pb.gen)) (minpoly A pb.gen) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
inst✝³ : Algebra A S
S' : Type u_7
inst✝² : Ring S'
inst✝¹ : Algebra A S'
inst✝ : IsDomain B
pb : PowerBasis A S
x : B
⊢ (aeval x) (minpoly A pb.gen) = 0 ↔ (Equiv.refl B) x ∈ (minpoly A pb.gen).aroots B

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0
⊢ (pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁) = AlgHom.id A S'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0
⊢ (pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂) = AlgHom.id A S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ Function.RightInverse
    (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) fun i ↦
      (Ideal.Quotient.mk (Ideal.map C I)) (X i))
    ⇑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
⊢ LinearIndependent K fun i ↦ x ^ ↑i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x y : S
hx : IsIntegral R x
hy : ∃ f, y = (aeval x) f
⊢ y ∈ Submodule.span R (Set.range fun i ↦ x ^ ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
K : Type u_6
inst✝² : Field K
S' : Type u_7
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
pb : PowerBasis R S
e : S ≃ₐ[R] S'
i : Fin pb.dim
⊢ (pb.basis.map ↑e) i = e pb.gen ^ ↑i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
⊢ (pb.map e).minpolyGen = pb.minpolyGen

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
⊢ pb.equivOfRoot (pb.map e) h₁ h₂ = e

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
⊢ R[B.gen] = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
x : S
hx : B.gen ∈ R[x]
⊢ R[x] = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ norm R = MonoidHom.id R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis (↥s) R S)
x : S
⊢ (norm R) x = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬Module.Finite R S
x : S
⊢ (norm R) x = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ (norm R) s = ((leftMulMatrix b) s).det

Tactic:
by

Goal state after: