-- Mathlib/RingTheory/Invariant.lean
theorem fixed_of_fixed2 (f : L ≃ₐ[K] L) (x : L)
    (hx : ∀ g : MulAction.stabilizer G Q, IsFractionRing.stabilizerHom G P Q K L g x = x) :
    f x = x

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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : L ≃ₐ[K] L
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y b : B ⧸ Q
a : A ⧸ P
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
h : (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y = (algebraMap (B ⧸ Q) L) b / (algebraMap (A ⧸ P) L) a
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) b) /
        (algebraMap K L) ((algebraMap (A ⧸ P) K) a) =
      (algebraMap (B ⧸ Q) L) b / (algebraMap K L) ((algebraMap (A ⧸ P) K) a)
⊢ f ((algebraMap (B ⧸ Q) L) b) / (algebraMap K L) ((algebraMap (A ⧸ P) K) a) =
    (algebraMap (B ⧸ Q) L) b / (algebraMap K L) ((algebraMap (A ⧸ P) K) a)

Tactic:
simp only [← algebraMap_apply, div_left_inj' ha] at hx ⊢

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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : L ≃ₐ[K] L
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y b : B ⧸ Q
a : A ⧸ P
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
h : (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y = (algebraMap (B ⧸ Q) L) b / (algebraMap (A ⧸ P) L) a
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) 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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : L ≃ₐ[K] L
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
h : a • x = y * b
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
⊢ f ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) = (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y

Tactic:
replace h : algebraMap (B ⧸ Q) L x / algebraMap (B ⧸ Q) L y =
    algebraMap (B ⧸ Q) L b / algebraMap (A ⧸ P) L a := by
  rw [mul_comm, Algebra.smul_def, mul_comm] at h
  rw [div_eq_div_iff hy ha, ← map_mul, ← h, map_mul, ← algebraMap_apply]

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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : L ≃ₐ[K] L
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
h : (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y = (algebraMap (B ⧸ Q) L) b / (algebraMap (A ⧸ P) L) a
⊢ f ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) = (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y

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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : L ≃ₐ[K] L
x : L
hx : ∀ (g : ↥(MulAction.stabilizer G Q)), ((IsFractionRing.stabilizerHom G P Q K L) g) x = x
val✝ : Fintype G
⊢ f x = x

Tactic:
have : P.IsPrime := Ideal.over_def Q P ▸ Ideal.IsPrime.under A Q

Result:
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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : L ≃ₐ[K] L
x : L
hx : ∀ (g : ↥(MulAction.stabilizer G Q)), ((IsFractionRing.stabilizerHom G P Q K L) g) x = x
val✝ : Fintype G
this : P.IsPrime
⊢ f x = x