-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            ((b.repr : (a : S) → I →₀ R) y : I →₀ R))
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
      (f.sum fun (i : I) (y : S) ↦
        Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
          HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
i : I
hi : i ∈ f.support
h :
  (a i).support ⊆
    f.support.biUnion fun (i : I) ↦
      Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x))
hg :
  ∀
    x_1 ∈
      (f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x))) \
        (a i).support,
    Eq (α := S ⊗[R] S)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R)
                x_1 :
              R)
            ((f : (a : I) → S) i : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1 :
        S ⊗[R] S)
      (0 : S ⊗[R] S)
hfg :
  ∀ x_1 ∈ (a i).support,
    Eq (α := S ⊗[R] S)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a i : (a : I) → R) x_1 : R) ((f : (a : I) → S) i : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1 :
        S ⊗[R] S)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R)
                x_1 :
              R)
            ((f : (a : I) → S) i : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1 :
        S ⊗[R] S)
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ x ∈ (a i).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a i : (a : I) → R) x : R) ((f : (a : I) → S) i : S) ⊗ₜ[R]
        (b : (a : I) → S) x)
    (∑
      x_1 ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
          ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) x_1 :
            R)
          ((f : (a : I) → S) i : S) ⊗ₜ[R]
        (b : (a : I) → S) x_1)

Tactic:
apply Finset.sum_subset_zero_on_sdiff

Premises used: Finset.sum_subset_zero_on_sdiff