internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.ex p t, Γ) :: l)
H : (isProper l = true ∧ ∃' p ∈ Γ) ∧ [→ t].hom p :: Γ ∈ sequents l
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases H with ⟨⟨hl, H⟩, hp⟩
Proof state after:
case intro.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.ex p t, Γ) :: l)
hp : [→ t].hom p :: Γ ∈ sequents l
hl : isProper l = true
H : ∃' p ∈ Γ
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.ex p t, Γ) :: l)
hp : [→ t].hom p :: Γ ∈ sequents l
hl : isProper l = true
H : ∃' p ∈ Γ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
simp[sequents] at hΔ
Proof state after:
case intro.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hp : [→ t].hom p :: Γ ∈ sequents l
hl : isProper l = true
H : ∃' p ∈ Γ
hΔ : Δ = Γ ∨ ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hp : [→ t].hom p :: Γ ∈ sequents l
hl : isProper l = true
H : ∃' p ∈ Γ
hΔ : Δ = Γ ∨ ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases hΔ with (rfl | hΔ)
Proof state after:
case intro.intro.inl
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : [→ t].hom p :: Δ ∈ sequents l
H : ∃' p ∈ Δ
⊢ Nonempty ( ⊢¹ Δ)

case intro.intro.inr
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hp : [→ t].hom p :: Γ ∈ sequents l
hl : isProper l = true
H : ∃' p ∈ Γ
hΔ : ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro.inl
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : [→ t].hom p :: Δ ∈ sequents l
H : ∃' p ∈ Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases derivation_of_isProper l hl _ hp with ⟨b⟩
Proof state after:
case intro.intro.inl.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : [→ t].hom p :: Δ ∈ sequents l
H : ∃' p ∈ Δ
b :  ⊢¹ [→ t].hom p :: Δ
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro.inl.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : [→ t].hom p :: Δ ∈ sequents l
H : ∃' p ∈ Δ
b :  ⊢¹ [→ t].hom p :: Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
have : ⊢¹ (∃' p) :: Δ := Derivation.ex t (by simpa using b)
Proof state after:
case intro.intro.inl.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : [→ t].hom p :: Δ ∈ sequents l
H : ∃' p ∈ Δ
b :  ⊢¹ [→ t].hom p :: Δ
this :  ⊢¹ (∃' p) :: Δ
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro.inl.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : [→ t].hom p :: Δ ∈ sequents l
H : ∃' p ∈ Δ
b :  ⊢¹ [→ t].hom p :: Δ
this :  ⊢¹ (∃' p) :: Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
exact ⟨this.weakening (by simp[H])⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : [→ t].hom p :: Δ ∈ sequents l
H : ∃' p ∈ Δ
b :  ⊢¹ [→ t].hom p :: Δ
⊢ Derivation ([→ t].hom p :: Δ)
Tactic:
simpa using b
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : [→ t].hom p :: Δ ∈ sequents l
H : ∃' p ∈ Δ
b :  ⊢¹ [→ t].hom p :: Δ
this :  ⊢¹ (∃' p) :: Δ
⊢ (∃' p) :: Δ ⊆ Δ
Tactic:
simp[H]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro.inr
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hp : [→ t].hom p :: Γ ∈ sequents l
hl : isProper l = true
H : ∃' p ∈ Γ
hΔ : ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
exact derivation_of_isProper l hl _ (by simpa[sequents] using hΔ)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hp : [→ t].hom p :: Γ ∈ sequents l
hl : isProper l = true
H : ∃' p ∈ Γ
hΔ : ∃ a, (a, Δ) ∈ l
⊢ Δ ∈ sequents l
Tactic:
simpa[sequents] using hΔ
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
H : isProper ((Code.wk E, Γ) :: l) = true
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.wk E, Γ) :: l)
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
simp[isProper] at H
Proof state after:
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.wk E, Γ) :: l)
H : (isProper l = true ∧ E ⊆ Γ) ∧ E ∈ sequents l
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.wk E, Γ) :: l)
H : (isProper l = true ∧ E ⊆ Γ) ∧ E ∈ sequents l
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases H with ⟨⟨hl, H⟩, h⟩
Proof state after:
case intro.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.wk E, Γ) :: l)
h : E ∈ sequents l
hl : isProper l = true
H : E ⊆ Γ
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.wk E, Γ) :: l)
h : E ∈ sequents l
hl : isProper l = true
H : E ⊆ Γ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
simp[sequents] at hΔ
Proof state after:
case intro.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h : E ∈ sequents l
hl : isProper l = true
H : E ⊆ Γ
hΔ : Δ = Γ ∨ ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h : E ∈ sequents l
hl : isProper l = true
H : E ⊆ Γ
hΔ : Δ = Γ ∨ ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases hΔ with (rfl | hΔ)
Proof state after:
case intro.intro.inl
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h : E ∈ sequents l
hl : isProper l = true
H : E ⊆ Δ
⊢ Nonempty ( ⊢¹ Δ)

