Theorem: LO.Modal.Standard.Kripke.reducible_of_subset_axiomSetFrameClass (Logic/Modal/Standard/Kripke/Reducible.lean)

State before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
⊢ L₁ ≤ₛ L₂
Tactic:
apply System.reducible_iff.mpr
State after:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
⊢ ∀ {f : Formula α}, L₁ ⊢! f → L₂ ⊢! f

State before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
⊢ ∀ {f : Formula α}, L₁ ⊢! f → L₂ ⊢! f
Tactic:
intro p hp
State after:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
⊢ L₂ ⊢! p

State before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
⊢ L₂ ⊢! p
Tactic:
apply complete₂.complete
State after:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
⊢ 𝔽(Ax(L₂)) ⊧ p

State before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
⊢ 𝔽(Ax(L₂)) ⊧ p
Tactic:
intro F hF
State after:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
F : Frame' α
hF : F ∈ 𝔽(Ax(L₂))
⊢ F ⊧ p

State before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
F : Frame' α
hF : F ∈ 𝔽(Ax(L₂))
⊢ F ⊧ p
Tactic:
exact sound₁.sound hp F $ hs hF
State after:
no goals