Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.formula_hereditary (Logic/Propositional/Superintuitionistic/Kripke/Semantics.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
p : Formula α
hw : w ≺ w'
⊢ Satisfies M w p → Satisfies M w' p
Tactic:
induction p using Formula.rec' with
| hatom => apply M.hereditary hw;
| himp =>
  simp_all [Satisfies];
  intro hpq v hv;
  exact hpq $ M.Frame.Rel_trans hw hv;
| hor => simp_all [Satisfies]; tauto;
| _ => simp_all [Satisfies];
State after:
no goals

State before:
case hatom
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
a✝ : α
⊢ Satisfies M w (atom a✝) → Satisfies M w' (atom a✝)
Tactic:
apply M.hereditary hw
State after:
no goals

State before:
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w (p✝ ⟶ q✝) → Satisfies M w' (p✝ ⟶ q✝)
Tactic:
simp_all [Satisfies]
State after:
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ (∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p✝ ∨ Satisfies M w' q✝) →
    ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → ¬Satisfies M w'_1 p✝ ∨ Satisfies M w'_1 q✝

State before:
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ (∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p✝ ∨ Satisfies M w' q✝) →
    ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → ¬Satisfies M w'_1 p✝ ∨ Satisfies M w'_1 q✝
Tactic:
intro hpq v hv
State after:
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
hpq : ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p✝ ∨ Satisfies M w' q✝
v : M.Frame.World
hv : w' ≺ v
⊢ ¬Satisfies M v p✝ ∨ Satisfies M v q✝

State before:
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
hpq : ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p✝ ∨ Satisfies M w' q✝
v : M.Frame.World
hv : w' ≺ v
⊢ ¬Satisfies M v p✝ ∨ Satisfies M v q✝
Tactic:
exact hpq $ M.Frame.Rel_trans hw hv
State after:
no goals

State before:
case hor
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w (p✝ ⋎ q✝) → Satisfies M w' (p✝ ⋎ q✝)
Tactic:
simp_all [Satisfies]
State after:
case hor
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w p✝ ∨ Satisfies M w q✝ → Satisfies M w' p✝ ∨ Satisfies M w' q✝

State before:
case hor
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w p✝ ∨ Satisfies M w q✝ → Satisfies M w' p✝ ∨ Satisfies M w' q✝
Tactic:
tauto
State after:
no goals

State before:
case hand
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w (p✝ ⋏ q✝) → Satisfies M w' (p✝ ⋏ q✝)
Tactic:
simp_all [Satisfies]
State after:
no goals