Embedding into product set

Stream: lean4

[Tony Ma]

I have encountered the problem of embedding the divisor set of $mn$ into the product set of the divisor set of $n$ times the divisor set of $m$.
Minimal working example:

import Mathlib

example (m n : ℕ) (npos : 0 < n) (mpos : 0 < m) (h : n.Coprime m) : True := by
  let ϕ : (Finset.Icc 1 (m * n)).filter (fun f => f ∣ (m * n)) ↪ ((Finset.Icc 1 n).filter (fun d => d ∣ n) × (Finset.Icc 1 m).filter (fun e => e ∣ m)) := ⟨fun f => ?_, ?_⟩
  pick_goal 2
  . -- Assign value to ϕ.
    simp at f ⊢
    obtain ⟨f, ⟨⟨hf₁, hf₂⟩, hf₃⟩⟩ := f
    refine ⟨?_, ?_⟩
    use Nat.gcd f n
    refine ⟨⟨by apply Nat.gcd_pos_of_pos_left n hf₁, by apply Nat.gcd_le_right n npos⟩, by apply Nat.gcd_dvd_right⟩
    use Nat.gcd f m
    refine ⟨⟨by apply Nat.gcd_pos_of_pos_left m hf₁, by apply Nat.gcd_le_right m mpos⟩, by apply Nat.gcd_dvd_right⟩
  pick_goal 2
  . -- Prove that ϕ is injective.
    simp
    sorry

In the sorry place I get this info:
info.png

It was just too complicated that I tried everything but still cannot reduce. Is there a way to reduce heq in my code, or is it recommended to use other ways to define such an embedding? (I was doing this because I want to change some summation f=1 to m * n to a double summation.)

(I tried replacing × by ×ˢ or Finset.filter by Nat.divisors, but the similar complex stuffs still occur when I tried proving the embedding is injective.)

[Daniel Weber]

You should try to define the function directly as a term, it's hard to argue about data defined in tactic mode

[Tony Ma]

I've definitely tried. But it turns out that I was unable to define the function without proving that it is well-defined.
error.png

[Tony Ma]

Daniel Weber 发言道：

You should try to define the function directly as a term, it's hard to argue about data defined in tactic mode

I'm afraid that I may really have to argue about data defined in tactic mode. Is there a possible way to do it? What's the reason for such a mess in LEAN?

[Daniel Weber]

You can do

let ϕ : (Finset.Icc 1 (m * n)).filter (fun f => f ∣ (m * n)) ↪ ((Finset.Icc 1 n).filter (fun d => d ∣ n) × (Finset.Icc 1 m).filter (fun e => e ∣ m)) := ⟨fun f => (⟨Nat.gcd f n, ?_⟩, ⟨Nat.gcd f m, ?_⟩), ?_⟩

so the data is defined in term mode and only the proof is defined in tactic mode

[Tony Ma]

Daniel Weber 发言道：

You can do

let ϕ : (Finset.Icc 1 (m * n)).filter (fun f => f ∣ (m * n)) ↪ ((Finset.Icc 1 n).filter (fun d => d ∣ n) × (Finset.Icc 1 m).filter (fun e => e ∣ m)) := ⟨fun f => (⟨Nat.gcd f n, ?_⟩, ⟨Nat.gcd f m, ?_⟩), ?_⟩

so the data is defined in term mode and only the proof is defined in tactic mode

Ok. I just tried. But I get something that I was unable to get rid of... (When I do simp at f, the f in the goal becomes f✝, so I was unable to access the simplified f.)
image.png

[Daniel Weber]

Try doing obtain ⟨f, hf⟩ := f and then simp at hf

[Tony Ma]

Daniel Weber 发言道：

Try doing obtain ⟨f, hf⟩ := f and then simp at hf

Oh ok. This helps. Thanks!