Theorem: easy (LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean)

State before:
P Q R S : Prop
⊢ P → P
Tactic:
intro h
State after:
P Q R S : Prop
h : P
⊢ P

State before:
P Q R S : Prop
h : P
⊢ P
Tactic:
apply h
State after:
no goals