awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
have rw₁ : Polynomial.eval x (Polynomial.map (algebraMap A B) P) = 0
Tactic: rw [Polynomial.aeval_def, ← Polynomial.eval_map,
      ← Polynomial.coe_mapRingHom (R := A), hp, MulSemiringAction.eval_charpoly]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
have 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
Tactic: rw [Polynomial.aeval_def, ← Polynomial.eval_map,
      ← Polynomial.coe_mapRingHom (R := A), hp, MulSemiringAction.eval_charpoly]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
have rw₃ : Polynomial.eval x (MulSemiringAction.charpoly G x) = 0
Tactic: rw [Polynomial.aeval_def, ← Polynomial.eval_map,
      ← Polynomial.coe_mapRingHom (R := A), hp, MulSemiringAction.eval_charpoly]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
have rw₄ : Eq.{u_2 + 1} (α := B) 0 0
Tactic: rw [Polynomial.aeval_def, ← Polynomial.eval_map,
      ← Polynomial.coe_mapRingHom (R := A), hp, MulSemiringAction.eval_charpoly]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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)
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
have this₁ : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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)
have 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)
Tactic: refine (DFunLike.congr_fun (Polynomial.aeval_algHom ((σ.restrictScalars A).comp
      (IsScalarTower.toAlgHom A (B ⧸ Q) k)) _) P).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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)
    ((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)
have rw : Eq.{u_3 + 1} (α := k)
  ((AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) : (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) → B ⧸ Q)
          P :
        B ⧸ Q) :
    k)
  (0 : k)
Tactic: rw [AlgHom.comp_apply, ← algebraMap_eq, Polynomial.aeval_algebraMap_apply, this,
      map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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)
rw :
  Eq.{u_3 + 1} (α := k)
    ((AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) : (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) → B ⧸ Q)
            P :
          B ⧸ Q) :
      k)
    (0 : k)
⊢ 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)
have rw₁ : Eq.{u_3 + 1} (α := k)
  ((AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) : (a : B ⧸ Q) → k)
      (((Polynomial.aeval (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) x) :
              AlgHom.{u_1, u_1, u_2} A (Polynomial A) (B ⧸ Q)) :
            (a : Polynomial A) → B ⧸ Q)
          P :
        B ⧸ Q) :
    k)
  (0 : k)
Tactic: rw [AlgHom.comp_apply, ← algebraMap_eq, Polynomial.aeval_algebraMap_apply, this,
      map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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)
rw :
  Eq.{u_3 + 1} (α := k)
    ((AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) : (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) → B ⧸ Q)
            P :
          B ⧸ Q) :
      k)
    (0 : k)
rw₁ :
  Eq.{u_3 + 1} (α := k)
    ((AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) : (a : B ⧸ Q) → k)
        (((Polynomial.aeval (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) x) :
                AlgHom.{u_1, u_1, u_2} A (Polynomial A) (B ⧸ Q)) :
              (a : Polynomial A) → B ⧸ Q)
            P :
          B ⧸ Q) :
      k)
    (0 : k)
⊢ 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)
have rw₂ : Eq.{u_3 + 1} (α := k)
  ((AlgHom.comp (AlgHom.restrictScalars A σ) (IsScalarTower.toAlgHom A (B ⧸ Q) k) : (a : B ⧸ Q) → k)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) ((Polynomial.aeval x : (a : Polynomial A) → B) P) : B ⧸ Q) :
    k)
  (0 : k)
Tactic: rw [AlgHom.comp_apply, ← algebraMap_eq, Polynomial.aeval_algebraMap_apply, this,
      map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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)
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
have 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)
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]