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
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.stabilizerHom Q P G :
                    MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                      (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                  (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                g :
              AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
⊢ Eq (α := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
            (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
          L) :
      L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
have intro : ∀ (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
  (hb :
    ∀ (g : G),
      Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)),
  Eq (α := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
            (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
          L) :
      L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
Tactic: obtain ⟨a, b, ha1, ha2, hb⟩ := fixed_of_fixed1_aux2 G Q b₀ (fun g hg ↦ hx ⟨g, hg⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.stabilizerHom Q P G :
                    MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                      (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                  (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                g :
              AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
⊢ Eq (α := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
            (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
          L) :
      L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
have intro : ∀ (M : A[X]) (key : Eq (α := B[X]) (map (algebraMap A B) M) (MulSemiringAction.charpoly G b)),
  Eq (α := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
            (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
          L) :
      L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
Tactic: obtain ⟨M, key⟩ := (mem_lifts _).mp (Algebra.IsInvariant.charpoly_mem_lifts A B G b)
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.stabilizerHom Q P G :
                    MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                      (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                  (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                g :
              AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key : Eq (α := B[X]) (map (algebraMap A B) M) (MulSemiringAction.charpoly G b)
⊢ Eq (α := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
            (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
          L) :
      L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
have key₁ : Eq (α := (B ⧸ Q)[X]) (map (algebraMap B (B ⧸ Q)) (map (algebraMap A B) M))
  (map (algebraMap B (B ⧸ Q)) (MulSemiringAction.charpoly G b))
Tactic: replace key := congrArg (map (algebraMap B (B ⧸ Q))) key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.stabilizerHom Q P G :
                    MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                      (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                  (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                g :
              AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key :
  Eq (α := (B ⧸ Q)[X]) (map (algebraMap B (B ⧸ Q)) (map (algebraMap A B) M))
    (map (algebraMap B (B ⧸ Q)) (MulSemiringAction.charpoly G b))
⊢ Eq (α := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
            (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
          L) :
      L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
have key₁ : Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M))
  (∏ i : G, map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (i • b) : B[X])))
Tactic: rw [map_map, ← algebraMap_eq, algebraMap_eq A (A ⧸ P) (B ⧸ Q),
      ← map_map, MulSemiringAction.charpoly, Polynomial.map_prod] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.stabilizerHom Q P G :
                    MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                      (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                  (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                g :
              AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key :
  Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M))
    (∏ i : G, map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (i • b) : B[X])))
g : G
⊢ map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
    if g • Q = Q then
      HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
        ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
    else X
have rw : HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
    ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0)) :
      (B ⧸ Q)[X]) =
  if g • Q = Q then
    HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
      ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
  else X
Tactic: rw [Polynomial.map_sub, map_X, map_C, hb]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.stabilizerHom Q P G :
                    MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                      (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                  (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                g :
              AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key :
  Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M))
    (∏ i : G, map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (i • b) : B[X])))
g : G
⊢ HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
      ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0)) :
        (B ⧸ Q)[X]) =
    if g • Q = Q then
      HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
        ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
    else X
have pos : g • Q = Q →
  HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
      ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X]) =
    HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
      ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.stabilizerHom Q P G :
                    MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                      (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                  (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                g :
              AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key :
  Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M))
    (∏ i : G, map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (i • b) : B[X])))
g : G
pos :
  g • Q = Q →
    HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
        ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X]) =
      HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
        ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
⊢ HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
      ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0)) :
        (B ⧸ Q)[X]) =
    if g • Q = Q then
      HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
        ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
    else X
have neg : ¬g • Q = Q →
  HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
      ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0) : (B ⧸ Q)[X]) =
    X
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.stabilizerHom Q P G :
                    MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                      (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                  (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                g :
              AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key :
  Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M))
    (∏ i : G, map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (i • b) : B[X])))
g : G
h : ¬g • Q = Q
⊢ HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
      ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0) : (B ⧸ Q)[X]) =
    X
have neg : HSub.hSub (α := (B ⧸ Q)[X]) X ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) 0) = X
Tactic: rw [map_zero, map_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.stabilizerHom Q P G :
                    MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                      (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                  (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                g :
              AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key :
  Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M))
    (∏ i : G, map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (i • b) : B[X])))
g : G
h : ¬g • Q = Q
neg : HSub.hSub (α := (B ⧸ Q)[X]) X ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) 0) = X
⊢ HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
      ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0) : (B ⧸ Q)[X]) =
    X
have neg₁ : HSub.hSub (α := (B ⧸ Q)[X]) X 0 = X
Tactic: rw [map_zero, map_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.stabilizerHom Q P G :
                    MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                      (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                  (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
                g :
              AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key :
  Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M))
    (∏ i : G, map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (i • b) : B[X])))
g : G
h : ¬g • Q = Q
neg : HSub.hSub (α := (B ⧸ Q)[X]) X ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) 0) = X
neg₁ : HSub.hSub (α := (B ⧸ Q)[X]) X 0 = X
⊢ HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
      ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0) : (B ⧸ Q)[X]) =
    X
have neg₂ : Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) X X
Tactic: rw [map_zero, map_zero, sub_zero]