Theorem: LO.Modal.Standard.trivTranslated_of_K4 (Logic/Modal/Standard/Maximal.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! p → 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
Tactic:
intro h
State after:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒 ⊢! p
⊢ 𝐂𝐥 ⊢! (pᵀᴾ) ⋯

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒 ⊢! p
⊢ 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
Tactic:
apply iff_Triv_classical.mp
State after:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒 ⊢! p
⊢ 𝐓𝐫𝐢𝐯 ⊢! p

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒 ⊢! p
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
exact System.reducible_iff.mp reducible_K4_Triv h
State after:
no goals