Lean simplifying issue

Stream: lean4

[Anirudh Suresh]

import Mathlib
open scoped Matrix

def tensor_product_2 {m n o p : ℕ} (A : Matrix (Fin m) (Fin n) ℂ)
  (B : Matrix (Fin o) (Fin p) ℂ) : Matrix (Fin (m * o)) (Fin (n * p)) ℂ :=
(Matrix.kroneckerMap (fun (a:ℂ) (b:ℂ) => a*b) A B).reindex finProdFinEquiv finProdFinEquiv

infixl:80 " ⊗ " => tensor_product_2

theorem t1 (q1 q2: Matrix (Fin 2) (Fin 1) ℂ) :
    (!![1, 0, 0, 0; 0, 0, 1, 0; 0, 1, 0, 0; 0, 0, 0, 1]: Matrix (Fin 4) (Fin 4) ℂ) * (q1)⊗(q2) = (q2)⊗(q1) := by
    {
      ext (i : Fin (2 * 2)) j
      revert i j
      simp_rw [finProdFinEquiv.surjective.forall]
      rintro ⟨i1, i2⟩ ⟨j1, j2⟩
      unfold tensor_product_2
      simp [Matrix.mul_apply]
      simp [Fin.sum_univ_four]
      fin_cases i1
      fin_cases i2
      fin_cases j1
      fin_cases j2
      simp
      simp [finProdFinEquiv]
      {
        sorry
      }
      {
        sorry
      }
      {
        simp [finProdFinEquiv]
        simp [Fin.divNat,Fin.modNat]
        rw [mul_comm]
        have p1:j1=0:=by {
          sorry
        }
        have p2:j2=0:=by {
          sorry
        }
        rw[p1,p2]
        fin_cases i2
        {
          sorry
        }
        {
          simp
          let i : Fin 2 := ⟨(3 : ℕ) / 2, by norm_num⟩
          let j : Fin 2 := ⟨(3 : ℕ) % 2, by norm_num⟩
          have h1 : i = 1 := by dsimp [i]
          have h2 : j = 1 := by dsimp [j]
          have LHS : q1 ⟨(3 : ℕ) / 2, by norm_num⟩ 0 = q1 i 0 := by dsimp [i]
          have RHS : q2 ⟨(3 : ℕ) % 2, by norm_num⟩ 0 = q2 j 0 := by dsimp [j]
          change (q1 i 0 * q2 j 0 = q2 1 0 * q1 1 0)
          rw[h1,h2]
          exact mul_comm (q1 1 0) (q2 1 0)
        }
      }
    }

in this code, right before the line

let i : Fin 2 := ⟨(3 : ℕ) / 2, by norm_num⟩

, the goal is as shown in the picture.
image.png
In order to take care of the "⟨↑3 / 2, ⋯⟩", i need to write those few lines of code. Is there a way in lean which would evaluate it directly to 1 (Some way such that any such expression gets simplified to its evaluated value)?

[Aaron Liu]

Try conving into it and do a equals (1 : Fin 2) => rfl

[Aaron Liu]

reduce can also do this, but it's a bit overeager sometimes

[Anirudh Suresh]

Aaron Liu said:

reduce can also do this, but it's a bit overeager sometimes

Yeah reduce doesnt seem to be doing the trick

[Aaron Liu]

reduce also has the quirk that it will not reduce types

[Aaron Liu]

So you need to enter the expression because _ = _ is a type

[Anirudh Suresh]

Does this allow me to simplify any expression to its value or only the one in my goal?

[Aaron Liu]

Any expression, if you use it correctly

[Aaron Liu]

The results may not be what you want though (I assume you're talking about reduce)

[Anirudh Suresh]

how would i use it correctly in this case?

[Aaron Liu]

conv_lhs => reduce will get reduce to only "see" the lhs, which is not a type and therefore subject to reduction

[Aaron Liu]

conv is generally more useful, but has a learning curve

[Anirudh Suresh]

Aaron Liu said:

conv_lhs => reduce will get reduce to only "see" the lhs, which is not a type and therefore subject to reduction

Doesnt doing this oversimplify it tho?

[Aaron Liu]

Yes, that's what I was talking about

[Aaron Liu]

reduce for me is only to expose definitions if I'm not familiar with them and want to see the internals

[Aaron Liu]

conv => enter [1, 1, 1] will get you where you want

[Aaron Liu]

Then you can do reduce, but since you know what you want to convert this to I would recommend change 1 instead

[Kyle Miller]

(For reference, reduce is never used once in all of mathlib.)

[Anirudh Suresh]

What if I do not know what I want to convert it to?

[Aaron Liu]

Then you can use reduce to get an idea of what you want to change this to, and then use change or simp or norm_num or rw to get there.

[Anirudh Suresh]

Ahh that makes sense