Golfable proof?

Stream: lean4

[Wojciech Nawrocki]

Hello! In the context of std4 this proof felt like it should be a one-liner, but I ended up having to do a manual inversion. Does anyone see a quicker strategy?

example [BEq α]
    (a : α) (p q : α × β)
    (h: (p.fst == a) = true → (q.fst != a) = true)
    (hSome: Option.isSome (bif p.fst == a then some (a, b) else none) = true)
    : ¬Option.isSome (bif q.fst == a then some (a, b) else none) = true := by
  cases hEq: p.fst == a with
  | false => cases hEq ▸ hSome
  | true =>
    have : (q.fst == a) = false :=
      Bool.eq_false_iff.mpr (Bool.bne_iff_not_beq.mp <| h hEq)
    simp [this]

[Mario Carneiro]

kind of hammer-ish, but this works:

theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = if c then a else b := by cases c <;> rfl
theorem bne_iff [BEq α] (a b : α) : (a != b) ↔ ¬(a == b) := by unfold bne; cases a == b <;> decide

example [BEq α]
    (a : α) (p q : α × β)
    (h: (p.fst == a) = true → (q.fst != a) = true)
    (hSome: Option.isSome (bif p.fst == a then some (a, b) else none) = true)
    : ¬Option.isSome (bif q.fst == a then some (a, b) else none) = true := by
  revert hSome; simp [cond_eq_ite, bne_iff] at h ⊢; split <;> split <;> simp_all [Option.isSome]

[Mario Carneiro]

there are probably more things you can do in the lead-up to this goal to avoid the case splitting

[Mario Carneiro]

theorem bne_iff [BEq α] (a b : α) : (a != b) ↔ ¬(a == b) := by unfold bne; cases a == b <;> decide
theorem isSome_cond_some (c : Bool) (a : α) :
  (bif c then some a else none).isSome = c := by cases c <;> simp [Option.isSome]

example [BEq α]
    (a : α) (p q : α × β)
    (h: (p.fst == a) = true → (q.fst != a) = true)
    (hSome: Option.isSome (bif p.fst == a then some (a, b) else none) = true)
    : ¬Option.isSome (bif q.fst == a then some (a, b) else none) = true := by
  simp [isSome_cond_some, bne_iff] at *; exact h hSome