-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
    (Submodule.span A
            (Set.range fun (x : A × A) ↦
              HAdd.hAdd (α := B →₀ B) (β := B →₀ B) (single ((algebraMap A B : (a : A) → B) x.1) 1 : B →₀ B)
                  (single ((algebraMap A B : (a : A) → B) x.2) 1 : B →₀ B) -
                single
                  (HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) x.1 : B)
                    ((algebraMap A B : (a : A) → B) x.2 : B))
                  1) ⊔
          Submodule.span A
            (Set.range fun (x : A × A) ↦
              HAdd.hAdd (α := B →₀ B) (β := B →₀ B)
                  (single ((algebraMap A B : (a : A) → B) x.2) ((algebraMap A B : (a : A) → B) x.1) : B →₀ B)
                  (single ((algebraMap A B : (a : A) → B) x.1) ((algebraMap A B : (a : A) → B) x.2) : B →₀ B) -
                single
                  (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x.1 : B)
                    ((algebraMap A B : (a : A) → B) x.2 : B))
                  1) ⊔
        Submodule.span A
          (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1) ⊔
      Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
    (Submodule.span A
          (Set.range fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ⊔
        Submodule.span A
          (Set.range fun (x : B × B) ↦
            HAdd.hAdd (α := B →₀ B) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ⊔
      Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
have simp_rw : Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
  (Submodule.span A
      (Set.range fun (x : A × A) ↦
        HAdd.hAdd (α := B →₀ B) (β := B →₀ B) (single ((algebraMap A B : (a : A) → B) x.1) 1 : B →₀ B)
            (single ((algebraMap A B : (a : A) → B) x.2) 1 : B →₀ B) -
          single
            (HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) x.1 : B)
              ((algebraMap A B : (a : A) → B) x.2 : B))
            1) ⊔
    (Submodule.span A
        (Set.range fun (x : A × A) ↦
          HAdd.hAdd (α := B →₀ B) (β := B →₀ B)
              (single ((algebraMap A B : (a : A) → B) x.2) ((algebraMap A B : (a : A) → B) x.1) : B →₀ B)
              (single ((algebraMap A B : (a : A) → B) x.1) ((algebraMap A B : (a : A) → B) x.2) : B →₀ B) -
            single
              (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x.1 : B)
                ((algebraMap A B : (a : A) → B) x.2 : B))
              1) ⊔
      (Submodule.span A
          (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1) ⊔
        Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))))
  (Submodule.span A
      (Set.range.{u_3, u_2 + 1} (ι := A × A)
        ((fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ∘
          Prod.map (⇑(algebraMap A B) : (a : A) → B) (⇑(algebraMap A B) : (a : A) → B))) ⊔
    (Submodule.span A
        (Set.range.{u_3, u_2 + 1} (ι := A × A)
          ((fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ∘
            Prod.map (⇑(algebraMap A B) : (a : A) → B) (⇑(algebraMap A B) : (a : A) → B))) ⊔
      Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1)))
Tactic: simp_rw [sup_assoc, ← (h.prodMap h).range_comp]