Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.equality_def (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁ = Ω₂ ↔ Ω₁.theory = Ω₂.theory
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁ = Ω₂ → Ω₁.theory = Ω₂.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₂.theory → Ω₁ = Ω₂

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁ = Ω₂ → Ω₁.theory = Ω₂.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₂.theory → Ω₁ = Ω₂
Tactic:
. intro h; cases h; rfl;
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₂.theory → Ω₁ = Ω₂

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₂.theory → Ω₁ = Ω₂
Tactic:
. intro h; cases Ω₁; cases Ω₂; simp_all;
State after:
no goals

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁ = Ω₂ → Ω₁.theory = Ω₂.theory
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω₁ = Ω₂
⊢ Ω₁.theory = Ω₂.theory

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω₁ = Ω₂
⊢ Ω₁.theory = Ω₂.theory
Tactic:
cases h
State after:
case mp.refl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₁.theory

State before:
case mp.refl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₁.theory
Tactic:
rfl
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₂.theory → Ω₁ = Ω₂
Tactic:
intro h
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω₁.theory = Ω₂.theory
⊢ Ω₁ = Ω₂

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω₁.theory = Ω₂.theory
⊢ Ω₁ = Ω₂
Tactic:
cases Ω₁
State after:
case mpr.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₂ : MCT L
p : Formula α
theory✝ : Theory α
consistent✝ : (L)-Consistent theory✝
maximal✝ : ∀ {U : Theory α}, theory✝ ⊂ U → ¬(L)-Consistent U
h : { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }.theory = Ω₂.theory
⊢ { theory := theory✝, consistent := consistent✝, maximal := maximal✝ } = Ω₂

State before:
case mpr.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₂ : MCT L
p : Formula α
theory✝ : Theory α
consistent✝ : (L)-Consistent theory✝
maximal✝ : ∀ {U : Theory α}, theory✝ ⊂ U → ¬(L)-Consistent U
h : { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }.theory = Ω₂.theory
⊢ { theory := theory✝, consistent := consistent✝, maximal := maximal✝ } = Ω₂
Tactic:
cases Ω₂
State after:
case mpr.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω : MCT L
p : Formula α
theory✝¹ : Theory α
consistent✝¹ : (L)-Consistent theory✝¹
maximal✝¹ : ∀ {U : Theory α}, theory✝¹ ⊂ U → ¬(L)-Consistent U
theory✝ : Theory α
consistent✝ : (L)-Consistent theory✝
maximal✝ : ∀ {U : Theory α}, theory✝ ⊂ U → ¬(L)-Consistent U
h :
  { theory := theory✝¹, consistent := consistent✝¹, maximal := maximal✝¹ }.theory =
    { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }.theory
⊢ { theory := theory✝¹, consistent := consistent✝¹, maximal := maximal✝¹ } =
    { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }

State before:
case mpr.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω : MCT L
p : Formula α
theory✝¹ : Theory α
consistent✝¹ : (L)-Consistent theory✝¹
maximal✝¹ : ∀ {U : Theory α}, theory✝¹ ⊂ U → ¬(L)-Consistent U
theory✝ : Theory α
consistent✝ : (L)-Consistent theory✝
maximal✝ : ∀ {U : Theory α}, theory✝ ⊂ U → ¬(L)-Consistent U
h :
  { theory := theory✝¹, consistent := consistent✝¹, maximal := maximal✝¹ }.theory =
    { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }.theory
⊢ { theory := theory✝¹, consistent := consistent✝¹, maximal := maximal✝¹ } =
    { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }
Tactic:
simp_all
State after:
no goals