type casting about Fin (1 * n) and Fin n

Stream: new members

[polaris]

I'm working on proving some lemmas involving the Kronecker product, such as:

lemma kron_id_left : (I 1) ⊗ A = cast (by simp) A

After simplifying, I encountered the following issue:

import Mathlib.Data.Complex.Basic

set_option pp.proofs true

lemma h: i = (cast (Eq.symm (of_eq_true (Eq.trans (congrArg (fun x => Fin m = Fin x) (one_mul m)) (eq_self (Fin m))))) ⟨i, ip⟩) :=by
  sorry

I have tried

unfold cast

and

lemma eq_Fin_n (n: ℕ) : Fin (1 * n) = Fin n :=by
  simp
have hh :  Eq.symm (of_eq_true (Eq.trans (congrArg (fun x => Fin n = Fin x) (one_mul n)) (eq_self (Fin n)))) = eq_Fin_n n :=by
      simp

but

rw [hh]

failed
I don't have much experience with cast and type theory, so this goal feels quite difficult to tackle. I'd really appreciate any guidance on where to learn more about these concepts or how to approach solving this.

I believe the context provided should be sufficient to reproduce the issue.

[Aaron Liu]

You should use docs#Fin.cast instead

[Eric Wieser]

Could you provide your full statement of kron_id_left?

[polaris]

@Eric Wieser

import Mathlib.Algebra.Star.Basic
import Mathlib.Analysis.RCLike.Basic
import Mathlib.Data.Matrix.Basic
import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Matrix.Reflection

open Complex Matrix

notation "|" x "|" => ‖x‖
notation x "†" => star x

@[reducible]
def qMatrix (m n : Nat) := Matrix (Fin m) (Fin n) ℂ

notation "I" n => (1 : qMatrix n n)

section krondef

variable {m n p q : Nat}

lemma fin_add_mul_lt {m p : ℕ} (r : Fin m) (v : Fin p) :
    p * (r : ℕ) + (v : ℕ) < m * p := by
  cases r with | mk r hr =>
  cases v with | mk v hv =>
  simp only [Fin.val_mk]
  have f1 : p * (r + 1) ≤ p * m := by
    apply Nat.mul_le_mul
    linarith
    apply Nat.add_one_le_of_lt
    exact hr
  calc p * r + v < p * r + p := by linarith
               _ = p * (r + 1) := by ring
               _ ≤ p * m := f1
               _ = m * p := by ring

@[reducible]
def kronDiv (i : Fin (m * n)) : Fin m :=
  ⟨i.1 / n, Nat.div_lt_of_lt_mul (Nat.mul_comm m n ▸ i.2)⟩

@[reducible]
def kronMod (i : Fin (m*p)) : Fin p :=
⟨ (i : ℕ)%p, Nat.mod_lt (i : ℕ) (Nat.pos_of_mul_pos_left (Fin.pos i)) ⟩


def kron (A : qMatrix m n) (B : qMatrix p q) : qMatrix (m * p) (n * q) :=
  fun i j =>
    let hp : 0 < p := by
      apply Nat.pos_of_mul_pos_left
      exact Fin.pos i
    let hq : 0 < q := by
      apply Nat.pos_of_mul_pos_left
      exact Fin.pos j
    A (kronDiv i) (kronDiv j) * B (kronMod i) (kronMod j)


@[reducible]
def kronLoc (r : Fin m) (v : Fin p) : Fin (m * p) :=
  ⟨p * r.1 + v.1, fin_add_mul_lt r v⟩

end krondef

infixl:75 " ⊗ " => kron

section matrix_cast_apply

variable {α : Type*}
variable {m n m' n' : Type}  [Fintype m'] [Fintype n']
variable (A : Matrix m n α) (B : Matrix m' n' α)

lemma A_eq (m_eq : m = m') (n_eq : n = n') : Matrix m n α = Matrix m' n' α := by
  subst m_eq
  subst n_eq
  rfl

-- for easier pattern matching with matrix
lemma matrix_cast_apply (m_eq : m = m') (n_eq : n = n') (i' : m') (j' : n') :
    (cast (A_eq m_eq n_eq) A) i' j' = A (cast m_eq.symm i') (cast n_eq.symm j') := by
  subst m_eq
  subst n_eq
  rfl

end matrix_cast_apply

lemma nat_add_mul_left_div_left {a b c : ℕ} (c_pos : 0 < c) : (c * a + b) / c = a + b / c := by
  rw [add_comm]
  rw [Nat.add_mul_div_left _ _ c_pos]
  ring

lemma nat_add_mul_left_mod_left {a b c : ℕ} : (c * a + b) % c = b % c := by
  rw [add_comm, Nat.add_mul_mod_self_left]

lemma add_mul_congr_factor_lt_contra {a b c d e : ℕ} :
    c < a → b < d → ¬ (a * b + c = a * d + e) := by
  intro cp ep h
  have h3 : a * b + c < a * (b + 1) := by
    apply add_lt_add_left
    linarith
  have h4 : a * (b + 1) ≤ a * d := by
    apply mul_le_mul
    linarith
    exact Nat.succ_le_of_lt ep
    exact Nat.zero_le (b + 1)
    exact Nat.zero_le a
  linarith

lemma add_mul_congr_factor {a b c d e : ℕ} :
    c < a → e < a → a * b + c = a * d + e → b = d := by
  intro cp ep h
  by_contra h1
  cases Nat.lt_or_gt_of_ne h1 with
  | inl h2 => exact add_mul_congr_factor_lt_contra cp h2 h
  | inr h2 => exact add_mul_congr_factor_lt_contra ep h2 h.symm

lemma add_mul_congr {a b c d e : ℕ} :
    a * b + c = a * d + e → c < a → e < a → b = d ∧ c = e := by
  intro h cp ep
  cases add_mul_congr_factor cp ep h with
  | refl =>
    simp
    simp at h
    exact h


@[simp]
lemma id_one_apply {x y : Fin 1} : (I 1) x y = 1 := by
  have xp : x = 0 := by
    cases x with | mk x hx =>
    apply Fin.ext
    simp
    simp at hx
    exact hx
  have yp : y = 0 := by
    cases y with | mk y hy =>
    apply Fin.ext
    simp
    simp at hy
    exact hy
  subst xp
  subst yp
  simp



section kron
variable {m n p q : ℕ}
variable (A : qMatrix m n) (B : qMatrix p q)

set_option pp.proofs true

lemma eq_Fin_m : Fin m = Fin (1 * m) :=by
  simp

lemma eq_Fin_n (n: ℕ) : Fin (1 * n) = Fin n :=by
  simp

@[simp] lemma kron_id_left :
    (I 1) ⊗ A = cast (by simp) A := by
  apply Matrix.ext
  intro i j
  --rw[one_mul] at i j
  unfold qMatrix
  simp [kron, kronDiv, kronMod]
  cases i with |mk i ip =>
  cases j with |mk j jp =>
    --unfold cast
    simp
    --unfold qMatrix
    --rw [Eq.trans]
    rw [matrix_cast_apply]
    case a.mk.mk.m_eq =>
      simp
    case a.mk.mk.n_eq =>
      simp
    have ip': i < m:=by
      linarith
    have jp': j < n:=by
      linarith
    congr 2
    rw [Nat.mod_eq_of_lt ip']
    sorry
    sorry

end kron

This is my full statement of kron_id_left