awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
rw : Polynomial.eval₂ (algebraMap A B) x P = 0
rw₁ : Polynomial.eval x (Polynomial.map (algebraMap A B) P) = 0
rw₂ :
  Polynomial.eval x
      (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P) =
    0
rw₃ : Polynomial.eval x (MulSemiringAction.charpoly G x) = 0
rw₄ rw₅ : Eq.{u_2 + 1} (α := B) 0 0
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)

Tactic:
rw [Polynomial.aeval_def, ← Polynomial.eval_map,
      ← Polynomial.coe_mapRingHom (R := A), hp, MulSemiringAction.eval_charpoly]

Premises used: Polynomial.eval_map, Polynomial.aeval_def, MulSemiringAction.eval_charpoly, Polynomial.coe_mapRingHom
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)

Tactic:
have : Polynomial.aeval x P = 0 := by
    rw [Polynomial.aeval_def, ← Polynomial.eval_map,
      ← Polynomial.coe_mapRingHom (R := A), hp, MulSemiringAction.eval_charpoly]
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this_2 : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
this : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
⊢ Eq.{u_3 + 1} (α := k)
    (((Polynomial.aeval
              ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
            Polynomial A →ₐ[A] k) :
          (a : Polynomial A) → k)
        P :
      k)
    (0 : k)

Tactic:
(DFunLike.congr_fun (Polynomial.aeval_algHom ((σ.restrictScalars A).comp
      (IsScalarTower.toAlgHom A (B ⧸ Q) k)) _) P).trans ?_

Premises used: DFunLike.congr_fun, IsScalarTower.toAlgHom, HasQuotient.Quotient, AlgHom.restrictScalars, AlgHom.comp, Polynomial.aeval_algHom, Eq.trans
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this_2 : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
this : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
refine :
  Eq.{u_3 + 1} (α := k)
    ((AlgHom.comp (B := B ⧸ Q)
            (AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) :
              AlgHom.{u_1, u_2, u_3} A (B ⧸ Q) k)
            (Polynomial.aeval ((mk Q : (a : B) → B ⧸ Q) x) : AlgHom.{u_1, u_1, u_2} A (Polynomial A) (B ⧸ Q)) :
          (a : Polynomial A) → k)
        P :
      k)
    (0 : k)
⊢ Eq.{u_3 + 1} (α := k)
    (((Polynomial.aeval
              ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
            Polynomial A →ₐ[A] k) :
          (a : Polynomial A) → k)
        P :
      k)
    (0 : k)

Tactic:
refine (DFunLike.congr_fun (Polynomial.aeval_algHom ((σ.restrictScalars A).comp
      (IsScalarTower.toAlgHom A (B ⧸ Q) k)) _) P).trans ?_

Premises used: DFunLike.congr_fun, IsScalarTower.toAlgHom, HasQuotient.Quotient, AlgHom.restrictScalars, AlgHom.comp, Polynomial.aeval_algHom, Eq.trans
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this_2 : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
this : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
⊢ Eq.{u_3 + 1} (α := k)
    (((Polynomial.aeval
              ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
            Polynomial A →ₐ[A] k) :
          (a : Polynomial A) → k)
        P :
      k)
    (0 : k)

Tactic:
have : Polynomial.aeval (σ (algebraMap (B ⧸ Q) k (mk _ x))) P = 0 := by
    refine (DFunLike.congr_fun (Polynomial.aeval_algHom ((σ.restrictScalars A).comp
      (IsScalarTower.toAlgHom A (B ⧸ Q) k)) _) P).trans ?_
    rw [AlgHom.comp_apply, ← algebraMap_eq, Polynomial.aeval_algebraMap_apply, this,
      map_zero, map_zero]
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this_2 : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
this_3 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := k)
    (((Polynomial.aeval
              ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
            Polynomial A →ₐ[A] k) :
          (a : Polynomial A) → k)
        P :
      k)
    (0 : k)
⊢ Eq.{u_3 + 1} (α := k)
    (((Polynomial.aeval
              ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
            Polynomial B →ₐ[B] k) :
          (a : Polynomial B) → k)
        (MulSemiringAction.charpoly G x) :
      k)
    (0 : k)

Tactic:
rw [← Polynomial.aeval_map_algebraMap B, ← Polynomial.coe_mapRingHom, hp] at this

Premises used: Polynomial.aeval_map_algebraMap, Polynomial.coe_mapRingHom
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this_2 : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
this_3 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := k)
    (((Polynomial.aeval
              ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
            Polynomial B →ₐ[B] k) :
          (a : Polynomial B) → k)
        (MulSemiringAction.charpoly G x) :
      k)
    (0 : k)
⊢ ∃ (τ : G),
    Eq (α := k) ((σ : (a : k) → k) ((algebraMap B k : (a : B) → k) x : k) : k)
      ((algebraMap B k : (a : B) → k) (τ • x) : k)

Tactic:
simpa [MulSemiringAction.charpoly, sub_eq_zero, Finset.prod_eq_zero_iff] using this

Premises used: sub_eq_zero, MulSemiringAction.charpoly, Finset.prod_eq_zero_iff
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this_2 : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
this_3 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := k)
    (((Polynomial.aeval
              ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
            Polynomial B →ₐ[B] k) :
          (a : Polynomial B) → k)
        (MulSemiringAction.charpoly G x) :
      k)
    (0 : k)
intro :
  ∀ (τ : G)
    (hτ :
      Eq (α := k) ((σ : (a : k) → k) ((algebraMap B k : (a : B) → k) x : k) : k)
        ((algebraMap B k : (a : B) → k) (τ • x) : k)),
    Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)

Tactic:
obtain ⟨τ, hτ⟩ : ∃ τ : G, σ (algebraMap _ _ x) = algebraMap _ _ (τ • x) := by
    simpa [MulSemiringAction.charpoly, sub_eq_zero, Finset.prod_eq_zero_iff] using this

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this_2 : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
this_3 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := k)
    (((Polynomial.aeval
              ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
            Polynomial B →ₐ[B] k) :
          (a : Polynomial B) → k)
        (MulSemiringAction.charpoly G x) :
      k)
    (0 : k)
τ : G
hτ :
  Eq (α := k) ((σ : (a : k) → k) ((algebraMap B k : (a : B) → k) x : k) : k)
    ((algebraMap B k : (a : B) → k) (τ • x) : k)
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)

Tactic:
⟨Ideal.Quotient.mk _ (τ • x), hτ.symm⟩

Premises used: Set.Mem, Ideal.Quotient.mk, setOf, Exists.intro, HSMul.hSMul, Set.range, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this_2 : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
this_3 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := k)
    (((Polynomial.aeval
              ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
            Polynomial B →ₐ[B] k) :
          (a : Polynomial B) → k)
        (MulSemiringAction.charpoly G x) :
      k)
    (0 : k)
τ : G
hτ :
  Eq (α := k) ((σ : (a : k) → k) ((algebraMap B k : (a : B) → k) x : k) : k)
    ((algebraMap B k : (a : B) → k) (τ • x) : k)
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)

Tactic:
exact ⟨Ideal.Quotient.mk _ (τ • x), hτ.symm⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)

Tactic:
have hf : Function.Injective f := FaithfulSMul.algebraMap_injective _ _