Theorem: LO.Modal.Standard.reducible_K4Henkin_GL (Logic/Modal/Standard/Deduction.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒𝐇 ≤ₛ 𝐆𝐋
Tactic:
apply normal_reducible
State after:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {p : Formula α}, p ∈ Ax(𝐊𝟒𝐇) → 𝐆𝐋 ⊢! p

State before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {p : Formula α}, p ∈ Ax(𝐊𝟒𝐇) → 𝐆𝐋 ⊢! p
Tactic:
intro p hp
State after:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hp : p ∈ Ax(𝐊𝟒𝐇)
⊢ 𝐆𝐋 ⊢! p

State before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hp : p ∈ Ax(𝐊𝟒𝐇)
⊢ 𝐆𝐋 ⊢! p
Tactic:
rcases hp with (hK | hFour) | hH
State after:
case hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p

State before:
case hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
State after:
case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p

State before:
case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
Tactic:
. obtain ⟨_, _, e⟩ := hFour; subst_vars; exact axiomFour!;
State after:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p

State before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
Tactic:
. obtain ⟨_, _, e⟩ := hH; subst_vars; exact axiomH!;
State after:
no goals

State before:
case hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐆𝐋 ⊢! p
Tactic:
obtain ⟨_, _, e⟩ := hK
State after:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p
⊢ 𝐆𝐋 ⊢! p

State before:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p
⊢ 𝐆𝐋 ⊢! p
Tactic:
subst_vars
State after:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
w✝¹ w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝

State before:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
w✝¹ w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
Tactic:
exact axiomK!
State after:
no goals

State before:
case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p
Tactic:
obtain ⟨_, _, e⟩ := hFour
State after:
case hMaxm.inl.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.Four w✝

State before:
case hMaxm.inl.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.Four w✝
Tactic:
exact axiomFour!
State after:
no goals

State before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p
Tactic:
obtain ⟨_, _, e⟩ := hH
State after:
case hMaxm.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.H w✝

State before:
case hMaxm.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.H w✝
Tactic:
exact axiomH!
State after:
no goals