case intro.intro.inr
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h : E ∈ sequents l
hl : isProper l = true
H : E ⊆ Γ
hΔ : ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro.inl
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h : E ∈ sequents l
hl : isProper l = true
H : E ⊆ Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases derivation_of_isProper l hl E h with ⟨b⟩
Proof state after:
case intro.intro.inl.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h : E ∈ sequents l
hl : isProper l = true
H : E ⊆ Δ
b :  ⊢¹ E
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro.inl.intro
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h : E ∈ sequents l
hl : isProper l = true
H : E ⊆ Δ
b :  ⊢¹ E
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
exact ⟨b.weakening H⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro.inr
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h : E ∈ sequents l
hl : isProper l = true
H : E ⊆ Γ
hΔ : ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
exact derivation_of_isProper l hl _ (by simpa[sequents] using hΔ)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
μ : Type ?u.546030
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
E Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h : E ∈ sequents l
hl : isProper l = true
H : E ⊆ Γ
hΔ : ∃ a, (a, Δ) ∈ l
⊢ Δ ∈ sequents l
Tactic:
simpa[sequents] using hΔ
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.mem_ofDerivation
Proof state before:
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
b : { d // CutFree d }
⊢ Γ ∈ (ofDerivation b).sequents
Tactic:
rcases b with ⟨b, hb⟩
Proof state after:
case mk
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
b :  ⊢¹ Γ
hb : CutFree b
⊢ Γ ∈ (ofDerivation ⟨b, hb⟩).sequents
Theorem: LO.FirstOrder.Derivation.ProofList.mem_ofDerivation
Proof state before:
case mk
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
b :  ⊢¹ Γ
hb : CutFree b
⊢ Γ ∈ (ofDerivation ⟨b, hb⟩).sequents
Tactic:
cases b <;> simp[ofDerivation, sequents]
Proof state after:
case mk.cut
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Γ)
a✝ : Derivation (~p✝ :: Γ)
hb : CutFree (a✝¹.cut a✝)
⊢ ∃ a, (a, Γ) ∈ ofDerivation ⟨a✝¹.cut a✝, hb⟩
Theorem: LO.FirstOrder.Derivation.ProofList.mem_ofDerivation
Proof state before:
case mk.cut
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Γ)
a✝ : Derivation (~p✝ :: Γ)
hb : CutFree (a✝¹.cut a✝)
⊢ ∃ a, (a, Γ) ∈ ofDerivation ⟨a✝¹.cut a✝, hb⟩
Tactic:
{ contradiction }
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.mem_ofDerivation
Proof state before:
case mk.cut
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Γ)
a✝ : Derivation (~p✝ :: Γ)
hb : CutFree (a✝¹.cut a✝)
⊢ ∃ a, (a, Γ) ∈ ofDerivation ⟨a✝¹.cut a✝, hb⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.iff_mem_sequents
Proof state before:
μ : Type ?u.883067
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
l : ProofList L
⊢ (∃ c, (c, Γ) ∈ l) ↔ Γ ∈ l.sequents
Tactic:
simp[sequents]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.sequents_cons
Proof state before:
μ : Type ?u.896686
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
c : Code L
Γ : List (SyntacticFormula L)
l : ProofList L
⊢ sequents ((c, Γ) :: l) = Γ :: l.sequents
Tactic:
simp[sequents]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.List.mem_cons_cons
Proof state before:
μ : Type ?u.897613
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Type u_1
l : List α
a b : α
⊢ l ⊆ a :: b :: l
Tactic:
intro x hx
Proof state after:
μ : Type ?u.897613
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Type u_1
l : List α
a b x : α
hx : x ∈ l
⊢ x ∈ a :: b :: l