Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ =ₛ L₂
Tactic:
apply System.Equiv.antisymm_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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ ≤ₛ L₂ ∧ L₂ ≤ₛ L₁

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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ ≤ₛ L₂ ∧ L₂ ≤ₛ L₁
Tactic:
constructor
State after:
case left
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ ≤ₛ L₂

case right
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₂ ≤ₛ L₁

State before:
case left
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ ≤ₛ L₂

case right
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₂ ≤ₛ L₁
Tactic:
. apply reducible_of_definability (definability₁ := definability₁) (definability₂ := definability₂); intros; exact h.mpr (by assumption)
State after:
case right
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₂ ≤ₛ L₁

State before:
case right
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₂ ≤ₛ L₁
Tactic:
. apply reducible_of_definability (definability₁ := definability₂) (definability₂ := definability₁); intros; exact h.mp (by assumption)
State after:
no goals

State before:
case left
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ ≤ₛ L₂
Tactic:
apply reducible_of_definability (definability₁ := definability₁) (definability₂ := definability₂)
State after:
case left
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ ∀ {F : Frame}, P₂ F → P₁ F

State before:
case left
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ ∀ {F : Frame}, P₂ F → P₁ F
Tactic:
intros
State after:
case left
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₂ F✝
⊢ P₁ F✝

State before:
case left
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₂ F✝
⊢ P₁ F✝
Tactic:
exact h.mpr (by assumption)
State after:
no goals

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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₂ F✝
⊢ P₂ F✝
Tactic:
assumption
State after:
no goals

State before:
case right
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₂ ≤ₛ L₁
Tactic:
apply reducible_of_definability (definability₁ := definability₂) (definability₂ := definability₁)
State after:
case right
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ ∀ {F : Frame}, P₁ F → P₂ F

State before:
case right
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ ∀ {F : Frame}, P₁ F → P₂ F
Tactic:
intros
State after:
case right
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₁ F✝
⊢ P₂ F✝

State before:
case right
α : 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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₁ F✝
⊢ P₂ F✝
Tactic:
exact h.mp (by assumption)
State after:
no goals

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₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₁ F✝
⊢ P₁ F✝
Tactic:
assumption
State after:
no goals