[Merged by Bors] - chore(algebra/punit_instances): add comm_cancel_monoid_with_zero, normalized_gcd_monoid, and scalar action instances

[eric-wieser]

Motivated by this Zulip thread.

This also moves the simp lemmas closer to the instances they refer to.

---

[eric-wieser]

This was causing horrible timeouts in files I don't care about, so in the interest of getting all the other instances merged I'm going to skip this one.

[robertylewis]

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed:

• Build mathlib

[Vierkantor]

The direct cause of the error seems to be that the _inst provided by letI fails the defeq check:

@normed_space 𝕜
  (@continuous_multilinear_map 𝕜 (fin m) (λ (i : fin m), E) (Π (i : ι), F' i)
     (λ (a b : fin m),
        (λ (a b : fin m), @subtype.decidable_eq ℕ (λ (x : ℕ), x < m) (λ (a b : ℕ), nat.decidable_eq a b) a b) a
          b)
     (@ring.to_semiring 𝕜
        (@normed_ring.to_ring 𝕜
           (@normed_comm_ring.to_normed_ring 𝕜
              (@normed_field.to_normed_comm_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_12)))))
     (λ (i : fin m),
        @add_comm_group.to_add_comm_monoid ((λ (i : fin m), E) i)
          (@normed_group.to_add_comm_group ((λ (i : fin m), E) i) ((λ (i : fin m), _inst_11) i)))
     (@add_comm_group.to_add_comm_monoid (Π (i : ι), F' i)
        (@normed_group.to_add_comm_group (Π (i : ι), F' i)
           (@pi.normed_group ι (λ (i : ι), F' i) _inst_14 (λ (i : ι), _inst_15 i))))
     (λ (i : fin m),
        @normed_space.to_module 𝕜 ((λ (i : fin m), E) i) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_12)
          ((λ (i : fin m), _inst_11) i)
          ((λ (i : fin m), _inst_13) i))
     (@normed_space.to_module 𝕜 (Π (i : ι), F' i) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_12)
        (@pi.normed_group ι (λ (i : ι), F' i) _inst_14 (λ (i : ι), _inst_15 i))
        (@pi.normed_space 𝕜 ι (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_12) (λ (i : ι), F' i) _inst_14
           (λ (i : ι), _inst_15 i)
           (λ (i : ι), _inst_16 i)))
     (λ (i : fin m),
        @uniform_space.to_topological_space ((λ (i : fin m), E) i)
          (@metric_space.to_uniform_space' ((λ (i : fin m), E) i)
             (@semi_normed_group.to_pseudo_metric_space ((λ (i : fin m), E) i)
                (@normed_group.to_semi_normed_group ((λ (i : fin m), E) i) ((λ (i : fin m), _inst_11) i)))))
     (@uniform_space.to_topological_space (Π (i : ι), F' i)
        (@metric_space.to_uniform_space' (Π (i : ι), F' i)
           (@semi_normed_group.to_pseudo_metric_space (Π (i : ι), F' i)
              (@normed_group.to_semi_normed_group (Π (i : ι), F' i)
                 (@pi.normed_group ι (λ (i : ι), F' i) _inst_14 (λ (i : ι), _inst_15 i)))))))
  (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_12)
  (@continuous_multilinear_map.to_normed_group 𝕜 (fin m) (λ (i : fin m), E) (Π (i : ι), F' i)
     (λ (a b : fin m),
        (λ (a b : fin m), @subtype.decidable_eq ℕ (λ (x : ℕ), x < m) (λ (a b : ℕ), nat.decidable_eq a b) a b) a
          b)
     (fin.fintype m)
     _inst_12
     (λ (i : fin m), (λ (i : fin m), _inst_11) i)
     (λ (i : fin m), (λ (i : fin m), _inst_13) i)
     (@pi.normed_group ι (λ (i : ι), F' i) _inst_14 (λ (i : ι), _inst_15 i))
     (@pi.normed_space 𝕜 ι (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_12) (λ (i : ι), F' i) _inst_14
        (λ (i : ι), _inst_15 i)
        (λ (i : ι), _inst_16 i)))
 := _inst_1 ?x_1 ?x_2
failed is_def_eq

[Vierkantor]

In addition, local attribute [-instance] punit.mul_action fixes the error.

[eric-wieser]

Does punit appear anywhere in the goal?

[Vierkantor]

Nope, although punit.mul_action does appear at a few points in the instance search log. I have no idea why that would break anything (out_params sneakily being unified wrongly?)

[Vierkantor]

Another way to fix it is to remind the elaborator that the instance exists:

  { intros m hm x hx,
    have := has_fderiv_within_at_pi.2 (λ i, (h i).fderiv_within m hm x hx),
    letI : normed_space 𝕜
      (continuous_multilinear_map 𝕜 (λ (i : fin m), E) (Π (i : ι), F' i)) := infer_instance,
    convert (L m).has_fderiv_at.comp_has_fderiv_within_at x this }, -- works?!

[Vierkantor]

Another thought, is this the instance-under-binder issue popping up again? (lean4 #509) That one has similar symptoms of inexplicable failure to find instances that goes away if you put the failing instance on its own and infer_instance it.

[eric-wieser]

I went for the letI solution because it's a bit more explanatory and the comment can go closer to the problem.

Weirly, by apply_instance fails where infer_instance succeeds...

[eric-wieser]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[eric-wieser]

#11972 (accidentally) makes this unecessary