Difficulty in Mathlib/NumberTheory/Cyclotomic/Discriminant

Stream: mathlib4

[Kim Morrison]

@Riccardo Brasca, you're listed as the original author of this file, but anyone else who knows this file well: help here would be much appreciated. (I see that @Jeremy Tan did the port?)

On the lean-pr-testing-3151 branch, I can not get IsCyclotomicExtension.discr_prime_pow working (in Mathlib/NumberTheory/Cyclotomic/Discriminant.lean).

On this branch, the simplifier is behaving a bit differently, and won't visit instance arguments unless directed to via simp (config := { instances := true }). However, that doesn't seem to fix this proof, and I can't really see what's going on.

The critical steps of the proof are:

      -- Porting note: the goal at this point is `(discr K fun i ↦ ζ ^ ↑i) = 1`.
      -- This `simp_rw` is needed so the next `rw` can rewrite the type of `i` from
      -- `Fin (natDegree (minpoly K ζ))` to `Fin 1`
      simp_rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp]
      rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp,
        minpoly.eq_X_sub_C_of_algebraMap_inj _ (algebraMap K L).injective, natDegree_X_sub_C]

This is pretty nasty: we're using rw to rewrite a type. On the lean-pr-testing-3151 branch, the first step of the rw fails. I don't see why it used to not fail, to be honest!

If anyone is able to take a look at this proof and see if they can hack through it, that would be much appreciated.

[Kim Morrison]

It seems there is some whole API missing for changing the indexing type for discr, and this proof is a fragile hack trying to avoid that?

[Kim Morrison]

Ah, crisis averted, just adding a dsimp is enough. I've rewritten a little to use convert_to to make the type rewriting clearer.

convert_to (discr K fun i : Fin 1 ↦ (algebraMap K L) (-1) ^ ↑i) = _
      · simp_rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp]
        dsimp
        rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp,
          minpoly.eq_X_sub_C_of_algebraMap_inj _ (algebraMap K L).injective, natDegree_X_sub_C]
      · ... continue proof as before

works.

[Johan Commelin]

I guess it make sense to PR this diff already, right? Because it's simply a cleaner proof then what's there atm.

[Riccardo Brasca]

I agree the new proof is better, I can PR it if you want.

[Kim Morrison]

Thanks.

[Riccardo Brasca]

#9589

It is not your modification, but I've checked that it works in the lean-pr-testing-3151 branch. I think this one is more robust, I use docs#Algebra.discr_reindex to change the type.

[Kim Morrison]

@Riccardo Brasca, would you mind transplanting it into lean-pr-testing-3151, so I don't have to sort out the conflict later?