Typeclass inference help 2

Stream: new members

[Gareth Ma]

Is it possible to make the following work automatically for all IsMultiplicative functions?

import Mathlib.NumberTheory.VonMangoldt

open Nat Finset BigOperators ArithmeticFunction

variable {R : Type*} [Ring R] (f : ArithmeticFunction R)

instance (hf : IsMultiplicative f) : Invertible (f 1) := by
  rw [hf.map_one]
  exact invertibleOne

theorem only_if_invertible [Invertible (f 1)] : 1 + 1 = 3 := by
  sorry

example : 1 + 1 = 3 := by
  /- Use ζ -/
  apply only_if_invertible f /- fails to synthesize Invertible (f 1) -/

The idea is I want [Invertible (f 1)] to be inferred automatically (when possible, i.e. when f is multiplicative). This is because I am defining $f^{-1}$, which is only defined when $f(1) \in R^{\times}$.

[Gareth Ma]

Sorry if the example is not really clear, I can dump my full code when I'm done, so give me an hour or something.

[Gareth Ma]

In short I have a definition
def mkUnit (f : ArithmeticFunction R) [Invertible (f 1)] : (ArithmeticFunction R)ˣ := ⟨f, f.inv, f.mul_inv, f.inv_mul⟩

[Damiano Testa]

You can do

example : 1 + 1 = 3 := by
  /- Use ζ -/
  apply @only_if_invertible _ _ f (_)
  sorry

to make Invertible (f 1) an explicit goal.

[Gareth Ma]

Yeah I was trying to let the typeclass system infer it automatically, but I'll leave that aside for now.

[Jireh Loreaux]

(deleted - I misread)

[Gareth Ma]

Oh I might have typo'ed as well...

[Gareth Ma]

Okay I came up with a hack (and fixed my mistake). TLDR use [Fact ...] to infer the facts automatically.

instance [hf : Fact (IsMultiplicative f)] : Invertible (f 1) := by
  rw [hf.out.map_one]
  exact invertibleOne

theorem only_if_invertible [Invertible (f 1)] : 1 + 1 = 3 := by
  sorry

instance : Fact (IsMultiplicative (ζ : ArithmeticFunction R)) := by
  apply Fact.mk
  exact ⟨by simp, @fun m n h ↦ by
    simp only [natCoe_apply]; rw [isMultiplicative_zeta.right h, Nat.cast_mul]⟩

example : 1 + 1 = 3 := by
  apply only_if_invertible (ζ : ArithmeticFunction R) /- works now lol? -/

[Gareth Ma]

But this is probably not good code

[Gareth Ma]

I will just put something together then let some Lean expert take a look at it...