-- 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 : IsFractionRing.{u_1, u_4} (A ⧸ P) K
inst_19 : IsFractionRing.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
this_1 : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((((IsFractionRing.stabilizerHom G P Q K L : MonoidHom.{u_3, u_5} ↥(MulAction.stabilizer G Q) Gal(L/K)) :
                (a : ↥(MulAction.stabilizer G Q)) → Gal(L/K))
              g :
            Gal(L/K)) :
          (a : L) → L)
        (HDiv.hDiv (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) x : L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L)) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) x : L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L)
b : B ⧸ Q
a : A ⧸ P
h : HMul.hMul (β := B ⧸ Q) x ((algebraMap (A ⧸ P) (B ⧸ Q) : (a : A ⧸ P) → B ⧸ Q) a : B ⧸ Q) = b * y
ha : Ne.{u_5 + 1} (α := L) ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) (0 : L)
hy : Ne.{u_5 + 1} (α := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L) (0 : L)
rw :
  HMul.hMul (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) x : L)
      ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) =
    HMul.hMul (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L)
rw₁ :
  HMul.hMul (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) x : L)
      ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) =
    (algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (b * y)
rw₂ :
  HMul.hMul (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) x : L)
      ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) =
    (algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
      (HMul.hMul (β := B ⧸ Q) x ((algebraMap (A ⧸ P) (B ⧸ Q) : (a : A ⧸ P) → B ⧸ Q) a : B ⧸ Q))
rw₃ :
  HMul.hMul (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) x : L)
      ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) =
    HMul.hMul (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) x : L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap (A ⧸ P) (B ⧸ Q) : (a : A ⧸ P) → B ⧸ Q) a : B ⧸ Q) : L)
⊢ HDiv.hDiv (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) x : L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L)
      ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L)
have rw₄ : HMul.hMul (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) x : L)
    ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) =
  HMul.hMul (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) x : L)
    ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L)
Tactic: rw [div_eq_div_iff hy ha, ← map_mul, ← h, map_mul, ← algebraMap_apply]