internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
case left
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ ≤ₛ L₂

case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₂ ≤ₛ L₁
Tactic:
. apply reducible_of_definability (definability₁ := definability₁) (definability₂ := definability₂); intros; exact h.mpr (by assumption)
Proof state after:
case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₂ ≤ₛ L₁
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₂ ≤ₛ L₁
Tactic:
. apply reducible_of_definability (definability₁ := definability₂) (definability₂ := definability₁); intros; exact h.mp (by assumption)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
case left
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ ≤ₛ L₂
Tactic:
apply reducible_of_definability (definability₁ := definability₁) (definability₂ := definability₂)
Proof state after:
case left
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ ∀ {F : Frame}, P₂ F → P₁ F
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
case left
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ ∀ {F : Frame}, P₂ F → P₁ F
Tactic:
intros
Proof state after:
case left
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₂ F✝
⊢ P₁ F✝
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
case left
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₂ F✝
⊢ P₁ F✝
Tactic:
exact h.mpr (by assumption)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₂ F✝
⊢ P₂ F✝
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₂ ≤ₛ L₁
Tactic:
apply reducible_of_definability (definability₁ := definability₂) (definability₂ := definability₁)
Proof state after:
case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ ∀ {F : Frame}, P₁ F → P₂ F
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ ∀ {F : Frame}, P₁ F → P₂ F
Tactic:
intros
Proof state after:
case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₁ F✝
⊢ P₂ F✝
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₁ F✝
⊢ P₂ F✝
Tactic:
exact h.mp (by assumption)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
F✝ : Frame
a✝ : P₁ F✝
⊢ P₁ F✝
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.shifts_cons
Proof state before:
L : Language
n : ℕ
p : SyntacticSemiformula L n
Δ : List (SyntacticSemiformula L n)
⊢ (p :: Δ)⁺ = (Rew.hom ⇑) p :: Δ⁺
Tactic:
simp[shifts]
Proof state after:
no goals
Theorem: LO.FirstOrder.shifts_union
Proof state before:
L : Language
n : ℕ
Δ Γ : List (SyntacticSemiformula L n)
⊢ (Δ ++ Γ)⁺ = Δ⁺ ++ Γ⁺
Tactic:
simp[shifts]
Proof state after:
no goals
Theorem: LO.FirstOrder.shifts_emb
Proof state before:
L : Language
n : ℕ
Γ : List (Semisentence L n)
⊢ (List.map (⇑Rew.emb.hom) Γ)⁺ = List.map (⇑Rew.emb.hom) Γ
Tactic:
simp[shifts, Function.comp, ←Rew.hom_comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.or'
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
d :  ⊢¹ p :: q :: Δ
⊢ CutRestricted C (Derivation.or d) → CutRestricted C d
Tactic:
rintro ⟨⟩
Proof state after:
case or
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
d :  ⊢¹ p :: q :: Δ✝
Δ : Sequent L
a✝ : CutRestricted C d
⊢ CutRestricted C d
Theorem: LO.FirstOrder.Derivation.CutRestricted.or'
Proof state before:
case or
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
d :  ⊢¹ p :: q :: Δ✝
Δ : Sequent L
a✝ : CutRestricted C d
⊢ CutRestricted C d
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.and'
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ
dq :  ⊢¹ q :: Δ
⊢ CutRestricted C (Derivation.and dp dq) → CutRestricted C dp ∧ CutRestricted C dq
Tactic:
rintro ⟨⟩
Proof state after:
case and
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dq :  ⊢¹ q :: Δ✝
Δ : Sequent L
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dq
⊢ CutRestricted C dp ∧ CutRestricted C dq
Theorem: LO.FirstOrder.Derivation.CutRestricted.and'
Proof state before:
case and
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dq :  ⊢¹ q :: Δ✝
Δ : Sequent L
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dq
⊢ CutRestricted C dp ∧ CutRestricted C dq
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.and'
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ
dq :  ⊢¹ q :: Δ
⊢ CutRestricted C dp ∧ CutRestricted C dq → CutRestricted C (Derivation.and dp dq)
Tactic:
rintro ⟨dp, dq⟩
Proof state after:
case intro
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp✝ :  ⊢¹ p :: Δ
dq✝ :  ⊢¹ q :: Δ
dp : CutRestricted C dp✝
dq : CutRestricted C dq✝
⊢ CutRestricted C (Derivation.and dp✝ dq✝)
Theorem: LO.FirstOrder.Derivation.CutRestricted.and'
Proof state before:
case intro
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp✝ :  ⊢¹ p :: Δ
dq✝ :  ⊢¹ q :: Δ
dp : CutRestricted C dp✝
dq : CutRestricted C dq✝
⊢ CutRestricted C (Derivation.and dp✝ dq✝)
Tactic:
exact CutRestricted.and dp dq
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.all'
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p✝ q : SyntacticFormula L
p : Semiformula L ℕ (0 + 1)
d :  ⊢¹ (Rew.hom Rew.free) p :: Δ⁺
⊢ CutRestricted C (Derivation.all d) → CutRestricted C d
Tactic:
rintro ⟨⟩
Proof state after:
case all
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p✝ q : SyntacticFormula L
p : Semiformula L ℕ (0 + 1)
d :  ⊢¹ (Rew.hom Rew.free) p :: Δ✝⁺
Δ : Sequent L
a✝ : CutRestricted C d
⊢ CutRestricted C d
Theorem: LO.FirstOrder.Derivation.CutRestricted.all'
Proof state before:
case all
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p✝ q : SyntacticFormula L
p : Semiformula L ℕ (0 + 1)
d :  ⊢¹ (Rew.hom Rew.free) p :: Δ✝⁺
Δ : Sequent L
a✝ : CutRestricted C d
⊢ CutRestricted C d
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.ex'
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p✝ q : SyntacticFormula L
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d :  ⊢¹ [→ t].hom p :: Δ
⊢ CutRestricted C (Derivation.ex t d) → CutRestricted C d
Tactic:
rintro ⟨⟩
Proof state after:
case ex
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p✝ q : SyntacticFormula L
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d :  ⊢¹ [→ t].hom p :: Δ✝
Δ : Sequent L
a✝ : CutRestricted C d
⊢ CutRestricted C d
Theorem: LO.FirstOrder.Derivation.CutRestricted.ex'
Proof state before:
case ex
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p✝ q : SyntacticFormula L
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d :  ⊢¹ [→ t].hom p :: Δ✝
Δ : Sequent L
a✝ : CutRestricted C d
⊢ CutRestricted C d
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.wk'
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
d :  ⊢¹ Δ
ss : Δ ⊆ Γ
⊢ CutRestricted C (Derivation.wk d ss) → CutRestricted C d
Tactic:
rintro ⟨⟩
Proof state after:
case wk
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
d :  ⊢¹ Δ✝
ss : Δ✝ ⊆ Γ
Δ : Sequent L
ss✝ : Δ✝ ⊆ Γ
a✝ : CutRestricted C d
⊢ CutRestricted C d
Theorem: LO.FirstOrder.Derivation.CutRestricted.wk'
Proof state before:
case wk
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
d :  ⊢¹ Δ✝
ss : Δ✝ ⊆ Γ
Δ : Sequent L
ss✝ : Δ✝ ⊆ Γ
a✝ : CutRestricted C d
⊢ CutRestricted C d
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.cut'
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ
dn :  ⊢¹ ~p :: Δ
⊢ CutRestricted C (Derivation.cut dp dn) → p ∈ C ∧ CutRestricted C dp ∧ CutRestricted C dn
Tactic:
rintro ⟨⟩
Proof state after:
case cut
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ p ∈ C ∧ CutRestricted C dp ∧ CutRestricted C dn
Theorem: LO.FirstOrder.Derivation.CutRestricted.cut'
Proof state before:
case cut
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ p ∈ C ∧ CutRestricted C dp ∧ CutRestricted C dn
Tactic:
constructor
Proof state after:
case cut.left
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ p ∈ C

case cut.right
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ CutRestricted C dp ∧ CutRestricted C dn
Theorem: LO.FirstOrder.Derivation.CutRestricted.cut'
Proof state before:
case cut.left
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ p ∈ C

case cut.right
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ CutRestricted C dp ∧ CutRestricted C dn
Tactic:
{ assumption }
Proof state after:
case cut.right
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ CutRestricted C dp ∧ CutRestricted C dn
Theorem: LO.FirstOrder.Derivation.CutRestricted.cut'
Proof state before:
case cut.right
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ CutRestricted C dp ∧ CutRestricted C dn
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.cut'
Proof state before:
case cut.left
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ p ∈ C
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.cut'
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ
dn :  ⊢¹ ~p :: Δ
⊢ p ∈ C ∧ CutRestricted C dp ∧ CutRestricted C dn → CutRestricted C (Derivation.cut dp dn)
Tactic:
rintro ⟨h, dp, dq⟩
Proof state after:
case intro.intro
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp✝ :  ⊢¹ p :: Δ
dn :  ⊢¹ ~p :: Δ
h : p ∈ C
dp : CutRestricted C dp✝
dq : CutRestricted C dn
⊢ CutRestricted C (Derivation.cut dp✝ dn)
Theorem: LO.FirstOrder.Derivation.CutRestricted.cut'
Proof state before:
case intro.intro
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp✝ :  ⊢¹ p :: Δ
dn :  ⊢¹ ~p :: Δ
h : p ∈ C
dp : CutRestricted C dp✝
dq : CutRestricted C dn
⊢ CutRestricted C (Derivation.cut dp✝ dn)
Tactic:
exact CutRestricted.cut dp dq h
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
d :  ⊢¹ Δ
ss : C ⊆ C'
⊢ CutRestricted C d → CutRestricted C' d
Tactic:
induction d <;> simp[*]
Proof state after:
case or
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝¹ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
a_ih✝ : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝

case and
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝¹ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
a_ih✝¹ : CutRestricted C a✝¹ → CutRestricted C' a✝¹
a_ih✝ : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝¹ → CutRestricted C a✝ → CutRestricted C' a✝¹ ∧ CutRestricted C' a✝

case all
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
a_ih✝ : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝

case ex
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
a_ih✝ : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝

case wk
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝¹ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ Γ✝ : Sequent L
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
a_ih✝ : CutRestricted C a✝¹ → CutRestricted C' a✝¹
⊢ CutRestricted C a✝¹ → CutRestricted C' a✝¹

case cut
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
a_ih✝¹ : CutRestricted C a✝¹ → CutRestricted C' a✝¹
a_ih✝ : CutRestricted C a✝ → CutRestricted C' a✝
⊢ p✝ ∈ C → CutRestricted C a✝¹ → CutRestricted C a✝ → p✝ ∈ C' ∧ CutRestricted C' a✝¹ ∧ CutRestricted C' a✝
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof state before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝¹ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
ihp : CutRestricted C a✝¹ → CutRestricted C' a✝¹
ihq : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝¹ → CutRestricted C a✝ → CutRestricted C' a✝¹ ∧ CutRestricted C' a✝
Tactic:
case and _ _ _ _ ihp ihq => intro hp hq; exact ⟨ihp hp, ihq hq⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof state before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝¹ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
ih : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝
Tactic:
case or _ _ _ _ ih => exact ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof state before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝
Tactic:
case all _ _ _ _ ih => exact ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof state before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝
Tactic:
case ex _ _ _ _ ih => exact ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof state before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝¹ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ Γ✝ : Sequent L
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
ih : CutRestricted C a✝¹ → CutRestricted C' a✝¹
⊢ CutRestricted C a✝¹ → CutRestricted C' a✝¹
Tactic:
case wk _ _ _ _ ih => exact ih
Proof state after:
no goals