no contradiction

Stream: general

[Kevin Buzzard]

example (P : Prop) (hP : ¬ P) : ¬ P := by contradiction

Where's the contradiction?

This is minimised from

import tactic

example (X : Type) (s : set X) (a : X) (ha : a ∉ s) :
  ∃ b : X, b ∉ s :=
begin
  use a, -- done!
end

-- apparently use tries triv, which is a weaker version of trivial, which tries contradiction.

[Kyle Miller]

It looks like contradiction starts with intro1 and then assembles an absurd proof using hP and the term of P.