CODEWITHSUNDEEP
logiclean
Srikar Yellapragada
Srikar Yellapragada

Reputation: 21

How do I prove this in Lean? p ∨ ¬p

I have a theorem to prove on lean,

theorem T (h : ¬ A) : ¬ (A ∨ B) ∨ (¬ A ∧ B)

For which to prove, I guess, I need to use,

or.elim (B ∨ ¬B) (assume b: B, ...) (assume nb:¬B, ...)

For which, again, I have to prove

B v ¬B

So, how do I proceed with this? Is there any better method?

Upvotes: 2

Views: 283

Answers (2)

Kevin Buzzard
Kevin Buzzard

Reputation: 469

import tactic

variables (A B : Prop)

theorem T (h : ¬ A) : ¬ (A ∨ B) ∨ (¬ A ∧ B) := by tauto!

Upvotes: 0

Mario Carneiro
Mario Carneiro

Reputation: 1683

p v ¬p is a lemma from the core library called classical.em.

Upvotes: 2

Related Questions