Theorem: exercise3_1 (LeanCourse/Assignments/Solutions/Solutions3.lean)

State before:
p : Prop
⊢ p ∨ ¬p
Tactic:
by_contra h
State after:
p : Prop
h : ¬(p ∨ ¬p)
⊢ False

State before:
p : Prop
h : ¬(p ∨ ¬p)
⊢ False
Tactic:
apply h
State after:
p : Prop
h : ¬(p ∨ ¬p)
⊢ p ∨ ¬p

State before:
p : Prop
h : ¬(p ∨ ¬p)
⊢ p ∨ ¬p
Tactic:
right
State after:
case h
p : Prop
h : ¬(p ∨ ¬p)
⊢ ¬p

State before:
case h
p : Prop
h : ¬(p ∨ ¬p)
⊢ ¬p
Tactic:
intro h2
State after:
case h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ False

State before:
case h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ False
Tactic:
apply h
State after:
case h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ p ∨ ¬p

State before:
case h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ p ∨ ¬p
Tactic:
left
State after:
case h.h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ p

State before:
case h.h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ p
Tactic:
assumption
State after:
no goals