Can't subst

Stream: Is there code for X?

[Antoine Chambert-Loir]

I wish to prove the following result about docs#Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity :

import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

open Subgroup Matrix.SpecialLinearGroup Matrix

variable (n : Type*) [Fintype n] [DecidableEq n] (R : Type*) [CommRing R]

example (A : center (SpecialLinearGroup n R)) :
    A = scalar n ((center_equiv_rootsOfUnity A : Rˣ) : R) := sorry

but this function is a bit tricky and I can't manage to get some inner substitution away.

Namely, I have the following code

import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

open Subgroup Matrix.SpecialLinearGroup

variable (n : Type*) [Fintype n] [DecidableEq n] (R : Type*) [CommRing R]

example (A : center (SpecialLinearGroup n R)) :
    A = scalar n ((center_equiv_rootsOfUnity A : Rˣ) : R) := by
  by_cases hn : IsEmpty n
  · ext i j; exfalso
    exact IsEmpty.false i
  simp only [center_equiv_rootsOfUnity, Or.by_cases, dif_neg hn]
  rw [not_isEmpty_iff] at hn
  obtain ⟨i⟩ := id hn
  have : NeZero (Fintype.card n) := inferInstance
  have hA (i : n) := Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply i A
  simp only [← Subtype.coe_inj, ← Units.val_inj,
      rootsOfUnity.val_mkOfPowEq_coe] at hA
  rw [← scalar_eq_coe_self_center A (Classical.arbitrary n), ← hA]
  congr 2
  have : Fintype.card n = max (Fintype.card n) 1 := (max_eq_left (NeZero.one_le)).symm
  sorry

and the final goal is very similar to the following

import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

variable (n : Type*) [Fintype n] [DecidableEq n] (R : Type*) [CommRing R]

example {m n : ℕ} (hmn : m = n) (a : rootsOfUnity m R) :
    ((hmn ▸ a : rootsOfUnity n R) : Rˣ) = a := by
  subst hmn
  rfl

but I can't have the (presumably appropriate) subst work in my case.

[Etienne Marion]

When I find myself in this situation I write the result I need as a separate private lemma where subst works and I use it in the main proof.

[Antoine Chambert-Loir]

That didn't work neither, but I'll try harder!

[Antoine Chambert-Loir]

And indeed, your advice was excellent! I tried once more, and the trick was to add enough parameters for the auxiliary lemma so that no variable appears on both sides of the equality.

[Aaron Liu]

I'll have a go at it

[Aaron Liu]

doesn't work

[Aaron Liu]

center is not defined

[Aaron Liu]

I'll come back when you have a #mwe

[Aaron Liu]

oh it works now

[Antoine Chambert-Loir]

(I had forgotten to add the openline… sorry)

[Antoine Chambert-Loir]

import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

open Subgroup Matrix.SpecialLinearGroup

variable (n : Type*) [Fintype n] [DecidableEq n] (R : Type*) [CommRing R]

private lemma auxLemma (i : n) (A : center (SpecialLinearGroup n R))
    {m : ℕ} (h : Fintype.card n = m) :
    (((SpecialLinearGroup.center_equiv_rootsOfUnity' i) A) : Rˣ) =
      ((h ▸ SpecialLinearGroup.center_equiv_rootsOfUnity' i) A) := by
  subst h
  rfl

theorem _root_.Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity
    (A : center (SpecialLinearGroup n R)) :
    A = scalar n ((Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity A : Rˣ) : R) := by
  by_cases hn : IsEmpty n
  · ext i j; exfalso
    exact IsEmpty.false i
  simp only [Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity, Or.by_cases, dif_neg hn]
  rw [not_isEmpty_iff] at hn
  obtain ⟨i⟩ := id hn
  have : NeZero (Fintype.card n) := inferInstance
  have hA (i : n) := Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply i A
  simp only [← Subtype.coe_inj, ← Units.val_inj,
      rootsOfUnity.val_mkOfPowEq_coe] at hA
  rw [← Matrix.SpecialLinearGroup.scalar_eq_coe_self_center A (Classical.arbitrary n), ← hA]
  congr 2
  have := (max_eq_left (NeZero.one_le : 1 ≤ Fintype.card n)).symm
  rw [auxLemma]

seems to work. Thank you @Etienne Marion for the impetus!

[Aaron Liu]

oh center_equiv_rootsOfUnity is so ugly

[Aaron Liu]

and named wrong

[Aaron Liu]

oh this is terrible

[Antoine Chambert-Loir]

this was quite a mess, yes!

[Aaron Liu]

can we replace it

[Aaron Liu]

with something better

[Antoine Chambert-Loir]

Yes, one can remove the docs#Eq.rec it uses by something more explicit (take the unit, and write the according proof — by rewriting — that it has the given order). This will make the function easier to use.

[Aaron Liu]

I did it

import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

open Subgroup Matrix.SpecialLinearGroup Matrix

variable (n : Type*) [Fintype n] [DecidableEq n] (R : Type*) [CommRing R]

example (A : center (SpecialLinearGroup n R)) :
    A = scalar n ((center_equiv_rootsOfUnity A : Rˣ) : R) := by
  unfold center_equiv_rootsOfUnity Or.by_cases
  split_ifs with h
  · subsingleton
  dsimp only
  generalize_proofs _ eq
  generalize max (Fintype.card n) 1 = c at eq
  subst eq
  rw [center_equiv_rootsOfUnity'_apply, rootsOfUnity.val_mkOfPowEq_coe,
    scalar_eq_coe_self_center]

[Aaron Liu]

easy

[Ruben Van de Velde]

Misnamed and no API about it at all? Pretty disappointing that we landed that

[Antoine Chambert-Loir]

It's hard to check everything all the time. Don't blame yourself.

[Johan Commelin]

Thanks @Aaron Liu. Would you mind PRing the cleanup?

[Antoine Chambert-Loir]

That's included in #31078 (which, however, depends on #30987)