awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
rw :
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
      A =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * C * V) -
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              C *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
        (U * C * V)
⊢ 1 -
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
          A +
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * C * V) -
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
          (U * C * V)) =
    1

Tactic:
rw [sub_add, sub_eq_self, sub_eq_zero]

Premises used: sub_add, sub_eq_zero, sub_eq_self
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
simp :
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
      (U *
        (C *
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)))))) =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
      (U *
        (C *
          (V -
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V))))))))
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
      A =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * C * V) -
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              C *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
        (U * C * V)

Tactic:
simp only [Matrix.mul_assoc, ← Matrix.mul_sub]

Premises used: Matrix.mul_assoc, Matrix.mul_sub
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
e_a :
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
      (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A))) =
    V -
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
          (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
        (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V)))))
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
      (U *
        (C *
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)))))) =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
      (U *
        (C *
          (V -
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V))))))))

Tactic:
congr
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
e_a :
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
      (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)) +
        C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V))))) =
    V
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
      (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A))) =
    V -
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
          (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
        (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V)))))

Tactic:
rw [eq_sub_iff_add_eq, ← Matrix.mul_add]

Premises used: eq_sub_iff_add_eq, Matrix.mul_add
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
e_a :
  C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)) +
      C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V)))) =
    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) * V
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
      (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)) +
        C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V))))) =
    V

Tactic:
rw [Matrix.invOf_mul_eq_iff_eq_mul_left]

Premises used: Matrix.invOf_mul_eq_iff_eq_mul_left
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
e_a :
  C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V)))) =
    C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C * V
⊢ C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)) +
      C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V)))) =
    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) * V

Tactic:
simp only [Matrix.add_mul, invOf_mul_self', Matrix.mul_one, add_right_inj]

Premises used: Matrix.add_mul, Matrix.mul_one, invOf_mul_self', add_right_inj
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V)))) =
    C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C * V

Tactic:
simp only [Matrix.mul_assoc]

Premises used: Matrix.mul_assoc
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
inst_7 : Invertible (A + U * C * V)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul' U C V
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A + U * C * V) _ =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A + U * C * V) _

Tactic:
(rfl : ⅟(A + U * C * V) = _)

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
inst_7 : Invertible (A + U * C * V)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul' U C V
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A + U * C * V) _ =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _

Tactic:
convert! (rfl : ⅟(A + U * C * V) = _)

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalSemiring α
u : m → α
w : n → α
v : Matrix m n α
⊢ (fun (j : n) ↦ u ⬝ᵥ fun (i : m) ↦ v i j) ⬝ᵥ w = u ⬝ᵥ fun (i : m) ↦ v i ⬝ᵥ w

Tactic:
simpa [dotProduct, Finset.mul_sum, Finset.sum_mul, mul_assoc] using Finset.sum_comm

Premises used: Finset.mul_sum, dotProduct, mul_assoc, Finset.sum_comm, Finset.sum_mul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
α : Type v
inst : AddCommMonoid α
inst_1 : Mul α
v w : PUnit.{u_10 + 1} → α
⊢ v ⬝ᵥ w = v PUnit.unit * w PUnit.unit

Tactic:
simp [dotProduct]

Premises used: dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : Fintype n
inst_1 : MulOneClass α
inst_2 : AddCommMonoid α
v : n → α
⊢ v ⬝ᵥ 1 = ∑ i : n, v i

Tactic:
simp [(· ⬝ᵥ ·)]

Premises used: dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
n : Type u_3
α : Type v
inst : Fintype n
inst_1 : MulOneClass α
inst_2 : AddCommMonoid α
v : n → α
⊢ 1 ⬝ᵥ v = ∑ i : n, v i

Tactic:
simp [(· ⬝ᵥ ·)]

Premises used: dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
v : m → α
⊢ v ⬝ᵥ 0 = 0

Tactic:
simp [dotProduct]

Premises used: dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
v : m → α
⊢ (v ⬝ᵥ fun (x : m) ↦ 0) = 0

Tactic:
dotProduct_zero v

