-- 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_rw :
  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))
⊢ Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
    (Submodule.span A
        (Set.image.{u_2, u_3} (α := A →₀ A)
          (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
            (a : A →₀ A) → B →₀ B)
          (((Set.range fun (x : A × A) ↦ HAdd.hAdd (α := A →₀ A) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ∪
              Set.range fun (x : A × A) ↦
                HAdd.hAdd (α := A →₀ A) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ∪
            Set.range fun (x : R) ↦ 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) ∪
          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) ∪
        Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))

Tactic:
simp_rw [Set.image_union, Submodule.span_union, ← Set.image_univ, Set.image_image, Set.image_univ,
    map_sub, map_add]

Premises used: Set.image_image, Set.image_univ, map_sub, map_add, Submodule.span_union, Set.image_union