Theorem: LO.Modal.Standard.provable_S4_of_provable_efq (Logic/Modal/Standard/Kripke/ModalCompanion.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
⊢ 𝐒𝟒 ⊢! pᵍ → 𝐈𝐧𝐭 ⊢! p
Tactic:
contrapose
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
⊢ ¬𝐈𝐧𝐭 ⊢! p → ¬𝐒𝟒 ⊢! pᵍ

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
⊢ ¬𝐈𝐧𝐭 ⊢! p → ¬𝐒𝟒 ⊢! pᵍ
Tactic:
intro h
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h : ¬𝐈𝐧𝐭 ⊢! p
⊢ ¬𝐒𝟒 ⊢! pᵍ

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h : ¬𝐈𝐧𝐭 ⊢! p
⊢ ¬𝐒𝟒 ⊢! pᵍ
Tactic:
obtain ⟨iF, _, iV, iV_hereditary, w, h⟩ := by simpa [ValidOnFrameClass, ValidOnFrame, ValidOnModel] using not_imp_not.mpr Superintuitionistic.Kripke.complete! h;
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
⊢ ¬𝐒𝟒 ⊢! pᵍ

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
⊢ ¬𝐒𝟒 ⊢! pᵍ
Tactic:
let M : Modal.Standard.Kripke.Model α := { Frame := { Rel := iF.Rel }, Valuation := iV }
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
⊢ ¬𝐒𝟒 ⊢! pᵍ

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
⊢ ¬𝐒𝟒 ⊢! pᵍ
Tactic:
have h₁ : ∀ q v, Satisfies ⟨iF, iV, iV_hereditary⟩ v q ↔ (Modal.Standard.Formula.Kripke.Satisfies M v (qᵍ)) := by
  intro q v;
  induction q using Superintuitionistic.Formula.rec' generalizing v with
  | hatom a =>
    constructor;
    . intro _ _ h;
      simp_all only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies];
      exact iV_hereditary h (by assumption);
    . intro h;
      simpa only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies] using h v $ iF.Rel_refl v;
  | _ => simp_all;
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
⊢ ¬𝐒𝟒 ⊢! pᵍ

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
⊢ ¬𝐒𝟒 ⊢! pᵍ
Tactic:
have : ¬(Modal.Standard.Formula.Kripke.Satisfies M w (pᵍ)) := (h₁ p w).not.mp h
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ¬𝐒𝟒 ⊢! pᵍ

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ¬𝐒𝟒 ⊢! pᵍ
Tactic:
apply not_imp_not.mpr $ Modal.Standard.Kripke.sound!_on_frameclass
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ¬𝔽(Ax(𝐒𝟒)) ⊧ pᵍ

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ¬𝔽(Ax(𝐒𝟒)) ⊧ pᵍ
Tactic:
simp [Formula.Kripke.ValidOnFrame, Formula.Kripke.ValidOnModel]
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ∃ x ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰), ∃ x_1 x_2, ¬Formula.Kripke.Satisfies { Frame := x, Valuation := x_1 } x_2 (pᵍ)

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ∃ x ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰), ∃ x_1 x_2, ¬Formula.Kripke.Satisfies { Frame := x, Valuation := x_1 } x_2 (pᵍ)
Tactic:
existsi M.Frame
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ M.Frame ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰) ∧ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ M.Frame ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰) ∧ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ M.Frame ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰)

case intro.intro.intro.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)

State before:
case intro.intro.intro.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ M.Frame ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰)

case intro.intro.intro.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)
Tactic:
. apply Modal.Standard.Kripke.iff_definability_memAxiomSetFrameClass
    (show Kripke.Definability _ (λ F => Reflexive F.Rel ∧ Transitive F.Rel) by simpa using instGeachDefinability (L := 𝐒𝟒))
    |>.mpr;
  constructor;
  . exact iF.Rel_refl;
  . exact iF.Rel_trans;
State after:
case intro.intro.intro.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)

State before:
case intro.intro.intro.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)
Tactic:
. use M.Valuation, w;
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h : ¬𝐈𝐧𝐭 ⊢! p
⊢ ?m.89406
Tactic:
simpa [ValidOnFrameClass, ValidOnFrame, ValidOnModel] using not_imp_not.mpr Superintuitionistic.Kripke.complete! h
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
⊢ ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
Tactic:
intro q v
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q✝ r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
q : Superintuitionistic.Formula α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q✝ r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
q : Superintuitionistic.Formula α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
Tactic:
induction q using Superintuitionistic.Formula.rec' generalizing v with
| hatom a =>
  constructor;
  . intro _ _ h;
    simp_all only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies];
    exact iV_hereditary h (by assumption);
  . intro h;
    simpa only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies] using h v $ iF.Rel_refl v;
