awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
i : I
e_m :
  ∑
      a ∈
        Finsupp.support.{u_2, u_1} (M := R)
          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
        ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S)) : I →₀ R) : (a : I) → R) a : R)
        ((b : (a : I) → S) a : S) =
    HMul.hMul (β := S) x ((f : (a : I) → S) i : S)
⊢ Eq (α := S ⊗[R] S)
    ((∑
          a ∈
            Finsupp.support.{u_2, u_1} (M := R)
              ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))),
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S)) : I →₀ R) : (a : I) → R) a :
              R)
            ((b : (a : I) → S) a : S)) ⊗ₜ[R]
        (b : (a : I) → S) i :
      S ⊗[R] S)
    (HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)

Tactic:
congr 1
-- 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
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
i : I
⊢ ∑
      a ∈
        Finsupp.support.{u_2, u_1} (M := R)
          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
        ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S)) : I →₀ R) : (a : I) → R) a : R)
        ((b : (a : I) → S) a : S) =
    HMul.hMul (β := S) x ((f : (a : I) → S) i : S)

Tactic:
b.linearCombination_repr _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Module.Basis.linearCombination_repr, Finset.sum
-- 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
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
i : I
⊢ ∑
      a ∈
        Finsupp.support.{u_2, u_1} (M := R)
          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
        ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S)) : I →₀ R) : (a : I) → R) a : R)
        ((b : (a : I) → S) a : S) =
    HMul.hMul (β := S) x ((f : (a : I) → S) i : S)

Tactic:
exact b.linearCombination_repr _

Premises used: Module.Basis.linearCombination_repr
-- 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
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
⊢ ∀ (i : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))) fun (j : I) (k : R) ↦
          HSMul.hSMul (β := S ⊗[R] S) k ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) :
        S ⊗[R] S)
      (HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)

Tactic:
have : ∀ i, ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i := by
      intro i
      simp_rw [Finsupp.sum, TensorProduct.smul_tmul', ← TensorProduct.sum_tmul]
      congr 1
      exact b.linearCombination_repr _
-- 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
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
this :
  ∀ (i : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))) fun (j : I) (k : R) ↦
          HSMul.hSMul (β := S ⊗[R] S) k ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) :
        S ⊗[R] S)
      (HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)
a₁ :
  Eq (α := S ⊗[R] S)
    (∑ a ∈ f.support,
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) a : S))) fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a : S ⊗[R] S))
    (∑ a_1 ∈ f.support.biUnion fun (i : I) ↦ (a i).support,
      Finsupp.sum (M := R)
        ((b.repr : (a : S) → I →₀ R)
            (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) a_1 : R) y) :
          I →₀ R)
        fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a_1 : S ⊗[R] S))
a₂ a₃ :
  ∀ (a : I),
    Eq.{u_2 + 1} (α := S ⊗[R] S)
      (Finsupp.sum 0 fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a : S ⊗[R] S))
      0
⊢ Eq (α := S ⊗[R] S)
    (F.sum fun (a : I) (f : I →₀ R) ↦
      f.sum fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a : S ⊗[R] S))
    (G.sum fun (a : I) (f : I →₀ R) ↦
      f.sum fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a : S ⊗[R] S))

Tactic:
rw [Finsupp.onFinset_sum, Finsupp.onFinset_sum]

Premises used: Finsupp.onFinset_sum
-- 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
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
this :
  ∀ (i : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))) fun (j : I) (k : R) ↦
          HSMul.hSMul (β := S ⊗[R] S) k ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) :
        S ⊗[R] S)
      (HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)
trans :
  (∑ a ∈ f.support,
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) a : S))) fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a : S ⊗[R] S)) =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (elem R S)
trans₁ :
  HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (elem R S) =
    ∑ a_1 ∈ f.support.biUnion fun (i : I) ↦ (a i).support,
      Finsupp.sum (M := R)
        ((b.repr : (a : S) → I →₀ R)
            (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) a_1 : R) y) :
          I →₀ R)
        fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a_1 : S ⊗[R] S)
⊢ Eq (α := S ⊗[R] S)
    (∑ a ∈ f.support,
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) a : S))) fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a : S ⊗[R] S))
    (∑ a_1 ∈ f.support.biUnion fun (i : I) ↦ (a i).support,
      Finsupp.sum (M := R)
        ((b.repr : (a : S) → I →₀ R)
            (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) a_1 : R) y) :
          I →₀ R)
        fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a_1 : S ⊗[R] S))

