Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.disj₃ (Logic/Propositional/Superintuitionistic/Kripke/Semantics.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ (p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r
Tactic:
simp_all only [ValidOnModel.iff_models, ValidOnModel, Satisfies.iff_models, Satisfies.imp_def, Satisfies.or_def]
State after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' →
      (∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 p → Satisfies M w'_1 r) →
        ∀ {w'_1 : M.Frame.World},
          w' ≺ w'_1 →
            (∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' q → Satisfies M w' r) →
              ∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' p ∨ Satisfies M w' q → Satisfies M w' r

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' →
      (∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 p → Satisfies M w'_1 r) →
        ∀ {w'_1 : M.Frame.World},
          w' ≺ w'_1 →
            (∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' q → Satisfies M w' r) →
              ∀ {w' : M.Frame.World}, w'_1 ≺ w' → Satisfies M w' p ∨ Satisfies M w' q → Satisfies M w' r
Tactic:
intro w₁ w₂ _ hpr w₃ hw₂₃ hqr w₄ hw₃₄ hpq
State after:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝ : w₁ ≺ w₂
hpr : ∀ {w' : M.Frame.World}, w₂ ≺ w' → Satisfies M w' p → Satisfies M w' r
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
hqr : ∀ {w' : M.Frame.World}, w₃ ≺ w' → Satisfies M w' q → Satisfies M w' r
w₄ : M.Frame.World
hw₃₄ : w₃ ≺ w₄
hpq : Satisfies M w₄ p ∨ Satisfies M w₄ q
⊢ Satisfies M w₄ r

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝ : w₁ ≺ w₂
hpr : ∀ {w' : M.Frame.World}, w₂ ≺ w' → Satisfies M w' p → Satisfies M w' r
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
hqr : ∀ {w' : M.Frame.World}, w₃ ≺ w' → Satisfies M w' q → Satisfies M w' r
w₄ : M.Frame.World
hw₃₄ : w₃ ≺ w₄
hpq : Satisfies M w₄ p ∨ Satisfies M w₄ q
⊢ Satisfies M w₄ r
Tactic:
cases hpq with
| inl hp => exact hpr (M.Frame.Rel_trans hw₂₃ hw₃₄) hp;
| inr hq => exact hqr hw₃₄ hq;
State after:
no goals

State before:
case inl
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝ : w₁ ≺ w₂
hpr : ∀ {w' : M.Frame.World}, w₂ ≺ w' → Satisfies M w' p → Satisfies M w' r
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
hqr : ∀ {w' : M.Frame.World}, w₃ ≺ w' → Satisfies M w' q → Satisfies M w' r
w₄ : M.Frame.World
hw₃₄ : w₃ ≺ w₄
hp : Satisfies M w₄ p
⊢ Satisfies M w₄ r
Tactic:
exact hpr (M.Frame.Rel_trans hw₂₃ hw₃₄) hp
State after:
no goals

State before:
case inr
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝ : w₁ ≺ w₂
hpr : ∀ {w' : M.Frame.World}, w₂ ≺ w' → Satisfies M w' p → Satisfies M w' r
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
hqr : ∀ {w' : M.Frame.World}, w₃ ≺ w' → Satisfies M w' q → Satisfies M w' r
w₄ : M.Frame.World
hw₃₄ : w₃ ≺ w₄
hq : Satisfies M w₄ q
⊢ Satisfies M w₄ r
Tactic:
exact hqr hw₃₄ hq
State after:
no goals