help wanted porting Algebra.Hom.Centroid

Stream: mathlib4

[Maxwell Thum]

I'm having trouble porting the following from mathlib:

instance : has_add (centroid_hom α) :=
⟨λ f g,
  { map_mul_left' := λ a b, by simp [map_mul_left, mul_add], -- squeeze gives simp only [map_mul_left, mul_add, add_monoid_hom.to_fun_eq_coe, add_monoid_hom.add_apply, coe_to_add_monoid_hom]
    map_mul_right' := λ a b, by simp [map_mul_right, add_mul], -- squeeze gives simp only [map_mul_right, add_mul, add_monoid_hom.to_fun_eq_coe, add_monoid_hom.add_apply, coe_to_add_monoid_hom]
    ..(f + g : α →+ α) } ⟩

I messed around with it a bit and I currently have the following in mathlib4, which doesn't work:

instance : Add (CentroidHom α) :=
  ⟨fun f g ↦
    {
      (f + g : α →+
          α) with
      map_mul_left' := fun a b ↦ by simp [map_mul_left, mul_add, to_fun_eq_coe, AddMonoidHom.add_apply, coe_to_add_monoid_hom]
      map_mul_right' := fun a b ↦ by simp [map_mul_right, add_mul, to_fun_eq_coe, AddMonoidHom.add_apply, coe_to_add_monoid_hom] }⟩

[Johan Commelin]

Which branch is this?

[Maxwell Thum]

mathlib4#1325

[Johan Commelin]

@Maxwell Thum You could do something like

by
        show f (a * b) + g (a * b) = a * (f b + g b)
        simp [map_mul_left, mul_add]

[Maxwell Thum]

@Johan Commelin Thanks; that and the analogous thing for map_mul_right' seem to work!

[Maxwell Thum]

In

-- Eligible for `dsimp`
@[simp, norm_cast, nolint simpNF]
theorem coe_nsmul (f : CentroidHom α) (n : ℕ) : ⇑(n • f) = n • f :=
  rfl

the norm_cast linter is telling me this is a badly shaped lemma. The infoview sees the lemma as ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (n : ℕ), ↑(n • f) = ↑(n • f).

[Ruben Van de Velde]

should the rhs be n \bub (\u f)?

[Maxwell Thum]

n \bub (\u= f) works

[Maxwell Thum]

There's a comment in the file

-- Making `centroid_hom` an old structure will allow the lemma `to_add_monoid_hom_eq_coe`
-- to be true by `rfl`. After upgrading to Lean 4, this should no longer be needed
-- because eta for structures should provide the same result.

Does this mean I should just remove to_add_monoid_hom_eq_coe altogether?

[Yaël Dillies]

Old structures are not a thing in Lean 4. Please delete this comment.

[Maxwell Thum]

simpNF gives me

#check @CentroidHom.to_fun_eq_coe /- Left-hand side simplifies from
  ↑↑f.toAddMonoidHom
to
  ↑↑↑f
using
  simp only [CentroidHom.to_add_monoid_hom_eq_coe]
Try to change the left-hand side to the simplified term!
 -/

for

@[simp]
theorem to_fun_eq_coe {f : CentroidHom α} : f.toFun = (f : α → α) :=
  rfl
#align centroid_hom.to_fun_eq_coe CentroidHom.to_fun_eq_coe

but when I change f.toFun to ↑↑↑f, it becomes a tautology. Does this mean the lemma is redundant?

[Maxwell Thum]

simpNF also gives me

#check @CentroidHom.coe_nat_cast /- LINTER FAILED:
simplify fails on left-hand side:
maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit) -/

and

#check @CentroidHom.coe_int_cast /- LINTER FAILED:
simplify fails on left-hand side:
maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit) -/

for
theorem coe_nat_cast (n : ℕ) : ⇑(n : CentroidHom α) = n • (CentroidHom.id α)
and
theorem coe_int_cast (z : ℤ) : ⇑(z : CentroidHom α) = z • (CentroidHom.id α)
respectively.

[Maxwell Thum]

For coe_nat_cast and coe_int_cast, is Lean caught in a loop on \u=?

[Maxwell Thum]

Maxwell Thum said:

simpNF gives me

#check @CentroidHom.to_fun_eq_coe /- Left-hand side simplifies from
  ↑↑f.toAddMonoidHom
to
  ↑↑↑f
using
  simp only [CentroidHom.to_add_monoid_hom_eq_coe]
Try to change the left-hand side to the simplified term!
 -/

for

@[simp]
theorem to_fun_eq_coe {f : CentroidHom α} : f.toFun = (f : α → α) :=
  rfl
#align centroid_hom.to_fun_eq_coe CentroidHom.to_fun_eq_coe

but when I change f.toFun to ↑↑↑f, it becomes a tautology. Does this mean the lemma is redundant?

I looked at the porting wiki again and I guess the lemma was a tautology to begin with, so I removed it.

[Maxwell Thum]

Maxwell Thum said:

simpNF also gives me

#check @CentroidHom.coe_nat_cast /- LINTER FAILED:
simplify fails on left-hand side:
maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit) -/

and

#check @CentroidHom.coe_int_cast /- LINTER FAILED:
simplify fails on left-hand side:
maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit) -/

for
theorem coe_nat_cast (n : ℕ) : ⇑(n : CentroidHom α) = n • (CentroidHom.id α)
and
theorem coe_int_cast (z : ℤ) : ⇑(z : CentroidHom α) = z • (CentroidHom.id α)
respectively.

I ended up just telling simpNF to ignore these. Problem solved, I guess?

[Kevin Buzzard]

Please leave a porting note every time you deviate from the script