-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
simp :
  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))
⊢ Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
    (Submodule.span A
            (Set.range fun (x : A × A) ↦
              HSub.hSub (β := B →₀ B)
                (HAdd.hAdd (α := B →₀ B) (β := B →₀ B)
                  (((mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B) :
                          LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) (A →₀ A) (B →₀ B)) :
                        (a : A →₀ A) → B →₀ B)
                      (single x.1 1) :
                    B →₀ B)
                  (((mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B) :
                          LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) (A →₀ A) (B →₀ B)) :
                        (a : A →₀ A) → B →₀ B)
                      (single x.2 1) :
                    B →₀ B))
                (((mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B) :
                        LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) (A →₀ A) (B →₀ B)) :
                      (a : A →₀ A) → B →₀ B)
                    (single (x.1 + x.2) 1) :
                  B →₀ B)) ⊔
          Submodule.span A
            (Set.range fun (x : A × A) ↦
              HSub.hSub (β := B →₀ B)
                (HAdd.hAdd (α := B →₀ B) (β := B →₀ B)
                  (((mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B) :
                          LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) (A →₀ A) (B →₀ B)) :
                        (a : A →₀ A) → B →₀ B)
                      (single x.2 x.1) :
                    B →₀ B)
                  (((mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B) :
                          LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) (A →₀ A) (B →₀ B)) :
                        (a : A →₀ A) → B →₀ B)
                      (single x.1 x.2) :
                    B →₀ B))
                (((mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B) :
                        LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) (A →₀ A) (B →₀ B)) :
                      (a : A →₀ A) → B →₀ B)
                    (single (x.1 * x.2) 1) :
                  B →₀ B)) ⊔
        Submodule.span A
          (Set.range fun (x : R) ↦
            ((mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B) :
                  LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) (A →₀ A) (B →₀ B)) :
                (a : A →₀ A) → B →₀ B)
              (single ((algebraMap R A : (a : R) → A) x) 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))

Tactic:
simp only [LinearMap.comp_apply, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single,
    Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply,
    map_one, map_add, map_mul]

Premises used: LinearMap.comp_apply, Algebra.linearMap_apply, map_add, Finsupp.mapDomain_single, Finsupp.mapRange.linearMap_apply, map_mul, map_one, Finsupp.mapRange_single, Finsupp.lmapDomain_apply