-- 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
hg :
  ∀ (x_1 x_2 : I),
    ¬Eq.{u_2 + 1} (α := S) ((f : (a : I) → S) x_2 : S) (0 : S) →
      ¬Eq.{u_1 + 1} (α := R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) x_2 : S) x) : I →₀ R) : (a : I) → R)
                x_1 :
              R)
            (0 : R) →
        Eq.{u_1 + 1} (α := R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R)
                x_1 :
              R)
            (0 : R) →
          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)
⊢ ∀
    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)

Tactic:
simp only [a, Finset.mem_sdiff, Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_not,
      and_imp, forall_exists_index]

Premises used: Finsupp.mem_support_iff, Classical.not_not, and_imp, forall_exists_index, ne_eq, Finset.mem_sdiff, Finset.mem_biUnion