Finset.prod_add decidability diamond

Stream: lean4

[Arend Mellendijk]

I have this lemma I want to use that involves a Finset.sdiff of natural numbers. I'm running into the issue that it automatically uses that constructive Nat equality decidability instance. Is there some magic incantation I can write to make sure it uses the classical instance?

import Mathlib.NumberTheory.ArithmeticFunction
open Classical
open scoped Classical

theorem prod_compl_factors {n : ℕ} (hn : Squarefree n) {t : Finset ℕ} (ht : t ⊆ n.factors.toFinset) :
    ∏ a in (n.factors.toFinset \ t), a = n / (∏ a in t, a) := by
  sorry

[Sebastien Gouezel]

Normally, you should let Lean use the decidability instance it likes. Why is it an issue for you if it uses the Nat one?

[Arend Mellendijk]

I'm using docs#Finset.prod_add, which holds in more generality and hence uses the classical instance, and I can't make the two results fit together because of the different instances. Specifically, the only difference between those two expressions at the end are decidibility instances, as far as I can tell.

import Mathlib.NumberTheory.ArithmeticFunction

open Nat.ArithmeticFunction Classical
open scoped BigOperators Classical

theorem divisors_filter_squarefree_of_squarefree (n : ℕ) (hn : Squarefree n) :
    n.divisors.filter Squarefree = n.divisors := sorry

theorem prod_subset_factors_of_mult {R : Type _} [CommSemiring R] (f : Nat.ArithmeticFunction R)
  (h_mult : Nat.ArithmeticFunction.IsMultiplicative f) (l : ℕ)
  (t : Finset ℕ) (ht : t ⊆ l.factors.toFinset) :
    ∏ a : ℕ in t, f a = f (∏ a in t, a) := sorry

theorem prod_compl_factors {n : ℕ} (hn : Squarefree n) {t : Finset ℕ} (ht : t ⊆ n.factors.toFinset) :
    ∏ a in (n.factors.toFinset \ t), a = n / (∏ a in t, a) := by
  sorry

theorem mul_eq_mul {a b c d : α} [Mul α] (h0 : a = c) (h1 : b = d) : a*b=c*d := by
  rw [h0, h1]

--Nat.sum_divisors_filter_squarefree
theorem prod_add_mult' {R : Type _} [CommSemiring R] (f g : Nat.ArithmeticFunction R) (hf : IsMultiplicative f) (hg : IsMultiplicative g)
  (n : ℕ) (hn : Squarefree n) :
    ∏ p in n.factors.toFinset, (f p + g p) = (f * g) n := by

  rw [Finset.prod_add, mul_apply, Nat.sum_divisorsAntidiagonal (f:= λ x y => f x * g y),
    ←divisors_filter_squarefree_of_squarefree _ hn, Nat.sum_divisors_filter_squarefree $ Squarefree.ne_zero hn,
    Nat.factors_eq]
  apply Finset.sum_congr rfl
  intro t ht
  erw [Finset.prod_val]
  unfold _root_.id
  erw [←prod_compl_factors hn (Finset.mem_powerset.mp ht),
    prod_subset_factors_of_mult _ hf n t (Finset.mem_powerset.mp ht),
    ←prod_subset_factors_of_mult _ hg n (_ \ t) (Finset.sdiff_subset _ t) ]

  apply mul_eq_mul rfl
  apply Finset.prod_congr _ (fun _ _=> rfl)
  /-
  type mismatch
    HEq.rfl
  has type
    HEq ?m.6889 ?m.6889 : Prop
  but is expected to have type
    List.toFinset (Nat.factors n) \ t = List.toFinset (Nat.factors n) \ t : Prop
  -/
  rfl

[Yaël Dillies]

That means Finset.prod_add is miswritten. It should be about any decidability instance, not just the classical one.

[Kevin Buzzard]

docs#Finset.prod_add

[Kevin Buzzard]

Yeah Yaël is right. If you look at the source then there's an open Classical just before it

[Kevin Buzzard]

There was a time when the community had not properly understood how to handle these sorts of issues and perhaps this is left over from that time.

[Arend Mellendijk]

#5798

[Arend Mellendijk]

This'll have to wait until after the port