Decidable prop in hypothesis

Stream: new members

[Li Xuanji]

As part of a proof by contradiction, I am in a situation where my hypothesis has a proposition whose falseness can be shown by decide, and my goal is False. Basically, the starting state of the proof here:

example (h : (1 = 0 ∨ 1 = 2)) : False := by
  have h' : ¬(1 = 0 ∨ 1 = 2) := by decide
  exact h' h

Is there a way to make this proof without restating h? Something like

example (h : (1 = 0 ∨ 1 = 2)) : False := by
  decide_tactic at h
  exact h

[Kyle Miller]

Try revert h; decide

At least here, simp at h should close the goal.

[Niels Voss]

For me, either revert h; decide or just contradiction or aesop work in this case, though I'm not sure what the solution is more generally

[Li Xuanji]

In my actual proof, my numbers are in ZMod 4 and simp doesn't work.

I'm having some trouble reducing it, but here's an example over lists where simp doesn't work

def l1 := [1]
def l2 := [2]

example (h : l1 = l2) : False := by
  have h' : l1 ≠ l2 := by decide
  exact h' h

[Kevin Buzzard]

And does the revert; decide dance work? Simp definitely won't work because it doesn't see through definitions. Does simp_all [l1,l2] work?