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