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
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R
ha : a = fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
rw :
  Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ i ∈ f.support,
      HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (1 ⊗ₜ[R] x) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (∑ k ∈ 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) k : R) y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
⊢ HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] x) (f.sum fun (i : I) (y : S) ↦ y ⊗ₜ[R] (b : (a : I) → S) i) =
    ∑ k ∈ 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) k : R) y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)

Tactic:
rw [Finsupp.sum, Finset.mul_sum]

Premises used: Finset.mul_sum, 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
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R
ha : a = fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
subst :
  Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ i ∈ f.support,
      HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (1 ⊗ₜ[R] x) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (∑
      k ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
      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)
                (((fun (i : I) ↦
                          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                        i :
                      (a : I) → R)
                    k :
                  R)
                y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ i ∈ f.support,
      HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (1 ⊗ₜ[R] x) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (∑ k ∈ 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) k : R) y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))

Tactic:
subst ha
-- 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)
simp :
  ∑ i ∈ f.support, (f : (a : I) → S) i ⊗ₜ[R] (Finsupp.linearCombination R (⇑b : (a : I) → S) : (a : I →₀ R) → S) (a i)
| ∑ i ∈ f.support,
    HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (1 ⊗ₜ[R] x) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)

Tactic:
simp only [TensorProduct.tmul_mul_tmul, one_mul, mul_comm x (b _),
      ← show ∀ i, Finsupp.linearCombination _ b (a i) = b i * x from
          fun _ ↦ b.linearCombination_repr _]

Premises used: HMul.hMul, Algebra.TensorProduct.tmul_mul_tmul, Module.Basis.linearCombination_repr, mul_comm, DFunLike.coe, 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
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)
conv_lhs :
  Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ i ∈ f.support,
      (f : (a : I) → S) i ⊗ₜ[R] (Finsupp.linearCombination R (⇑b : (a : I) → S) : (a : I →₀ R) → S) (a i))
    (∑
      k ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
      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)
                (((fun (i : I) ↦
                          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                        i :
                      (a : I) → R)
                    k :
                  R)
                y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ i ∈ f.support,
      HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (1 ⊗ₜ[R] x) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (∑
      k ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
      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)
                (((fun (i : I) ↦
                          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                        i :
                      (a : I) → R)
                    k :
                  R)
                y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))

Tactic:
conv_lhs =>
    simp only [TensorProduct.tmul_mul_tmul, one_mul, mul_comm x (b _),
      ← show ∀ i, Finsupp.linearCombination _ b (a i) = b i * x from
          fun _ ↦ b.linearCombination_repr _]

Premises used: HMul.hMul, Algebra.TensorProduct.tmul_mul_tmul, Module.Basis.linearCombination_repr, mul_comm, DFunLike.coe, 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
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)
simp :
  ∑ x ∈ f.support,
    ∑ x_1 ∈ (a x).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) x_1 : R) ((f : (a : I) → S) x : S) ⊗ₜ[R]
        (b : (a : I) → S) x_1
| ∑ i ∈ f.support, (f : (a : I) → S) i ⊗ₜ[R] (Finsupp.linearCombination R (⇑b : (a : I) → S) : (a : I →₀ R) → S) (a i)

Tactic:
simp only [Finsupp.linearCombination, Finsupp.coe_lsum,
    LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, Finsupp.sum, TensorProduct.tmul_sum,
    ← TensorProduct.smul_tmul]

Premises used: TensorProduct.smul_tmul, LinearMap.id_coe, Finsupp.sum, TensorProduct.tmul_sum, Finsupp.coe_lsum, LinearMap.coe_smulRight, Finsupp.linearCombination, id_eq
-- 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)
conv_lhs :
  Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ x ∈ f.support,
      ∑ x_1 ∈ (a x).support,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) x_1 : R) ((f : (a : I) → S) x : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1)
    (∑
      k ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
      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)
                (((fun (i : I) ↦
                          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                        i :
                      (a : I) → R)
                    k :
                  R)
                y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ i ∈ f.support,
      (f : (a : I) → S) i ⊗ₜ[R] (Finsupp.linearCombination R (⇑b : (a : I) → S) : (a : I →₀ R) → S) (a i))
    (∑
      k ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
      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)
                (((fun (i : I) ↦
                          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                        i :
                      (a : I) → R)
                    k :
                  R)
                y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))

Tactic:
conv_lhs => simp only [Finsupp.linearCombination, Finsupp.coe_lsum,
    LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, Finsupp.sum, TensorProduct.tmul_sum,
    ← TensorProduct.smul_tmul]

