Simplify proof with ENNReal

Stream: new members

[Igor Khavkine]

As part of working on PR #9163, I've had to introduce a lemma about ENNReals. I've written a proof, but I think that due to my inexperience it came out a bit hacky. I suspect that with proper use of the simplification and automation tactics it could be made to look much nicer. Any suggestions/improvements welcome.

import Mathlib

open ENNReal

theorem ENNReal.add_sub_add_comm {a b c d : ENNReal}
    (ha : a ≠ ∞) (hb : b ≠ ∞) (hc : c ≠ ∞) (hd : d ≠ ∞)
    (hac : c ≤ a) (hbd : d ≤ b) :
    (a + b) - (c + d) = (a - c) + (b - d) := by
  apply calc
    a + b - (c + d) = .ofReal (a + b - (c + d)).toReal := (ofReal_toReal _).symm
    _               = .ofReal (a - c + (b - d)).toReal := ?cast_goal
    _               =          a - c + (b - d)         := (ofReal_toReal _)
  case cast_goal =>
    rw [ofReal_eq_ofReal_iff toReal_nonneg toReal_nonneg]
    repeat rw [toReal_add ?_, toReal_sub_of_le ?_ ?_]
    linarith
    repeat tauto
    exact add_le_add hac hbd
    repeat aesop
  aesop
  aesop

There is a general lemma docs#add_sub_add_comm, but it doesn't apply to ENNReal since it fails some of the hypotheses. Perhaps not all the ≠ ∞ are really necessary.

[Ruben Van de Velde]

If you assume none of your ENNReals are infinite, you're secretly working in NNReal:

import Mathlib

theorem NNReal.add_sub_add_comm {a b c d : NNReal}
    (hac : c ≤ a) (hbd : d ≤ b) :
    (a + b) - (c + d) = (a - c) + (b - d) := by
  apply calc
    a + b - (c + d) = Real.toNNReal (a + b - (c + d)).toReal := Real.toNNReal_coe.symm
    _               = Real.toNNReal (a - c + (b - d)).toReal := ?cast_goal
    _               =          a - c + (b - d)         := Real.toNNReal_coe
  rw [NNReal.coe_add]
  rw [NNReal.coe_sub (add_le_add hac hbd)]
  rw [NNReal.coe_sub hac]
  rw [NNReal.coe_sub hbd]
  rw [NNReal.coe_add]
  rw [NNReal.coe_add]
  rw [_root_.add_sub_add_comm]

open ENNReal

attribute [norm_cast] ENNReal.coe_sub

theorem ENNReal.add_sub_add_comm {a b c d : ENNReal}
    (ha : a ≠ ∞) (hb : b ≠ ∞) (hc : c ≠ ∞) (hd : d ≠ ∞)
    (hac : c ≤ a) (hbd : d ≤ b) :
    (a + b) - (c + d) = (a - c) + (b - d) := by
  lift a to NNReal using ha
  lift b to NNReal using hb
  lift c to NNReal using hc
  lift d to NNReal using hd
  norm_cast at *
  exact NNReal.add_sub_add_comm hac hbd

[Ruben Van de Velde]

Though you're correct that the assumptions are not minimal:

theorem ENNReal.add_sub_add_comm {a b c d : ENNReal}
    (hc : c ≠ ∞) (hd : d ≠ ∞)
    (hac : c ≤ a) (hbd : d ≤ b) :
    (a + b) - (c + d) = (a - c) + (b - d) := by
  lift c to NNReal using hc
  lift d to NNReal using hd
  obtain rfl|ha := eq_or_ne a ∞
  · simp [*]
  obtain rfl|hb := eq_or_ne b ∞
  · simp [*]
  lift a to NNReal using ha
  lift b to NNReal using hb
  norm_cast at *
  exact NNReal.add_sub_add_comm hac hbd

[Igor Khavkine]

Great, thanks! I unsuccessfully experiment with norm_cast first, but I obviously didn't know how to use it properly.