How do I prove this lemma?

Stream: new members

[Ching-Tsun Chou]

After much confusion, I finally figured out what lemma I need to prove:

lemma aux_1 {k m n : ℕ} (hn : 0 < n) (heq : k * m = n) :
    (↑ m : ENNReal) / (↑ n : ENNReal) = 1 / (↑ k : ENNReal) := by
  sorry

How do I prove it? What is the systematic way to go about this?

[Aaron Liu]

What's your proof on paper? That is, why do you think this lemma is true?

[Ching-Tsun Chou]

The assumption heq implies that k, m, n are all positive. Now divide both sides of heq by n * k. Did I get something wrong?

[Ching-Tsun Chou]

Also, since k, m, n are natural numbers, their ENNReal counterparts cannot be \top. So we don't need to worry about \top, either.

[Aaron Liu]

import Mathlib

lemma aux_1 {k m n : ℕ} (hn : 0 < n) (heq : k * m = n) :
    (↑ m : ENNReal) / (↑ n : ENNReal) = 1 / (↑ k : ENNReal) := by
  subst heq
  have hm : m ≠ 0 := by rintro rfl ; simp at hn
  have hk : k ≠ 0 := by rintro rfl ; simp at hn
  refine (ENNReal.toReal_eq_toReal ?_ ?_).mp ?_
  · intro h
    apply_fun ENNReal.toReal at h
    simp [hm, hk] at h
  · intro h
    apply_fun ENNReal.toReal at h
    simp [hk] at h
  · field_simp
    ring

My thought process:
Since we don't have to worry about \top, convert everything to a Real, because Reals are more well behaved with these operations.
I found docs#ENNReal.toReal_eq_toReal with loogle VSCode autocomplete, and then got stuck trying to show that the division does not result in \top.
I had the idea: converting \top to a Real probably results in the default value 0, and the division is not 0, so I can apply_fun ENNReal.toReal to show the division is nontop.

[Ching-Tsun Chou]

Thanks! I did not know that something like k ≠ 0 can be used in simp. What was your Loogle search query?

[Ruben Van de Velde]

You can also extract a more general lemma and note that docs#ENNReal.div_eq_div_iff exists:

import Mathlib

lemma aux_2 {k m n : NNReal} (hn : n ≠ 0) (heq : k * m = n) :
    (↑ m : ENNReal) / (↑ n : ENNReal) = 1 / (↑ k : ENNReal) := by
  subst heq
  rw [ENNReal.div_eq_div_iff] <;> simp_all [← ENNReal.coe_mul]

lemma aux_1 {k m n : ℕ} (hn : 0 < n) (heq : k * m = n) :
    (↑ m : ENNReal) / (↑ n : ENNReal) = 1 / (↑ k : ENNReal) := by
  simp_rw [← ENNReal.coe_natCast]
  rw [aux_2] <;> simp_all [Nat.pos_iff_ne_zero, ← Nat.cast_mul]