conditional `simp` lemmas

Stream: lean4

[Kevin Buzzard]

In mathlib, docs#zpow_lt_zpow_iff_right₀ is tagged simp. This is a theorem of the
form hyp -> (P <-> Q). But even if I put hyp in the local context, simp won't rewrite P to Q. How do I get this simp lemma to fire?

import Mathlib

#check zpow_lt_zpow_iff_right₀
/-
zpow_lt_zpow_iff_right₀.{u_2} {G₀ : Type u_2} [GroupWithZero G₀]
    [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀]
    {m n : ℤ} (ha : 1 < a) : a ^ m < a ^ n ↔ m < n
-/

universe u_2
example {G₀ : Type u_2} [GroupWithZero G₀]
    [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a : G₀} [PosMulStrictMono G₀]
    {m n : ℤ} (ha : 1 < a) : a ^ m < a ^ n := by
  -- rw [zpow_lt_zpow_iff_right₀] -- works fine
  -- simp -- does nothing
  -- simp only [zpow_lt_zpow_iff_right₀] -- does nothing
  revert ha
  -- simp -- still does nothing
  sorry

A mathlib-free version would be

@[simp] theorem foo (a : Nat) (h : a < 1) : a = 3 ↔ a = 4 := by
  omega

example (a : Nat) (h : a < 1) : a = 3 := by
  simp -- no progress

I am confused about whether stuff like this should be tagged @[simp].

[Tomas Skrivan]

That what the discharger is for, simp (disch:=assumption) You can specify a tactic to discharge assumptions for conditional simp theorems. assumption should be enough in this case.

simp +contextual should work after revert ha too

I'm on the phone and I didn't test it so hopefully it works.
(Btw I see you are struggling with jetlag too :grinning_face_with_smiling_eyes: )

[Daniel Weber]

Does simp [ha] work?

[Kevin Buzzard]

Aah I see -- so this must be how the simplifier is expected to use results like this.

[Kevin Buzzard]

simp_all also makes progress.