Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_disj₃ (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✝ : K4 m𝓓
⊢ m𝓓 ⊢! ((p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r)ᵍ
Tactic:
simp only [GoedelTranslation.imp_def, GoedelTranslation.or_def]
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! □(□(pᵍ ⟶ rᵍ) ⟶ □(□(qᵍ ⟶ rᵍ) ⟶ □(pᵍ ⋎ qᵍ ⟶ rᵍ)))

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! □(□(pᵍ ⟶ rᵍ) ⟶ □(□(qᵍ ⟶ rᵍ) ⟶ □(pᵍ ⋎ qᵍ ⟶ rᵍ)))
Tactic:
exact nec! $ imp_trans! axiomFour! $ axiomK'! $ nec! $ imp_trans! (axiomK'! $ nec! $ disj₃!) axiomK!
State after:
no goals