ENNReal: Marking lemmas with @[simp]

Stream: general

[Willem vanhulle]

I have tried to reduce boilerplate arithmetic calculations in my probability proofs. The proofs have to manipulate "extended-non-negative-reals" (ENNReal in Mathlib4). I came up with the following solution:

import Mathlib.Probability.ProbabilityMassFunction.Basic
import Mathlib.Probability.Notation
import Mathlib.Data.Finset.Basic
import Mathlib.Probability.ProbabilityMassFunction.Constructions
import Mathlib.Topology.Algebra.InfiniteSum.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Ring
import Mathlib.Data.Fintype.Card

open MeasureTheory ProbabilityTheory Set ENNReal Finset

@[simp] lemma ennreal_frac_reduce {a b c : ℕ} {hc_pos : 0 < c} :
  (a * c : ENNReal) / (b * c) = a / b := by
  apply ENNReal.mul_div_mul_right
  · simp [Nat.cast_ne_zero, ne_of_gt hc_pos]
  · simp [ENNReal.natCast_ne_top]

@[simp] lemma ennreal_inv_frac_mul_frac_general {a b c : ℕ} :
  (1 / (a : ENNReal))⁻¹ * ((b : ENNReal) / (c : ENNReal)) = ((a * b : ℕ) : ENNReal) / (c : ENNReal) := by
  rw [one_div, inv_inv, ← mul_div_assoc, Nat.cast_mul]

@[simp] lemma ennreal_ofReal_div_pos {a b : ℝ} {hb : 0 < b} :
  ENNReal.ofReal (a / b) = ENNReal.ofReal a / ENNReal.ofReal b :=
  ENNReal.ofReal_div_of_pos hb

@[simp] lemma ennreal_inv_inv {a: ENNReal}: (a ⁻¹)⁻¹ = a := by simp

@[simp] lemma ennreal_div_inv {a : ENNReal} {g: a ≠ ⊤} :
  ENNReal.ofReal ((1 / ENNReal.toReal a)⁻¹) = a := by
  rw [one_div, inv_inv, ENNReal.ofReal_toReal g]

@[simp] lemma ennreal_div_eq {a b : ENNReal} (h: b ≠ 0) (i: a ≠ ⊤):
  a / b = ENNReal.ofReal (ENNReal.toReal a / ENNReal.toReal b) := by
  rw [← ENNReal.ofReal_toReal (ENNReal.div_ne_top i h)]
  congr 1
  exact ENNReal.toReal_div a b

Is this the most efficient way? Did I state the @[simp] macro attribute correctly? I feel like the lemmas above are not structured in the most efficient way. Would it be possible to just tell Lean "do all arithmetic on ENNReal in Real as long as it is finite and non-zero"?

[Kenny Lau]

@Willem vanhulle Please include import Mathlib so the code compiles.

If you do #lint afterwards, you'll see the complaints about simpNF.

[Willem vanhulle]

Oh! You have the #lint command. I had never seen it before. Is it new? Maybe I should add support for it in the Lean-MCP server?

[Kenny Lau]

I thought it comes with mathlib

[Damiano Testa]

It is actually in Batteries and import Batteries.Tactic.Lint.Frontend is enough.

[Damiano Testa]

(In case it is useful, I got the information above using

import Mathlib.Tactic

#find_syntax "#lint"

and #find_syntax is in mathlib.)

[Willem vanhulle]

It is a pity you have to import Mathlib.Tactic, it takes a long time for me.

[Damiano Testa]

#find_syntax "#find_syntax" says that Mathlib.Tactic.FindSyntax is enough. :upside_down:

[Kevin Buzzard]

Willem vanhulle said:

It is a pity you have to import Mathlib.Tactic, it takes a long time for me.

Seconds or hours? If seconds, this should probably only be true the first time you type it. If hours, you're doing something wrong (you should run lake exe cache get to get the cache).