| _ => simp_all;
State after:
no goals

State before:
case hatom
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a) ↔
    Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ)
Tactic:
constructor
State after:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a) →
    Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ)

case hatom.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ) →
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)

State before:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a) →
    Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ)

case hatom.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ) →
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
Tactic:
. intro _ _ h;
  simp_all only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies];
  exact iV_hereditary h (by assumption);
State after:
case hatom.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ) →
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)

State before:
case hatom.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ) →
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
Tactic:
. intro h;
  simpa only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies] using h v $ iF.Rel_refl v;
State after:
no goals

State before:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a) →
    Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ)
Tactic:
intro _ _ h
State after:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
a✝ : Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
w'✝ : M.Frame.World
h : v ≺ w'✝
⊢ Formula.Kripke.Satisfies M w'✝ (Formula.atom a)

State before:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
a✝ : Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
w'✝ : M.Frame.World
h : v ≺ w'✝
⊢ Formula.Kripke.Satisfies M w'✝ (Formula.atom a)
Tactic:
simp_all only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies]
State after:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
w'✝ : M.Frame.World
a✝ : iV v a
h : v ≺ w'✝
⊢ iV w'✝ a

State before:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
w'✝ : M.Frame.World
a✝ : iV v a
h : v ≺ w'✝
⊢ iV w'✝ a
Tactic:
exact iV_hereditary h (by assumption)
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
w'✝ : M.Frame.World
a✝ : iV v a
h : v ≺ w'✝
⊢ iV v a
Tactic:
assumption
State after:
no goals

State before:
case hatom.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ) →
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
Tactic:
intro h
State after:
case hatom.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ)
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)

State before:
case hatom.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ)
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
Tactic:
simpa only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies] using h v $ iF.Rel_refl v
State after:
no goals

State before:
case hor
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
p✝ q✝ : Superintuitionistic.Formula α
a✝¹ :
  ∀ (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v p✝ ↔ Formula.Kripke.Satisfies M v (p✝ᵍ)
a✝ :
  ∀ (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q✝ ↔ Formula.Kripke.Satisfies M v (q✝ᵍ)
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (p✝ ⋎ q✝) ↔ Formula.Kripke.Satisfies M v ((p✝ ⋎ q✝)ᵍ)
Tactic:
simp_all
State after:
no goals

State before:
case intro.intro.intro.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ M.Frame ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰)
Tactic:
apply Modal.Standard.Kripke.iff_definability_memAxiomSetFrameClass
  (show Kripke.Definability _ (λ F => Reflexive F.Rel ∧ Transitive F.Rel) by simpa using instGeachDefinability (L := 𝐒𝟒))
  |>.mpr
State after:
case intro.intro.intro.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Reflexive M.Frame.Rel ∧ Transitive M.Frame.Rel

State before:
case intro.intro.intro.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Reflexive M.Frame.Rel ∧ Transitive M.Frame.Rel
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.left.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Reflexive M.Frame.Rel

case intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Transitive M.Frame.Rel

State before:
case intro.intro.intro.intro.intro.left.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Reflexive M.Frame.Rel

case intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Transitive M.Frame.Rel
Tactic:
. exact iF.Rel_refl;
State after:
case intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Transitive M.Frame.Rel

State before:
case intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Transitive M.Frame.Rel
Tactic:
. exact iF.Rel_trans;
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Kripke.Definability (𝗞 ∪ 𝗧 ∪ 𝟰) fun F => Reflexive F.Rel ∧ Transitive F.Rel
Tactic:
simpa using instGeachDefinability (L := 𝐒𝟒)
State after:
no goals

State before:
case intro.intro.intro.intro.intro.left.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Reflexive M.Frame.Rel
Tactic:
exact iF.Rel_refl
State after:
no goals

State before:
case intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Transitive M.Frame.Rel
Tactic:
exact iF.Rel_trans
State after:
no goals

State before:
case intro.intro.intro.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)
Tactic:
use M.Valuation, w
State after:
no goals