Premises used: TensorProduct.smul_tmul, LinearMap.id_coe, Finsupp.sum, TensorProduct.tmul_sum, Finsupp.coe_lsum, LinearMap.coe_smulRight, Finsupp.linearCombination, id_eq
-- 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)
i : I
rw :
  Eq (α := S ⊗[R] S)
    (f.sum fun (a_1 : I) (b_1 : S) ↦
      (HSMul.hSMul (α := R) (β := I →₀ R) ((a a_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) b_1 : I →₀ R)).sum
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (f.sum fun (i_1 : 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) ((a i_1 : (a : I) → R) i : R)
          (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
h_zero :
  ∀ (a : I),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S ⊗[R] S) 0 ((b : (a : I) → S) a ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) =
      0
h_add :
  ∀ (a : I) (b₁ b₂ : R),
    HSMul.hSMul (β := S ⊗[R] S) (b₁ + b₂) ((b : (a : I) → S) a ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) =
      HSMul.hSMul (β := S ⊗[R] S) b₁ ((b : (a : I) → S) a ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) +
        HSMul.hSMul (β := S ⊗[R] S) b₂ ((b : (a : I) → S) a ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)
⊢ Eq (α := S ⊗[R] S)
    (Finsupp.sum
      (f.sum fun (i_1 : I) (y : S) ↦
        HSMul.hSMul (α := R) (β := I →₀ R) ((a i_1 : (a : I) → R) i : 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) i : S ⊗[R] S))
    (f.sum fun (i_1 : 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) ((a i_1 : (a : I) → R) i : R)
          (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))

Tactic:
rw [Finsupp.sum_sum_index]

Premises used: Finsupp.sum_sum_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
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)
i : I
e_g :
  Eq (α := I → S → S ⊗[R] S)
    (fun (a_1 : I) (b_1 : S) ↦
      (HSMul.hSMul (α := R) (β := I →₀ R) ((a a_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) b_1 : I →₀ R)).sum
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    fun (i_1 : 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) ((a i_1 : (a : I) → R) i : R)
        (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
⊢ Eq (α := S ⊗[R] S)
    (f.sum fun (a_1 : I) (b_1 : S) ↦
      (HSMul.hSMul (α := R) (β := I →₀ R) ((a a_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) b_1 : I →₀ R)).sum
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (f.sum fun (i_1 : 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) ((a i_1 : (a : I) → R) i : R)
          (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))

Tactic:
congr
-- 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)
i : I
e_g :
  ∀ (j : I) (s : S),
    Eq.{u_2 + 1} (α := S ⊗[R] S)
      ((HSMul.hSMul (α := R) (β := I →₀ R) ((a j : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) s : I →₀ R)).sum
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
      (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (j_1 : I) (z : R) ↦
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a j : (a : I) → R) i : R)
          (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
⊢ Eq (α := I → S → S ⊗[R] S)
    (fun (a_1 : I) (b_1 : S) ↦
      (HSMul.hSMul (α := R) (β := I →₀ R) ((a a_1 : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) b_1 : I →₀ R)).sum
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    fun (i_1 : 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) ((a i_1 : (a : I) → R) i : R)
        (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))

Tactic:
ext j s
-- 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)
i j : I
s : S
e_g :
  Eq.{u_2 + 1} (α := S ⊗[R] S)
    (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (i_1 : I) (a_1 : R) ↦
      HSMul.hSMul (β := S ⊗[R] S) (HMul.hMul (α := R) ((a j : (a : I) → R) i : R) a_1)
        ((b : (a : I) → S) i_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (j_1 : I) (z : R) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a j : (a : I) → R) i : R)
        (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
e_g₁ :
  ∀ (i_1 : I),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S ⊗[R] S) 0
        ((b : (a : I) → S) i_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) =
      0
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    ((HSMul.hSMul (α := R) (β := I →₀ R) ((a j : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) s : I →₀ R)).sum
      fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (j_1 : I) (z : R) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a j : (a : I) → R) i : R)
        (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))

Tactic:
rw [Finsupp.sum_smul_index]

Premises used: Finsupp.sum_smul_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
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)
i j : I
s : S
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (i_1 : I) (a_1 : R) ↦
      HSMul.hSMul (β := S ⊗[R] S) (HMul.hMul (α := R) ((a j : (a : I) → R) i : R) a_1)
        ((b : (a : I) → S) i_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (j_1 : I) (z : R) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a j : (a : I) → R) i : R)
        (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))

Tactic:
simp only [mul_smul, Finsupp.sum, ← Finset.smul_sum]

Premises used: Finsupp.sum, Finset.smul_sum, SemigroupAction.mul_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
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)
i j : I
s : S
i_1 : I
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S ⊗[R] S) 0 ((b : (a : I) → S) i_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) =
    0

Tactic:
simp only [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
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)
i a_1 : I
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S ⊗[R] S) 0 ((b : (a : I) → S) a_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) =
    0

Tactic:
simp only [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
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)
i a_1 : I
b₁ b₂ : R
⊢ HSMul.hSMul (β := S ⊗[R] S) (b₁ + b₂) ((b : (a : I) → S) a_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) =
    HSMul.hSMul (β := S ⊗[R] S) b₁ ((b : (a : I) → S) a_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) +
      HSMul.hSMul (β := S ⊗[R] S) b₂ ((b : (a : I) → S) a_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)

Tactic:
simp only [add_smul]

Premises used: add_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
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)
⊢ ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R) ((a i : (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) ((a i : (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)))

Tactic:
have h₁ : ∀ k,
    (Finsupp.sum (Finsupp.sum f fun i y ↦ a i k • b.repr y) fun j z ↦ z • b j ⊗ₜ[R] b k) =
      (f.sum fun i y ↦ (b.repr y).sum fun j z ↦ a i k • z • b j ⊗ₜ[R] b k) := by
    intro i
    rw [Finsupp.sum_sum_index]
    · congr
      ext j s
      rw [Finsupp.sum_smul_index]
      · simp only [mul_smul, Finsupp.sum, ← Finset.smul_sum]
      intro; simp only [zero_smul]
    · intro; simp only [zero_smul]
    · intros; simp only [add_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
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) ((a i : (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) ((a i : (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)))
⊢ ∀ (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

Tactic:
simpa only [Finsupp.linearCombination_apply, Finsupp.sum] using b.linearCombination_repr

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, 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
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) ((a i : (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) ((a i : (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)))
⊢ ∀ (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

Tactic:
have h₂ : ∀ (x : S), ((b.repr x).support.sum fun a ↦ b.repr x a • b a) = x := by
    simpa only [Finsupp.linearCombination_apply, Finsupp.sum] using b.linearCombination_repr