Theorem: LO.Modal.Standard.Kripke.reducible_of_definability (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}, P₂ F → P₁ F
⊢ L₁ ≤ₛ L₂
Tactic:
apply reducible_of_subset_axiomSetFrameClass
State after:
case hs
α : 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}, P₂ F → P₁ F
⊢ ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))

State before:
case hs
α : 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}, P₂ F → P₁ F
⊢ ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
Tactic:
intro F hF
State after:
case hs
α : 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}, P₂ F → P₁ F
F : Frame
hF : F ∈ 𝔽(Ax(L₂))
⊢ F ∈ 𝔽(Ax(L₁))

State before:
case hs
α : 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}, P₂ F → P₁ F
F : Frame
hF : F ∈ 𝔽(Ax(L₂))
⊢ F ∈ 𝔽(Ax(L₁))
Tactic:
apply iff_definability_memAxiomSetFrameClass definability₁ |>.mpr
State after:
case hs
α : 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}, P₂ F → P₁ F
F : Frame
hF : F ∈ 𝔽(Ax(L₂))
⊢ P₁ F

State before:
case hs
α : 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}, P₂ F → P₁ F
F : Frame
hF : F ∈ 𝔽(Ax(L₂))
⊢ P₁ F
Tactic:
exact hs $ iff_definability_memAxiomSetFrameClass definability₂ |>.mp hF
State after:
no goals