internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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;
Proof 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
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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 ()
Proof 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 ()
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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 ()
Proof 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 ()
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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
Proof 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
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.and_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy Γ s (p ⋏ q) → Hierarchy Γ s p ∧ Hierarchy Γ s q
Tactic:
generalize hr : p ⋏ q = r
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋏ q = r
⊢ Hierarchy Γ s r → Hierarchy Γ s p ∧ Hierarchy Γ s q
Theorem: LO.FirstOrder.Arith.Hierarchy.and_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋏ q = r
⊢ Hierarchy Γ s r → Hierarchy Γ s p ∧ Hierarchy Γ s q
Tactic:
intro H
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋏ q = r
H : Hierarchy Γ s r
⊢ Hierarchy Γ s p ∧ Hierarchy Γ s q
Theorem: LO.FirstOrder.Arith.Hierarchy.and_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋏ q = r
H : Hierarchy Γ s r
⊢ Hierarchy Γ s p ∧ Hierarchy Γ s q
Tactic:
induction H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hr
Proof state after:
case and
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {p q : Semiformula L μ n✝}, p ⋏ q = p✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q : Semiformula L μ n✝}, p ⋏ q = q✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
p q : Semiformula L μ n✝
hr : p = p✝ ∧ q = q✝
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Theorem: LO.FirstOrder.Arith.Hierarchy.and_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {p q : Semiformula L μ n✝}, p ⋏ q = p✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q : Semiformula L μ n✝}, p ⋏ q = q✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
p q : Semiformula L μ n✝
hr : p = p✝ ∧ q = q✝
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Tactic:
case and =>
  rcases hr with ⟨rfl, rfl⟩
  constructor <;> assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.and_iff
Proof state before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {p q : Semiformula L μ (n✝ + 1)}, p ⋏ q = p✝ → Hierarchy 𝚺 (s✝ + 1) p ∧ Hierarchy 𝚺 (s✝ + 1) q
p q : Semiformula L μ n✝
hr : p ⋏ q = ∃' p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p ∧ Hierarchy 𝚷 (s✝ + 1 + 1) q
Tactic:
simp [LogicalConnective.ball, LogicalConnective.bex] at hr
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.and_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {p q : Semiformula L μ n✝}, p ⋏ q = p✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q : Semiformula L μ n✝}, p ⋏ q = q✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
p q : Semiformula L μ n✝
hr : p = p✝ ∧ q = q✝
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Tactic:
rcases hr with ⟨rfl, rfl⟩
Proof state after:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p q : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p
a_ih✝¹ : ∀ {p_1 q : Semiformula L μ n✝}, p_1 ⋏ q = p → Hierarchy Γ✝ s✝ p_1 ∧ Hierarchy Γ✝ s✝ q
a✝ : Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q_1 : Semiformula L μ n✝}, p ⋏ q_1 = q → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q_1
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Theorem: LO.FirstOrder.Arith.Hierarchy.and_iff
Proof state before:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p q : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p
a_ih✝¹ : ∀ {p_1 q : Semiformula L μ n✝}, p_1 ⋏ q = p → Hierarchy Γ✝ s✝ p_1 ∧ Hierarchy Γ✝ s✝ q
a✝ : Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q_1 : Semiformula L μ n✝}, p ⋏ q_1 = q → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q_1
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.and_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy Γ s p ∧ Hierarchy Γ s q → Hierarchy Γ s (p ⋏ q)
Tactic:
rintro ⟨hp, hq⟩
Proof state after:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
hp : Hierarchy Γ s p
hq : Hierarchy Γ s q
⊢ Hierarchy Γ s (p ⋏ q)
Theorem: LO.FirstOrder.Arith.Hierarchy.and_iff
Proof state before:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
hp : Hierarchy Γ s p
hq : Hierarchy Γ s q
⊢ Hierarchy Γ s (p ⋏ q)
Tactic:
exact Hierarchy.and hp hq
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.or_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy Γ s (p ⋎ q) → Hierarchy Γ s p ∧ Hierarchy Γ s q
Tactic:
generalize hr : p ⋎ q = r
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋎ q = r
⊢ Hierarchy Γ s r → Hierarchy Γ s p ∧ Hierarchy Γ s q
Theorem: LO.FirstOrder.Arith.Hierarchy.or_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋎ q = r
⊢ Hierarchy Γ s r → Hierarchy Γ s p ∧ Hierarchy Γ s q
Tactic:
intro H
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋎ q = r
H : Hierarchy Γ s r
⊢ Hierarchy Γ s p ∧ Hierarchy Γ s q
Theorem: LO.FirstOrder.Arith.Hierarchy.or_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋎ q = r
H : Hierarchy Γ s r
⊢ Hierarchy Γ s p ∧ Hierarchy Γ s q
Tactic:
induction H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hr
Proof state after:
case or
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = p✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = q✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
p q : Semiformula L μ n✝
hr : p = p✝ ∧ q = q✝
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Theorem: LO.FirstOrder.Arith.Hierarchy.or_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = p✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = q✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
p q : Semiformula L μ n✝
hr : p = p✝ ∧ q = q✝
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Tactic:
case or =>
  rcases hr with ⟨rfl, rfl⟩
  constructor <;> assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.or_iff
Proof state before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {p q : Semiformula L μ (n✝ + 1)}, p ⋎ q = p✝ → Hierarchy 𝚺 (s✝ + 1) p ∧ Hierarchy 𝚺 (s✝ + 1) q
p q : Semiformula L μ n✝
hr : p ⋎ q = ∃' p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p ∧ Hierarchy 𝚷 (s✝ + 1 + 1) q
Tactic:
simp [LogicalConnective.ball, LogicalConnective.bex] at hr
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.or_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = p✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = q✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
p q : Semiformula L μ n✝
hr : p = p✝ ∧ q = q✝
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Tactic:
rcases hr with ⟨rfl, rfl⟩
Proof state after:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p q : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p
a_ih✝¹ : ∀ {p_1 q : Semiformula L μ n✝}, p_1 ⋎ q = p → Hierarchy Γ✝ s✝ p_1 ∧ Hierarchy Γ✝ s✝ q
a✝ : Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q_1 : Semiformula L μ n✝}, p ⋎ q_1 = q → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q_1
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q