-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_4
inst : CommRing A
B : Type u_6
inst_1 : CommRing B
inst_2 : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Algebra A K₁
inst_6 : Algebra A K₂
inst_7 : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst_8 : Field L₁
inst_9 : Field L₂
inst_10 : Algebra B L₁
inst_11 : Algebra B L₂
inst_12 : Algebra K₁ L₁
inst_13 : Algebra K₂ L₂
inst_14 : Algebra A L₁
inst_15 : Algebra A L₂
inst_16 : IsScalarTower A K₁ L₁
inst_17 : IsScalarTower A K₂ L₂
inst_18 : IsScalarTower A B L₁
inst_19 : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : Membership.mem (γ := Submonoid A) A⁰ s
simp_rw :
  HDiv.hDiv (α := L₂) (β := L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : K₂) : L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : K₂) : L₂) =
    HDiv.hDiv (α := L₂) (β := L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : L₁) : L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : L₁) : L₂)
simp_rw₁ :
  HDiv.hDiv (α := L₂) (β := L₂) ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((algebraMap A K₂ : (a : A) → K₂) r : K₂) : L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((algebraMap A K₂ : (a : A) → K₂) s : K₂) : L₂) =
    HDiv.hDiv (α := L₂) (β := L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : L₁) : L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : L₁) : L₂)
simp_rw₂ :
  HDiv.hDiv (α := L₂) (β := L₂) ((algebraMap A L₂ : (a : A) → L₂) r : L₂) ((algebraMap A L₂ : (a : A) → L₂) s : L₂) =
    HDiv.hDiv (α := L₂) (β := L₂) ((f : (a : L₁) → L₂) ((algebraMap A L₁ : (a : A) → L₁) r : L₁) : L₂)
      ((f : (a : L₁) → L₂) ((algebraMap A L₁ : (a : A) → L₁) s : L₁) : L₂)
simp_rw₃ :
  HDiv.hDiv (α := L₂) (β := L₂) ((algebraMap A L₂ : (a : A) → L₂) r : L₂) ((algebraMap A L₂ : (a : A) → L₂) s : L₂) =
    HDiv.hDiv (α := L₂) (β := L₂)
      ((f : (a : L₁) → L₂) ((algebraMap B L₁ : (a : B) → L₁) ((algebraMap A B : (a : A) → B) r : B) : L₁) : L₂)
      ((f : (a : L₁) → L₂) ((algebraMap B L₁ : (a : B) → L₁) ((algebraMap A B : (a : A) → B) s : B) : L₁) : L₂)
⊢ Eq.{u_11 + 1} (α := L₂)
    ((algebraMap K₂ L₂ : (a : K₂) → L₂)
        ((e : (a : K₁) → K₂)
            (HDiv.hDiv (α := K₁) (β := K₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁)
              ((algebraMap A K₁ : (a : A) → K₁) s : K₁)) :
          K₂) :
      L₂)
    ((f : (a : L₁) → L₂)
        ((algebraMap K₁ L₁ : (a : K₁) → L₁)
            (HDiv.hDiv (α := K₁) (β := K₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁)
              ((algebraMap A K₁ : (a : A) → K₁) s : K₁)) :
          L₁) :
      L₂)
have simp_rw₄ : HDiv.hDiv (α := L₂) (β := L₂) ((algebraMap A L₂ : (a : A) → L₂) r : L₂) ((algebraMap A L₂ : (a : A) → L₂) s : L₂) =
  HDiv.hDiv (α := L₂) (β := L₂) ((algebraMap B L₂ : (a : B) → L₂) ((algebraMap A B : (a : A) → B) r : B) : L₂)
    ((algebraMap B L₂ : (a : B) → L₂) ((algebraMap A B : (a : A) → B) s : B) : L₂)
Tactic: simp_rw [map_div₀, AlgHom.commutes, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply A B L₁, AlgHom.commutes, ← IsScalarTower.algebraMap_apply]