barber's paradox

Stream: new members

[Claus-Peter Becke]

variables (men : Type*) (barber : men)
variable (shaves : men → men → Prop)

example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : false :=
begin
end

It is to prove that a contradiction follows from the hypotheses. My goal is to find two hypotheses which contradict each other. The first I would like to do is to remove the universal quantifier from the hypothesis. To be able to do that, x should be introduced. But to introduce it as an arbitrary object presupposes that the quantified x appears inside the goal. The only way to achieve this is to use the revert-tactic as far as I see. But after having done that I'll get an implication forall x ... -> false. Which alternatives do I have?

[Kenny Lau]

have h1 := h barber

[Claus-Peter Becke]

@Kenny Lau
Thanks.

[Alexandre Rademaker]

why using Type* ? Why not only Type?

[Scott Morrison]

Don't you have barbers in your universe? :-)

[Alexandre Rademaker]

Sorry, I didn't understand.

[Kenny Lau]

Type* means in an arbitrary universe

[Eric Wieser]

A proof of the barber paradox was discussed before in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/barber.20paradox/near/206917550