Equating (A → (B × C)) and (A → B) × (A → C)

Stream: Is there code for X?

[Terence Tao]

I needed to convert a sum over (A → (B × C)) to a sum over (A → B) × (A → C) and found it surprisingly fiddly:

import Mathlib

open BigOperators

example (A B C:Type*) [Fintype A] [Fintype B] [Fintype C] (f : (A → (B × C)) → ℝ) :
  have := Fintype.ofFinite (A → B)
  have := Fintype.ofFinite (A → C)
  have := Fintype.ofFinite (A → (B × C))
  ∑ p, f p = ∑ q : (A → B) × (A → C), f (fun a ↦ ⟨ q.1 a, q.2 a ⟩) := by
    have := Fintype.ofFinite (A → B)
    have := Fintype.ofFinite (A → C)
    have := Fintype.ofFinite (A → (B × C))
    set e : (A → (B × C)) ≃ (A → B) × (A → C) := {
          toFun := fun G ↦ ⟨ fun i ↦ (G i).1, fun i ↦ (G i).2 ⟩
          invFun := fun F ↦ (fun i ↦ ⟨ F.1 i, F.2 i ⟩)
          left_inv := by
            intro _
            simp only [Prod.mk.eta]
          right_inv := by
            intro _
            simp only [Prod.mk.eta]
        }
    convert Fintype.sum_equiv e _ _ _
    intro F
    simp only [Equiv.coe_fn_mk, Prod.mk.eta, e]

Firstly, it seems that the instances Fintype A and Fintype B do not automatically generate the instance Fintype A → B, so I had to manually enter them. Secondly, I couldn't find an existing equivalence between (A → (B × C)) and (A → B) × (A → C) in Mathlib, so I had to make it myself. And finally, the statement itself doesn't seem to be in Mathlib. But perhaps I missed some tools in Mathlib that would make this easier?

[Adam Topaz]

If you open Classical, you won't need to manually add the instances.

[Adam Topaz]

Also with exact?% I found the following:

example (A B C : Type*) : (A → (B × C)) ≃ ((A → B) × (A → C)) := Equiv.arrowProdEquivProdArrow
  B C A

[Adam Topaz]

that should help getting your example down to just a couple of lines :)

[Sébastien Gouëzel]

import Mathlib

open Classical in
example (A B C:Type*) [Fintype A] [Fintype B] [Fintype C] (f : (A → (B × C)) → ℝ) :
    ∑ p, f p = ∑ q : (A → B) × (A → C), f (fun a ↦ ⟨ q.1 a, q.2 a ⟩) :=
  Fintype.sum_equiv (Equiv.arrowProdEquivProdArrow B C A) _ _ (by tauto)

[Adam Topaz]

I got it down to two lines:

import Mathlib

open BigOperators

open Classical in
example (A B C:Type*) [Fintype A] [Fintype B] [Fintype C] (f : (A → (B × C)) → ℝ) :
  ∑ p, f p = ∑ q : (A → B) × (A → C), f (fun a ↦ ⟨ q.1 a, q.2 a ⟩) := by
    apply Fintype.sum_equiv (Equiv.arrowProdEquivProdArrow B C A) f
    aesop

[Adam Topaz]

More or less the same as Sebastien's proof :)

[Sébastien Gouëzel]

The key is really the exact? telling you the name of Equiv.arrowProdEquivProdArrow.

[Sébastien Gouëzel]

@loogle (?_ → (?_ × ?_)) ≃ ((?_ → ?_) × (?_ → ?_))

[loogle]

:search: Equiv.arrowProdEquivProdArrow

[Sébastien Gouëzel]

(Or you can ask loogle like I just did, here on Zulip or on its webpage https://loogle.lean-lang.org/?q=%28%3F_+%E2%86%92+%28%3F_+%C3%97+%3F_%29%29+%E2%89%83+%28%28%3F_+%E2%86%92+%3F_%29+%C3%97+%28%3F_+%E2%86%92+%3F_%29%29)

[Adam Topaz]

... or even in VSCode itself!

[Sébastien Gouëzel]

How do you do it in VSCode?

[Adam Topaz]

click the $\forall$ and there is a loogle option

[Adam Topaz]

it opens the webpage in a browser within vscode.

[Sébastien Gouëzel]

Awesome, thanks!

[Johan Commelin]

There's also a Loogle extension for VScode. And I think you can start a loogle query using Ctrl-Shift-L.

[Shreyas Srinivas]

That extension (loogle lean) also adds a search icon that typically appears next to the forall symbol.

[Kyle Miller]

Adam Topaz said:

If you open Classical, you won't need to manually add the instances.

It should also be possible to do have := Fintype.ofFinite just once (without any arguments), in case classical adds any complications.