Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A
            (Set.range fun x ↦
              (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.1 1) +
                  (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.2 1) -
                (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
                  (single (x.1 + x.2) 1)) ⊔
          Submodule.span A
            (Set.range fun x ↦
              (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.2 x.1) +
                  (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (single x.1 x.2) -
                (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
                  (single (x.1 * x.2) 1)) ⊔
        Submodule.span A
          (Set.range fun x ↦
            (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
              (single ((algebraMap R A) x) 1)) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1) =
    Submodule.span A (Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ⊔
        Submodule.span A (Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap 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]

Goal state after:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A
            (Set.range fun x ↦
              single ((algebraMap A B) x.1) 1 + single ((algebraMap A B) x.2) 1 -
                single ((algebraMap A B) x.1 + (algebraMap A B) x.2) 1) ⊔
          Submodule.span A
            (Set.range fun x ↦
              single ((algebraMap A B) x.2) ((algebraMap A B) x.1) +
                  single ((algebraMap A B) x.1) ((algebraMap A B) x.2) -
                single ((algebraMap A B) x.1 * (algebraMap A B) x.2) 1) ⊔
        Submodule.span A (Set.range fun x ↦ single ((algebraMap A B) ((algebraMap R A) x)) 1) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1) =
    Submodule.span A (Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ⊔
        Submodule.span A (Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1)