Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive (Logic/Modal/Standard/Kripke/Morphism.lean)

State before:
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
⊢ ¬∃ Ax, ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
Tactic:
by_contra hC
State after:
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
hC : ∃ Ax, ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
⊢ False

State before:
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
hC : ∃ Ax, ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
⊢ False
Tactic:
obtain ⟨Ax, h⟩ := hC
State after:
case intro
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
⊢ False

State before:
case intro
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
⊢ False
Tactic:
let F₁ : Frame' α := { World := Unit ⊕ Unit, Rel := λ w v => w ≠ v }
State after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
⊢ False

State before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
⊢ False
Tactic:
have hIF₁ : Irreflexive F₁.Rel' := by exact f;
State after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
⊢ False

State before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
⊢ False
Tactic:
let F₂ : Frame' α := { World := Unit, Rel := λ w v => w = v }
State after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ False

State before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ False
Tactic:
have hIF₂ : ¬Irreflexive F₂.Rel' := by simp [Irreflexive]; existsi (); trivial;
State after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
⊢ False

State before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
⊢ False
Tactic:
let f : F₁.World → F₂.World := λ _ => ()
State after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
⊢ False

State before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
⊢ False
Tactic:
have hSur : Function.Surjective f := by simp [Function.Surjective];
State after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ False

State before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ False
Tactic:
have hMorF : Frame.pMorphism F₁ F₂ f := {
  forth := by aesop;
  back := by
    simp [F₁, F₂];
    constructor;
    . intro a; right; exists (); intro; contradiction;
    . intro a; left; use (); intro; contradiction;
}
State after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ False

State before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ False
Tactic:
have : Irreflexive F₂.Rel := h.mpr $ Theory.Kripke.ValidOnFrame.morphism hSur hMorF (h.mp hIF₁)
State after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
this : Irreflexive F₂.Rel
⊢ False

State before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
this : Irreflexive F₂.Rel
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
⊢ Irreflexive Frame.Rel'
Tactic:
exact f
State after:
no goals

State before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ ¬Irreflexive Frame.Rel'
Tactic:
simp [Irreflexive]
State after:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ ∃ x, x ≺ x

State before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ ∃ x, x ≺ x
Tactic:
existsi ()
State after:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ () ≺ ()

State before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ () ≺ ()
Tactic:
trivial
State after:
no goals

State before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
⊢ Function.Surjective f
Tactic:
simp [Function.Surjective]
State after:
no goals

State before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ {w v : F₁.World}, w ≺ v → f w ≺ f v
Tactic:
aesop
State after:
no goals

State before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ {w : F₁.World} {v : F₂.World}, f w ≺ v → ∃ u, w ≺ u ∧ f u = v
Tactic:
simp [F₁, F₂]
State after:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ (∀ (a : Unit), (∃ a_1, Sum.inl a ≺ Sum.inl a_1) ∨ ∃ b, Sum.inl a ≺ Sum.inr b) ∧
    ∀ (b : Unit), (∃ a, Sum.inr b ≺ Sum.inl a) ∨ ∃ b_1, Sum.inr b ≺ Sum.inr b_1

State before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ (∀ (a : Unit), (∃ a_1, Sum.inl a ≺ Sum.inl a_1) ∨ ∃ b, Sum.inl a ≺ Sum.inr b) ∧
    ∀ (b : Unit), (∃ a, Sum.inr b ≺ Sum.inl a) ∨ ∃ b_1, Sum.inr b ≺ Sum.inr b_1
Tactic:
constructor
State after:
case left
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ (a : Unit), (∃ a_1, Sum.inl a ≺ Sum.inl a_1) ∨ ∃ b, Sum.inl a ≺ Sum.inr b

case right
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ (b : Unit), (∃ a, Sum.inr b ≺ Sum.inl a) ∨ ∃ b_1, Sum.inr b ≺ Sum.inr b_1

State before:
case left
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ (a : Unit), (∃ a_1, Sum.inl a ≺ Sum.inl a_1) ∨ ∃ b, Sum.inl a ≺ Sum.inr b

case right
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ (b : Unit), (∃ a, Sum.inr b ≺ Sum.inl a) ∨ ∃ b_1, Sum.inr b ≺ Sum.inr b_1
Tactic:
. intro a; right; exists (); intro; contradiction;
State after:
case right
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ (b : Unit), (∃ a, Sum.inr b ≺ Sum.inl a) ∨ ∃ b_1, Sum.inr b ≺ Sum.inr b_1

State before:
case right
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ (b : Unit), (∃ a, Sum.inr b ≺ Sum.inl a) ∨ ∃ b_1, Sum.inr b ≺ Sum.inr b_1
Tactic:
. intro a; left; use (); intro; contradiction;
State after:
no goals

State before:
case left
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ (a : Unit), (∃ a_1, Sum.inl a ≺ Sum.inl a_1) ∨ ∃ b, Sum.inl a ≺ Sum.inr b
Tactic:
intro a
State after:
case left
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ (∃ a_1, Sum.inl a ≺ Sum.inl a_1) ∨ ∃ b, Sum.inl a ≺ Sum.inr b

State before:
case left
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ (∃ a_1, Sum.inl a ≺ Sum.inl a_1) ∨ ∃ b, Sum.inl a ≺ Sum.inr b
Tactic:
right
State after:
case left.h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ ∃ b, Sum.inl a ≺ Sum.inr b

State before:
case left.h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ ∃ b, Sum.inl a ≺ Sum.inr b
Tactic:
exists ()
State after:
case left.h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ Sum.inl a ≺ Sum.inr ()

State before:
case left.h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ Sum.inl a ≺ Sum.inr ()
Tactic:
intro
State after:
case left.h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
a✝ : Sum.inl a = Sum.inr ()
⊢ False

State before:
case left.h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
a✝ : Sum.inl a = Sum.inr ()
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case right
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ (b : Unit), (∃ a, Sum.inr b ≺ Sum.inl a) ∨ ∃ b_1, Sum.inr b ≺ Sum.inr b_1
Tactic:
intro a
State after:
case right
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ (∃ a_1, Sum.inr a ≺ Sum.inl a_1) ∨ ∃ b, Sum.inr a ≺ Sum.inr b

State before:
case right
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ (∃ a_1, Sum.inr a ≺ Sum.inl a_1) ∨ ∃ b, Sum.inr a ≺ Sum.inr b
Tactic:
left
State after:
case right.h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ ∃ a_1, Sum.inr a ≺ Sum.inl a_1

State before:
case right.h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ ∃ a_1, Sum.inr a ≺ Sum.inl a_1
Tactic:
use ()
State after:
case h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ Sum.inr a ≺ Sum.inl ()

State before:
case h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ Sum.inr a ≺ Sum.inl ()
Tactic:
intro
State after:
case h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
a✝ : Sum.inr a = Sum.inl ()
⊢ False

State before:
case h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
a✝ : Sum.inr a = Sum.inl ()
⊢ False
Tactic:
contradiction
State after:
no goals