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))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
simp :
  Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (∑ x ∈ f.support,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S)) :
      I →₀ R)
    (0 : I →₀ R)
⊢ 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)

Tactic:
simp only [Finsupp.sum]

Premises used: Finsupp.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))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
trans :
  Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (∑ x ∈ f.support,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S)) :
      I →₀ R)
    ((b.repr : (a : S) → I →₀ R) (∑ x ∈ f.support, 0) : I →₀ R)
trans₁ : Eq (α := I →₀ R) ((b.repr : (a : S) → I →₀ R) (∑ x ∈ f.support, 0) : I →₀ R) (0 : I →₀ R)
⊢ Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (∑ x ∈ f.support,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S)) :
      I →₀ R)
    (0 : I →₀ R)

Tactic:
trans b.repr (f.support.sum (fun _ ↦ 0))

Premises used: Finsupp.support, Module.Basis.repr, OfNat.ofNat, DFunLike.coe, 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))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
⊢ Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (∑ x ∈ f.support,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S)) :
      I →₀ R)
    ((b.repr : (a : S) → I →₀ R) (∑ x ∈ f.support, 0) : I →₀ R)

Tactic:
congr_arg b.repr (Finset.sum_congr rfl ?_)

Premises used: Module.Basis.repr, congr_arg, DFunLike.coe, Finset.sum_congr, 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))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
refine :
  ∀ x ∈ f.support,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S) = 0
⊢ Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (∑ x ∈ f.support,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S)) :
      I →₀ R)
    ((b.repr : (a : S) → I →₀ R) (∑ x ∈ f.support, 0) : I →₀ R)

Tactic:
refine congr_arg b.repr (Finset.sum_congr rfl ?_)

Premises used: Module.Basis.repr, congr_arg, DFunLike.coe, Finset.sum_congr, 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))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
simp :
  ∀ (x : I),
    Ne (α := S) ((f : (a : I) → S) x : S) (0 : S) →
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S) = 0
⊢ ∀ x ∈ f.support,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S) = 0

Tactic:
simp only [Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff
-- 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))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
i : I
hi : Ne (α := S) ((f : (a : I) → S) i : S) (0 : S)
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 ((f : (a : I) → S) i : S) = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := S) 0 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a i : (a : I) → R) j : R) ((f : (a : I) → S) i : S) = 0

Tactic:
rw [hj i hi, zero_smul]

Premises used: zero_smul
-- 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))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
⊢ Eq (α := I →₀ R) ((b.repr : (a : S) → I →₀ R) (∑ x ∈ f.support, 0) : I →₀ R) (0 : I →₀ R)

Tactic:
simp only [Finset.sum_const_zero, map_zero]

Premises used: map_zero, Finset.sum_const_zero
-- 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))) ⋯
⊢ ∀ 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)

Tactic:
have hG : ∀ j ∉ (Finset.biUnion f.support fun i ↦ (a i).support),
      b.repr (f.sum (fun i y ↦ a i j • y)) = 0 := by
    intro j hj
    simp only [Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_exists, not_and,
      not_not] at hj
    simp only [Finsupp.sum]
    trans b.repr (f.support.sum (fun _ ↦ 0))
    · refine congr_arg b.repr (Finset.sum_congr rfl ?_)
      simp only [Finsupp.mem_support_iff]
      intro i hi
      rw [hj i hi, zero_smul]
    · simp only [Finset.sum_const_zero, map_zero]
-- 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))
    ⋯
a₁ :
  Eq (α := Finsupp.{u_2, u_1} (I × I) R)
    ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F : Finsupp.{u_2, u_1} (I × I) R)
    ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G : Finsupp.{u_2, u_1} (I × I) R)
⊢ F = G

Tactic:
apply Finsupp.curryEquiv.symm.injective

Premises used: Finsupp.curryEquiv, Equiv.injective, Equiv.symm
-- 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))
    ⋯
a₁ :
  Eq (α := Finsupp.{u_2, u_1} (I × I) R)
    ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
        ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F) :
      Finsupp.{u_2, u_1} (I × I) R)
    ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
        ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G) :
      Finsupp.{u_2, u_1} (I × I) R)
⊢ Eq (α := Finsupp.{u_2, u_1} (I × I) R)
    ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F : Finsupp.{u_2, u_1} (I × I) R)
    ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G : Finsupp.{u_2, u_1} (I × I) R)

Tactic:
apply (Finsupp.equivCongrLeft (Equiv.prodComm I I)).injective

Premises used: Equiv.prodComm, Equiv.injective, Finsupp.equivCongrLeft
-- 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))
    ⋯
a₁ :
  Eq.{u_2 + 1} (α := S ⊗[R] S)
    (((LinearEquiv.symm (Basis.repr (b.tensorProduct b)) : Finsupp.{u_2, u_1} (I × I) R ≃ₗ[R] S ⊗[R] S) :
          (a : I × I →₀ R) → S ⊗[R] S)
        ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
          ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F)) :
      S ⊗[R] S)
    (((LinearEquiv.symm (Basis.repr (b.tensorProduct b)) : Finsupp.{u_2, u_1} (I × I) R ≃ₗ[R] S ⊗[R] S) :
          (a : I × I →₀ R) → S ⊗[R] S)
        ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
          ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G)) :
      S ⊗[R] S)
⊢ Eq (α := Finsupp.{u_2, u_1} (I × I) R)
    ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
        ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F) :
      Finsupp.{u_2, u_1} (I × I) R)
    ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
        ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G) :
      Finsupp.{u_2, u_1} (I × I) R)

Tactic:
apply (b.tensorProduct b).repr.symm.injective

Premises used: LinearEquiv.symm, Module.Basis.repr, Module.Basis.tensorProduct, LinearEquiv.injective
-- 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 :
  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))
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (((LinearEquiv.symm (Basis.repr (b.tensorProduct b)) : Finsupp.{u_2, u_1} (I × I) R ≃ₗ[R] S ⊗[R] S) :
          (a : I × I →₀ R) → S ⊗[R] S)
        ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
          ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F)) :
      S ⊗[R] S)
    (((LinearEquiv.symm (Basis.repr (b.tensorProduct b)) : Finsupp.{u_2, u_1} (I × I) R ≃ₗ[R] S ⊗[R] S) :
          (a : I × I →₀ R) → S ⊗[R] S)
        ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
          ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G)) :
      S ⊗[R] S)

Tactic:
simpa [Finsupp.linearCombination_apply, Finsupp.sum_uncurry_index]

Premises used: Finsupp.linearCombination_apply, Finsupp.sum_uncurry_index
-- 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))
    ⋯
a₁ :
  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))
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (((LinearEquiv.symm (Basis.repr (b.tensorProduct b)) : Finsupp.{u_2, u_1} (I × I) R ≃ₗ[R] S ⊗[R] S) :
          (a : I × I →₀ R) → S ⊗[R] S)
        ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
          ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F)) :
      S ⊗[R] S)
    (((LinearEquiv.symm (Basis.repr (b.tensorProduct b)) : Finsupp.{u_2, u_1} (I × I) R ≃ₗ[R] S ⊗[R] S) :
          (a : I × I →₀ R) → S ⊗[R] S)
        ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
          ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G)) :
      S ⊗[R] S)

Tactic:
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]
-- 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
simp_rw :
  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)
⊢ 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:
simp_rw [Finsupp.sum, TensorProduct.smul_tmul', ← TensorProduct.sum_tmul]

Premises used: Finsupp.sum, TensorProduct.sum_tmul, TensorProduct.smul_tmul'