Is there a reason simp doesn't finish the proof?

Stream: lean4

[Mark Santa Clara Munro]

I am not sure how to simplify this further, is there anything I am missing? I was thinking that maybe distributing the sum would be the issue, what could write to do so?

import Mathlib

theorem extracted_1.{u_1, u_2} {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n]
  (M : Matrix n m ℝ) (i j : n) (h1 : j ≠ i) (x : ℝ) (k : n) (l : m) (h : k = i) :
  ∑ x_1 : n, ((if i = x_1 then 1 else 0) + if j = x_1 then x else 0) * M x_1 l = M i l + x * M j l :=  by
sorry

For reference, I have had similar code when proving something else instead of this and it worked great, but there was no distributive and there was only one of "if i = x_1 then 1 else 0". It finished the proof in that situation.

[Ruben Van de Velde]

It would be easier for someone to look into it if you posted a #mwe

[Mark Santa Clara Munro]

I'm sorry, I usually include everything but I forgot this time, I will re-ask this question

[Mark Santa Clara Munro]

I am not sure how to simplify this further, is there anything I am missing? I was thinking that maybe distributing the sum would be the issue, what could write to do so?

import Mathlib

variable {m n : Type*} {α R : Type*}
variable [DecidableEq m]

-- Operation which add x times Row j to Row i
def addMulRow [SMul R α] [Add α] (M : Matrix m n α) (i : m) (j : m) (x : R): Matrix m n α :=
  Matrix.updateRow M i (M i + x • M j)

-- If you add a multiple of Row j into Row i, then it will be the original i plus the multiple of Row j
lemma addMulRowi [SMul R α] [Add α] (M : Matrix m n α) (i : m) (j : m) (x : R)
  : addMulRow M i j x i = M i + x • M j := by
  sorry

-- Let Eijx by the elementary matrix formed by adding a multiple of Row j to Row i of the identity matrix
-- Here we show that multiplying Eijx by M is the same as adding a multiple of Row j into Row i of M
theorem addMulRowMat_eq_addMulRow [DecidableEq n] [Fintype n] [Fintype m] (M : Matrix n m ℝ) (i : n) (j : n)  (x : ℝ)
  : addMulRow (1 : Matrix n n ℝ) i j x * M = addMulRow M i j x := by
  ext k l
  by_cases h : k = i
  · rw [h, addMulRowi]
    rw [Matrix.mul_apply, addMulRowi]
    simp
    simp_rw [Matrix.one_apply]
    simp

For reference, I have had similar code when proving mulRow instead of this and it worked great, but there was no distributive and there was only one of "if i = x_1 then 1 else 0". It finished the proof in that situation.

[Shreyas Srinivas]

Don't re ask questions. Edit them in place or add a new message in the same thread

[Mark Santa Clara Munro]

Okay sorry, I will edit it

[Shreyas Srinivas]

Secondly, you still haven't provided an #mwe

[Notification Bot]

Mark Santa Clara Munro has marked this topic as resolved.

[Notification Bot]

Mark Santa Clara Munro has marked this topic as unresolved.

[Mark Santa Clara Munro]

What do I need to change for one? I only used what is strictly necessary

[Shreyas Srinivas]

There is a lot of code. Try to isolate the issue. Maybe try using the extract_goals tactic to get the goal that isn't being closed as a separate theorem.

[Shreyas Srinivas]

Basically debug and minimise the example to the point where only the bare essentials are present for you to get the same error.

[Mark Santa Clara Munro]

I have done that, is it better now? I wasn't familiar with that tactic, thank you so much! I will watch out in the future

[Kevin Buzzard]

import Mathlib

theorem extracted_1.{u_1, u_2} {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n]
    (M : Matrix n m ℝ) (i j : n) (h1 : j ≠ i) (x : ℝ) (k : n) (l : m) (h : k = i) :
    ∑ x_1 : n, ((if i = x_1 then 1 else 0) + if j = x_1 then x else 0) * M x_1 l = M i l + x * M j l :=  by
  -- turn (a + b) * c into a * c + b * c in the sum
  simp_rw [add_mul]
  -- sum of (a + b) is sum of a + sum of b
  rw [Finset.sum_add_distrib]
  -- "(if P then a else b) * M" = "(if P then a * M else b * M)"
  simp_rw [ite_mul]
  -- 0 * M = 0
  simp_rw [zero_mul]
  -- sum over x of "if x = i then something else 0" is just the value at i
  rw [Fintype.sum_ite_eq]
  -- Can you take it from here?
  sorry

[Kevin Buzzard]

If you make it to the end let me know and I'll give you the easter egg

[Kevin Buzzard]

Your code has errors so it's hard to work out what you're asking.

lemma addMulRowi [SMul R α] [Add α] (M : Matrix m n α) (i : m) (j : m) (x : R)
  : addMulRow M i j x i = M i + x • M j := by
  simp [addMulRow]

fills in the sorry which doesn't have an error.

[Notification Bot]

4 messages were moved here from #lean4 > Is there a reason simp doesn't finish the proof by Ruben Van de Velde.

[Mark Santa Clara Munro]

That was so helpful, thank you so much! I was able to finish it, what is the easter egg? I'm excited

[Kevin Buzzard]

All of the lemmas you're rewiting with are simp lemmas apart from the very first add_mul so the entire proof is simp [add_mul].

[Mark Santa Clara Munro]

I tried it but it didn't conclude the goal, do I not need the Finset_sum_add_distrib? It works with the simp_rw [add_mul] and that one for me.

[Kevin Buzzard]

Ok, if that works for you that's great :-)