-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
a : A
ha : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
b : A
hb :
  HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) =
    HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) b : B) y
hxy :
  HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) b : B) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
h₁ :
  (algebraMap K L : (a : K) → L)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) ((algebraMap A K : (a : A) → K) a : K)) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) b : B) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
h₂ :
  HDiv.hDiv (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) b : K) : L)
      ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) b : B) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
⊢ (algebraMap K L : (a : K) → L)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) ((algebraMap A K : (a : A) → K) a : K)) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
have h₃ : HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) b : B) : L)
    ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L) =
  HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) b : B) : L)
    ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
Tactic: rw [hxy, map_div₀, hc, hc]