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 μ
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.verum, Γ) :: l)
H : isProper l = true ∧ ⊤ ∈ Γ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases H with ⟨ih, h⟩
Proof state after:
case 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 μ
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.verum, Γ) :: l)
ih : isProper l = true
h : ⊤ ∈ Γ
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case 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 μ
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.verum, Γ) :: l)
ih : isProper l = true
h : ⊤ ∈ Γ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
simp[sequents] at hΔ
Proof state after:
case 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 μ
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h : ⊤ ∈ Γ
hΔ : Δ = Γ ∨ ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case 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 μ
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h : ⊤ ∈ Γ
hΔ : Δ = Γ ∨ ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases hΔ with (rfl | hΔ)
Proof state after:
case 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 μ
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h : ⊤ ∈ Δ
⊢ Nonempty ( ⊢¹ Δ)

case 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 μ
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h : ⊤ ∈ Γ
hΔ : ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case 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 μ
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h : ⊤ ∈ Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
exact ⟨verum' (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 μ
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h : ⊤ ∈ Δ
⊢ ⊤ ∈ Δ
Tactic:
simp[h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case 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 μ
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h : ⊤ ∈ Γ
hΔ : ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
exact derivation_of_isProper l ih _ (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 μ
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h : ⊤ ∈ Γ
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 μ
p q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
H : isProper ((Code.and p q, Γ) :: l) = true
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.and p q, Γ) :: 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 μ
p q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.and p q, Γ) :: l)
H : ((isProper l = true ∧ p ⋏ q ∈ Γ) ∧ p :: Γ ∈ sequents l) ∧ q :: Γ ∈ 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 μ
p q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.and p q, Γ) :: l)
H : ((isProper l = true ∧ p ⋏ q ∈ Γ) ∧ p :: Γ ∈ sequents l) ∧ q :: Γ ∈ sequents l
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases H with ⟨⟨⟨hl, H⟩, hp⟩, hq⟩
Proof state after:
case intro.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 q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.and p q, Γ) :: l)
hq : q :: Γ ∈ sequents l
hp : p :: Γ ∈ sequents l
hl : isProper l = true
H : p ⋏ q ∈ Γ
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.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 q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.and p q, Γ) :: l)
hq : q :: Γ ∈ sequents l
hp : p :: Γ ∈ sequents l
hl : isProper l = true
H : p ⋏ q ∈ Γ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
simp[sequents] at hΔ
Proof state after:
case intro.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 q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hq : q :: Γ ∈ sequents l
hp : p :: Γ ∈ sequents l
hl : isProper l = true
H : p ⋏ q ∈ Γ
hΔ : Δ = Γ ∨ ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.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 q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hq : q :: Γ ∈ sequents l
hp : p :: Γ ∈ sequents l
hl : isProper l = true
H : p ⋏ q ∈ Γ
hΔ : Δ = Γ ∨ ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases hΔ with (rfl | hΔ)
Proof state after:
case intro.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
⊢ Nonempty ( ⊢¹ Δ)

case intro.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 q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hq : q :: Γ ∈ sequents l
hp : p :: Γ ∈ sequents l
hl : isProper l = true
H : p ⋏ q ∈ Γ
hΔ : ∃ a, (a, Δ) ∈ l
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
have : Nonempty (⊢¹ p :: Δ) := derivation_of_isProper l hl _ hp
Proof state after:
case intro.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
this : Nonempty ( ⊢¹ p :: Δ)
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
this : Nonempty ( ⊢¹ p :: Δ)
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases this with ⟨bp⟩
Proof state after:
case intro.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
bp :  ⊢¹ p :: Δ
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
bp :  ⊢¹ p :: Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
have : Nonempty (⊢¹ q :: Δ) := derivation_of_isProper l hl _ hq
Proof state after:
case intro.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
bp :  ⊢¹ p :: Δ
this : Nonempty ( ⊢¹ q :: Δ)
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
bp :  ⊢¹ p :: Δ
this : Nonempty ( ⊢¹ q :: Δ)
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases this with ⟨bq⟩
Proof state after:
case intro.intro.intro.inl.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
bp :  ⊢¹ p :: Δ
bq :  ⊢¹ q :: Δ
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro.intro.inl.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
bp :  ⊢¹ p :: Δ
bq :  ⊢¹ q :: Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
have : ⊢¹ p ⋏ q :: Δ := and (by simpa using bp) (by simpa using bq)
Proof state after:
case intro.intro.intro.inl.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
bp :  ⊢¹ p :: Δ
bq :  ⊢¹ q :: Δ
this :  ⊢¹ p ⋏ q :: Δ
⊢ Nonempty ( ⊢¹ Δ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.intro.intro.inl.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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
bp :  ⊢¹ p :: Δ
bq :  ⊢¹ q :: Δ
this :  ⊢¹ p ⋏ q :: Δ
⊢ 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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
bp :  ⊢¹ p :: Δ
bq :  ⊢¹ q :: Δ
⊢ Derivation (p :: Δ)
Tactic:
simpa using bp
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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
bp :  ⊢¹ p :: Δ
bq :  ⊢¹ q :: Δ
⊢ Derivation (q :: Δ)
Tactic:
simpa using bq
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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hq : q :: Δ ∈ sequents l
hp : p :: Δ ∈ sequents l
H : p ⋏ q ∈ Δ
bp :  ⊢¹ p :: Δ
bq :  ⊢¹ q :: Δ
this :  ⊢¹ p ⋏ q :: Δ
⊢ p ⋏ q :: Δ ⊆ Δ
Tactic:
simp[H]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper
Proof state before:
case intro.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 q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hq : q :: Γ ∈ sequents l
hp : p :: Γ ∈ sequents l
hl : isProper l = true
H : p ⋏ q ∈ Γ
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 q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hq : q :: Γ ∈ sequents l
hp : p :: Γ ∈ sequents l
hl : isProper l = true
H : p ⋏ q ∈ Γ
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 μ
p q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
H : isProper ((Code.or p q, Γ) :: l) = true
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.or p q, Γ) :: 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 μ
p q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.or p q, Γ) :: l)
H : (isProper l = true ∧ p ⋎ q ∈ Γ) ∧ p :: q :: Γ ∈ sequents l
⊢ Nonempty ( ⊢¹ Δ)