rw not accepting pattern

Stream: new members

[Anirudh Suresh]

import Mathlib.Data.Complex.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Matrix.Kronecker
import Mathlib.LinearAlgebra.UnitaryGroup
open scoped Matrix
open ComplexConjugate

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

def conjugate_transpose {m n : Type*} [Fintype m] [Fintype n]
  (A : Matrix m n ℂ) : Matrix n m ℂ :=
Matrix.transpose (Matrix.map A (fun (x:ℂ)=> conj x))

theorem t1 (q1 q2 q3 q4: Matrix (Fin 2) (Fin 1) ℂ): ((conjugate_transpose q1 * q2) ⊗ (conjugate_transpose q3 * q4)) 0 0 =
  (conjugate_transpose q1 * q2) 0 0 * (conjugate_transpose q3 * q4) 0 0:=by {
    unfold conjugate_transpose
    unfold tensor_product_2
    simp only [Matrix.reindex_apply, Matrix.kroneckerMap_apply]
    rw [Matrix.submatrix_apply]
    have h : finProdFinEquiv.symm (0 : Fin (2*2)) = (0, 0) :=
    by rw [← Equiv.apply_symm_apply finProdFinEquiv (0 : Fin (2*2))]; rfl
    rw [h]
  }

even though there is an instance of the pattern in the goal, Lean says there isn't. Why is this the case?

[Aaron Liu]

The hypothesis h says that finProdFinEquiv.symm (0 : Fin (2 * 2)) = ((0 : Fin 2), (0 : Fin 2)).
The pattern in the goal is finProdFinEquiv.symm (0 : Fin (1 * 1)).
These are not the same

[Eric Wieser]

Are you aware of docs#Matrix.conjTranspose ?

[Notification Bot]

This topic was moved here from #lean4 > rw not accepting pattern by Eric Wieser.