Reducing iff statements

Stream: new members

[Jack M]

In general, if I have hypotheses of the form

p : a ≤ 1 ↔  b ≤ 1
q : a = 1 ↔ b = 1

how might I deduce

r : a < 1 ↔ b < 1

[Eric Wieser]

I would guess docs#iff.or and docs#iff.not would help

[Eric Wieser]

That is, p.or q.not should get you almost to your goal

[Mario Carneiro]

I would do something like simp [lt_iff_le_and_ne, p, q]

[Adam Topaz]

Here's Mario's proof:

import tactic
import data.real.basic

example {a b : ℝ} (h1 : a ≤ 1 ↔ b ≤ 1) (h2 : a = 1 ↔ b = 1) :
  a < 1 ↔ b < 1 :=
by simp [lt_iff_le_and_ne, h1, h2]