Tactic:
trans (x ⊗ₜ 1) * elem R S

Premises used: Algebra.FormallyUnramified.elem, TensorProduct.tmul, OfNat.ofNat
-- 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
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
this :
  ∀ (i : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))) fun (j : I) (k : R) ↦
          HSMul.hSMul (β := S ⊗[R] S) k ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) :
        S ⊗[R] S)
      (HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)
simp_rw :
  ∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1 =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (elem R S)
simp_rw₁ :
  ∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1 =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
simp_rw₂ :
  ∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1 =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (∑ x ∈ f.support, (f : (a : I) → S) x ⊗ₜ[R] (b : (a : I) → S) x)
simp_rw₃ :
  Eq (α := S ⊗[R] S) (∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1)
    (∑ i ∈ f.support,
      HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (x ⊗ₜ[R] 1) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
simp_rw₄ :
  Eq (α := S ⊗[R] S) (∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1)
    (∑ i ∈ f.support,
      HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R]
        HMul.hMul (α := S) (β := S) (1 : S) ((b : (a : I) → S) i : S))
⊢ (∑ a ∈ f.support,
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) a : S))) fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a : S ⊗[R] S)) =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (elem R S)

Tactic:
simp_rw [this, hf, Finsupp.sum, Finset.mul_sum, TensorProduct.tmul_mul_tmul, one_mul]

Premises used: Finset.mul_sum, Finsupp.sum, Algebra.TensorProduct.tmul_mul_tmul, one_mul
-- 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
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
this :
  ∀ (i : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))) fun (j : I) (k : R) ↦
          HSMul.hSMul (β := S ⊗[R] S) k ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) :
        S ⊗[R] S)
      (HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)
ha : a = fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
⊢ HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (elem R S) =
    ∑ a_1 ∈ f.support.biUnion fun (i : I) ↦ (a i).support,
      Finsupp.sum (M := R)
        ((b.repr : (a : S) → I →₀ R)
            (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) a_1 : R) y) :
          I →₀ R)
        fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a_1 : S ⊗[R] S)

Tactic:
rw [← one_tmul_mul_elem, hf, finite_of_free_aux]

Premises used: Algebra.FormallyUnramified.one_tmul_mul_elem, Algebra.FormallyUnramified.finite_of_free_aux
-- 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
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
this :
  ∀ (i : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))) fun (j : I) (k : R) ↦
          HSMul.hSMul (β := S ⊗[R] S) k ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) :
        S ⊗[R] S)
      (HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)
⊢ a = fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)

Tactic:
rfl
-- 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
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
this :
  ∀ (i : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))) fun (j : I) (k : R) ↦
          HSMul.hSMul (β := S ⊗[R] S) k ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) :
        S ⊗[R] S)
      (HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)
a_1 : I
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (Finsupp.sum 0 fun (b' : I) (c : R) ↦
      HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a_1 : S ⊗[R] S))
    0

Tactic:
simp
-- 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
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
⊢ F = G

Tactic:
have : F = G := by
    apply Finsupp.curryEquiv.symm.injective
    apply (Finsupp.equivCongrLeft (Equiv.prodComm I I)).injective
    apply (b.tensorProduct b).repr.symm.injective
    suffices (F.sum fun a f ↦ f.sum fun b' c ↦ c • b b' ⊗ₜ[R] b a) =
        G.sum fun a f ↦ f.sum fun b' c ↦ c • b b' ⊗ₜ[R] b a by
      simpa [Finsupp.linearCombination_apply, Finsupp.sum_uncurry_index]
    have : ∀ i, ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i := by
      intro i
      simp_rw [Finsupp.sum, TensorProduct.smul_tmul', ← TensorProduct.sum_tmul]
      congr 1
      exact b.linearCombination_repr _
    rw [Finsupp.onFinset_sum, Finsupp.onFinset_sum]
    · trans (x ⊗ₜ 1) * elem R S
      · simp_rw [this, hf, Finsupp.sum, Finset.mul_sum, TensorProduct.tmul_mul_tmul, one_mul]
      · rw [← one_tmul_mul_elem, hf, finite_of_free_aux]
        rfl
    · intro; simp
    · intro; simp