-- Mathlib/RingTheory/Invariant.lean
theorem fixed_of_fixed1 [NoZeroSMulDivisors (B ⧸ Q) L] (f : L ≃ₐ[K] L) (b : B ⧸ Q)
    (hx : ∀ g : MulAction.stabilizer G Q, Ideal.Quotient.stabilizerHom Q P G g b = b) :
    f (algebraMap (B ⧸ Q) L b) = (algebraMap (B ⧸ Q) L b)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : NoZeroSMulDivisors (B ⧸ Q) L
f : L ≃ₐ[K] L
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
M : A[X]
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) = if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) (a * b₀)) else X
key :
  map (algebraMap K L) (map (algebraMap (A ⧸ P) K) (map (algebraMap A (A ⧸ P)) M)) =
    (X - C ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) (a * b₀)))) ^
        (Finset.filter (fun x => x • Q = Q) Finset.univ).card *
      X ^ (Finset.filter (fun x => ¬x • Q = Q) Finset.univ).card
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)

Tactic:
replace key := fixed_of_fixed1_aux3 key f (Finset.card_ne_zero_of_mem
  (Finset.mem_filter.mpr ⟨Finset.mem_univ 1, one_smul G Q⟩))

Result:
case intro.intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : NoZeroSMulDivisors (B ⧸ Q) L
f : L ≃ₐ[K] L
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
M : A[X]
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) = if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) (a * b₀)) else X
key :
  f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) (a * b₀))) =
    (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) (a * b₀))
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : NoZeroSMulDivisors (B ⧸ Q) L
f : L ≃ₐ[K] L
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
M : A[X]
key :
  map (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M) = ∏ i : G, map (algebraMap B (B ⧸ Q)) (X - C (i • b))
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) = if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) (a * b₀)) else X
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)

Tactic:
simp only [key₀, Finset.prod_ite, Finset.prod_const] at key

Result:
case intro.intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : NoZeroSMulDivisors (B ⧸ Q) L
f : L ≃ₐ[K] L
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
M : A[X]
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) = if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) (a * b₀)) else X
key :
  map (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M) =
    (X - C ((algebraMap B (B ⧸ Q)) (a * b₀))) ^ (Finset.filter (fun x => x • Q = Q) Finset.univ).card *
      X ^ (Finset.filter (fun x => ¬x • Q = Q) Finset.univ).card
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : NoZeroSMulDivisors (B ⧸ Q) L
f : L ≃ₐ[K] L
b : B ⧸ Q
hx : ∀ (g : ↥(MulAction.stabilizer G Q)), ((Ideal.Quotient.stabilizerHom Q P G) g) b = b
val✝ : Fintype G
⊢ f ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) b

Tactic:
obtain ⟨b₀, rfl⟩ := Ideal.Quotient.mk_surjective b

Result:
case intro.intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : NoZeroSMulDivisors (B ⧸ Q) L
f : L ≃ₐ[K] L
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
⊢ f ((algebraMap (B ⧸ Q) L) ((Ideal.Quotient.mk Q) b₀)) = (algebraMap (B ⧸ Q) L) ((Ideal.Quotient.mk Q) b₀)