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

Question

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?

user_890016 · Answer

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

user_6893027 · Answer

import tactic

variables (A B : Prop)

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