Data.Nat.Factors mathlib4#1664

Stream: mathlib4

[Jihoon Hyun]

L241 ~ L257 contains the following code (with comments).

theorem dvd_of_factors_subperm {a b : ℕ} (ha : a ≠ 0) (h : a.factors <+~ b.factors) : a ∣ b := by
  rcases b.eq_zero_or_pos with (rfl | hb)
  · exact dvd_zero _
  rcases a with (_ | _ | a)
  · exact (ha rfl).elim
  · exact one_dvd _
  use (b.factors.diff a.succ.succ.factors).prod
  nth_rw 1 [← Nat.prod_factors ha]
  -- Porting note: Previous code was:
  -- rw [← List.prod_append,
  --   List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
  --   Nat.prod_factors hb.ne']
  --
  -- Fails to operate on the second line.
  -- However, the LHS of the second line is equal to the RHS of the status.
  admit
#align nat.dvd_of_factors_subperm Nat.dvd_of_factors_subperm

The LHS of List.Perm.prod_eq <| ... and the RHS of the goal are equal, but the rw fails.
I can't figure out what's happening here.

[Johan Commelin]

@Jihoon Hyun There are probably implicit differences.

[Johan Commelin]

Like differing typeclass variables

[Johan Commelin]

You can write set_option pp.explicit true above your theorem (or even above the tactic)

[Johan Commelin]

You can also try to change rw to erw. Then Lean tries a bit harder.

[Jihoon Hyun]

Thanks! I'll look at it again a few hours later!

[Frédéric Dupuis]

I had actually narrowed it down to something pretty scary: if you replace the code by this:

theorem dvd_of_factors_subperm {a b : ℕ} (ha : a ≠ 0) (h : a.factors <+~ b.factors) : a ∣ b := by
  rcases b.eq_zero_or_pos with (rfl | hb)
  · exact dvd_zero _
  rcases a with (_ | _ | a)
  · exact (ha rfl).elim
  · exact one_dvd _
  use (b.factors.diff a.succ.succ.factors).prod
  nth_rw 1 [← Nat.prod_factors ha]
  rw [← List.prod_append]
  have := (List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h).symm
  rw [Nat.prod_factors hb.ne'] at this
  convert this

you end up with the goal instBEqNat = instBEq, i.e. we seem to get a diamond in the BEq instance on Nat.

[Frédéric Dupuis]

Basically, after the last rw call, this and the goal look identical even if you click on it in the infoview, and then convert shows what the problem is.