Theorem: LO.Modal.Standard.dp_of_mdp (Logic/Modal/Standard/Kripke/ModalCompanion.lean)

State before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
⊢ i𝓓 ⊢! p ⋎ q → i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Tactic:
intro hpq
State after:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q

State before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Tactic:
have : m𝓓 ⊢! □pᵍ ⋎ □qᵍ := disj₃'! (implyOrLeft'! axiomTc_GTranslate!) (implyOrRight'! axiomTc_GTranslate!) (by simpa using ModalCompanion.companion.mp hpq)
State after:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q

State before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Tactic:
cases ModalDisjunctive.modal_disjunctive this with
| inl h => left; exact ModalCompanion.companion.mpr h;
| inr h => right; exact ModalCompanion.companion.mpr h;
State after:
no goals

State before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
⊢ m𝓓 ⊢! pᵍ ⋎ qᵍ
Tactic:
simpa using ModalCompanion.companion.mp hpq
State after:
no goals

State before:
case inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! pᵍ
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Tactic:
left
State after:
case inl.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! pᵍ
⊢ i𝓓 ⊢! p

State before:
case inl.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! pᵍ
⊢ i𝓓 ⊢! p
Tactic:
exact ModalCompanion.companion.mpr h
State after:
no goals

State before:
case inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! qᵍ
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Tactic:
right
State after:
case inr.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! qᵍ
⊢ i𝓓 ⊢! q

State before:
case inr.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! qᵍ
⊢ i𝓓 ⊢! q
Tactic:
exact ModalCompanion.companion.mpr h
State after:
no goals