Premises used: dotProduct_zero
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
v : m → α
⊢ 0 ⬝ᵥ v = 0

Tactic:
simp [dotProduct]

Premises used: dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
v : m → α
⊢ (fun (x : m) ↦ 0) ⬝ᵥ v = 0

Tactic:
zero_dotProduct v

Premises used: zero_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
u v w : m → α
⊢ (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w

Tactic:
simp [dotProduct, add_mul, Finset.sum_add_distrib]

Premises used: add_mul, dotProduct, Finset.sum_add_distrib
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
u v w : m → α
⊢ u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w

Tactic:
simp [dotProduct, mul_add, Finset.sum_add_distrib]

Premises used: dotProduct, Finset.sum_add_distrib, mul_add
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalNonAssocSemiring α
u v : m → α
x y : n → α
⊢ Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y

Tactic:
simp [dotProduct]

Premises used: dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalNonAssocSemiring α
u : m → α
x : n → α
e : m ≃ n
x_1 : m
h : Membership.mem (γ := Finset m) Finset.univ x_1
⊢ Function.comp.{u_3 + 1, u_2 + 1, v + 1} (α := n) u ((⇑e.symm : (a : n) → m) : (a : n) → m)
        ((e : (a : m) → n) x_1 : n) *
      x ((e : (a : m) → n) x_1) =
    u x_1 * (x ∘ (⇑e : (a : m) → n)) x_1

Tactic:
simp only [Function.comp, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, Function.comp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalNonAssocSemiring α
u : m → α
x : n → α
e : n ≃ m
⊢ u ⬝ᵥ x ∘ (⇑e.symm : (a : m) → n) = u ∘ (⇑e : (a : n) → m) ⬝ᵥ x

Tactic:
simpa only [Equiv.symm_symm] using (comp_equiv_symm_dotProduct u x e.symm).symm

Premises used: Equiv.symm_symm, Equiv.symm, Eq.symm, comp_equiv_symm_dotProduct
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalNonAssocSemiring α
x y : n → α
e : m ≃ n
⊢ dotProduct.{v, u_2} (m := m) (x ∘ (⇑e : (a : m) → n)) (y ∘ (⇑e : (a : m) → n)) = x ⬝ᵥ y

Tactic:
simp [← dotProduct_comp_equiv_symm, Function.comp_def _ e.symm]

Premises used: dotProduct_comp_equiv_symm, Function.comp_def, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
ι : Type u_10
u : m → α
s : Finset ι
v : ι → m → α
simp : Eq.{v + 1} (α := α) (∑ x : m, ∑ i ∈ s, u x * v i x) (∑ x ∈ s, ∑ i : m, u i * v x i)
⊢ u ⬝ᵥ ∑ i ∈ s, v i = ∑ i ∈ s, u ⬝ᵥ v i

Tactic:
simp only [dotProduct, Finset.sum_apply, Finset.mul_sum]

Premises used: Finset.mul_sum, dotProduct, Finset.sum_apply
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
ι : Type u_10
u : m → α
s : Finset ι
v : ι → m → α
rw rw₁ : Eq.{v + 1} (α := α) (∑ y ∈ s, ∑ x : m, u x * v y x) (∑ x ∈ s, ∑ i : m, u i * v x i)
⊢ Eq.{v + 1} (α := α) (∑ x : m, ∑ i ∈ s, u x * v i x) (∑ x ∈ s, ∑ i : m, u i * v x i)

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
ι : Type u_10
s : Finset ι
u : ι → m → α
v : m → α
simp : Eq.{v + 1} (α := α) (∑ x : m, ∑ i ∈ s, u i x * v x) (∑ x ∈ s, ∑ i : m, u x i * v i)
⊢ (∑ i ∈ s, u i) ⬝ᵥ v = ∑ i ∈ s, u i ⬝ᵥ v

Tactic:
simp only [dotProduct, Finset.sum_apply, Finset.sum_mul]

Premises used: dotProduct, Finset.sum_apply, Finset.sum_mul
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
ι : Type u_10
s : Finset ι
u : ι → m → α
v : m → α
rw rw₁ : Eq.{v + 1} (α := α) (∑ y ∈ s, ∑ x : m, u y x * v x) (∑ x ∈ s, ∑ i : m, u x i * v i)
⊢ Eq.{v + 1} (α := α) (∑ x : m, ∑ i ∈ s, u i x * v x) (∑ x ∈ s, ∑ i : m, u x i * v i)

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i j : m
hij : j ≠ i
⊢ diagonal v i j * w j = 0

Tactic:
simp [diagonal_apply_ne' _ hij]

Premises used: Matrix.diagonal_apply_ne'
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
⊢ ∀ (j : m), j ≠ i → diagonal v i j * w j = 0

Tactic:
have : ∀ j ≠ i, diagonal v i j * w j = 0 := fun j hij => by
    simp [diagonal_apply_ne' _ hij]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ ∑ x : m, diagonal v i x * w x = diagonal v i i * w i

Tactic:
Finset.sum_eq_single i (fun j _ => this j) _

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
h : v i * w i = diagonal v i i * w i
convert_2 : i ∉ Finset.univ → diagonal v i i * w i = 0
⊢ diagonal v i ⬝ᵥ w = v i * w i

Tactic:
convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ v i * w i = diagonal v i i * w i

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ i ∉ Finset.univ → diagonal v i i * w i = 0

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i j : m
hij : j ≠ i
⊢ v j * diagonal w i j = 0

Tactic:
simp [diagonal_apply_ne' _ hij]

Premises used: Matrix.diagonal_apply_ne'
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
⊢ ∀ (j : m), j ≠ i → v j * diagonal w i j = 0

Tactic:
have : ∀ j ≠ i, v j * diagonal w i j = 0 := fun j hij => by
    simp [diagonal_apply_ne' _ hij]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ ∑ x : m, v x * diagonal w i x = v i * diagonal w i i

Tactic:
Finset.sum_eq_single i (fun j _ => this j) _

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
h : v i * w i = v i * diagonal w i i
convert_2 : i ∉ Finset.univ → v i * diagonal w i i = 0
⊢ v ⬝ᵥ diagonal w i = v i * w i

Tactic:
convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ v i * w i = v i * diagonal w i i

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ i ∉ Finset.univ → v i * diagonal w i i = 0

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i j : m
hij : j ≠ i
⊢ v j * diagonal w j i = 0

Tactic:
simp [diagonal_apply_ne _ hij]

Premises used: Matrix.diagonal_apply_ne
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
⊢ ∀ (j : m), j ≠ i → v j * diagonal w j i = 0

Tactic:
have : ∀ j ≠ i, v j * diagonal w j i = 0 := fun j hij => by
    simp [diagonal_apply_ne _ hij]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ ∑ x : m, v x * diagonal w x i = v i * diagonal w i i

Tactic:
Finset.sum_eq_single i (fun j _ => this j) _

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
h : v i * w i = v i * diagonal w i i
convert_2 : i ∉ Finset.univ → v i * diagonal w i i = 0
⊢ (v ⬝ᵥ fun (j : m) ↦ diagonal w j i) = v i * w i

Tactic:
convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ v i * w i = v i * diagonal w i i

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ i ∉ Finset.univ → v i * diagonal w i i = 0

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i j : m
hij : j ≠ i
⊢ HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x j : α) (v j) = 0

Tactic:
simp [Pi.single_eq_of_ne hij]

Premises used: Pi.single_eq_of_ne
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
⊢ ∀ (j : m), j ≠ i → HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x j : α) (v j) = 0

Tactic:
have : ∀ j ≠ i, (Pi.single i x : m → α) j * v j = 0 := fun j hij => by
    simp [Pi.single_eq_of_ne hij]
-- Module: Mathlib.Data.Matrix.Mul
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x j : α) (v j) = 0
⊢ ∑ x_1 : m, HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x x_1 : α) (v x_1) =
    HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x i : α) (v i)

Tactic:
Finset.sum_eq_single i (fun j _ => this j) _

Premises used: Finset.sum_eq_single