Theorem: mytaut2 (Bml/Examples.lean)

State before:
p : Char
⊢ Tautology ((~~·p)↣·p)
Tactic:
unfold Tautology Evaluate
State after:
p : Char
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    match (M, w), (~~·p)↣·p with
    | (fst, snd), Formula.bottom => False
    | (M, w), ·p => M.val w p
    | (M, w), ~φ => ¬Evaluate (M, w) φ
    | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
    | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ

State before:
p : Char
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    match (M, w), (~~·p)↣·p with
    | (fst, snd), Formula.bottom => False
    | (M, w), ·p => M.val w p
    | (M, w), ~φ => ¬Evaluate (M, w) φ
    | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
    | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ
Tactic:
intro W M w
State after:
p : Char
W : Type
M : KripkeModel W
w : W
⊢ match (M, w), (~~·p)↣·p with
  | (fst, snd), Formula.bottom => False
  | (M, w), ·p => M.val w p
  | (M, w), ~φ => ¬Evaluate (M, w) φ
  | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
  | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ

State before:
p : Char
W : Type
M : KripkeModel W
w : W
⊢ match (M, w), (~~·p)↣·p with
  | (fst, snd), Formula.bottom => False
  | (M, w), ·p => M.val w p
  | (M, w), ~φ => ¬Evaluate (M, w) φ
  | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
  | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ
Tactic:
classical
simp
State after:
no goals

State before:
p : Char
W : Type
M : KripkeModel W
w : W
⊢ match (M, w), (~~·p)↣·p with
  | (fst, snd), Formula.bottom => False
  | (M, w), ·p => M.val w p
  | (M, w), ~φ => ¬Evaluate (M, w) φ
  | (M, w), φ⋀ψ => Evaluate (M, w) φ ∧ Evaluate (M, w) ψ
  | (M, w), □φ => ∀ (v : W), M.Rel w v → Evaluate (M, v) φ
Tactic:
simp
State after:
no goals