internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
case cons
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
c : Code L × List (SyntacticFormula L)
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
h₁ : isProper (c :: l₁) = true
⊢ (c :: l₁ ++ l₂).isProper = true
Tactic:
simp
Proof state after:
case cons
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
c : Code L × List (SyntacticFormula L)
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
h₁ : isProper (c :: l₁) = true
⊢ isProper (c :: (l₁ ++ l₂)) = true
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h₁ : (isProper l₁ = true ∧ Semiformula.rel r v ∈ Γ) ∧ Semiformula.nrel r v ∈ Γ
⊢ (isProper (l₁ ++ l₂) = true ∧ Semiformula.rel r v ∈ Γ) ∧ Semiformula.nrel r v ∈ Γ
Tactic:
case axL k r v => exact ⟨⟨ih h₁.1.1, h₁.1.2⟩, h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
h₁ : isProper l₁ = true ∧ ⊤ ∈ Γ
⊢ isProper (l₁ ++ l₂) = true ∧ ⊤ ∈ Γ
Tactic:
case verum => exact ⟨ih h₁.1, h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
h₁ : ((isProper l₁ = true ∧ p ⋏ q ∈ Γ) ∧ p :: Γ ∈ sequents l₁) ∧ q :: Γ ∈ sequents l₁
⊢ ((isProper (l₁ ++ l₂) = true ∧ p ⋏ q ∈ Γ) ∧ (p :: Γ ∈ sequents l₁ ∨ p :: Γ ∈ l₂.sequents)) ∧
    (q :: Γ ∈ sequents l₁ ∨ q :: Γ ∈ l₂.sequents)
Tactic:
case and p q => exact ⟨⟨⟨ih h₁.1.1.1, h₁.1.1.2⟩, Or.inl h₁.1.2⟩, Or.inl h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
h₁ : (isProper l₁ = true ∧ p ⋎ q ∈ Γ) ∧ p :: q :: Γ ∈ sequents l₁
⊢ (isProper (l₁ ++ l₂) = true ∧ p ⋎ q ∈ Γ) ∧ (p :: q :: Γ ∈ sequents l₁ ∨ p :: q :: Γ ∈ l₂.sequents)
Tactic:
case or p q => exact ⟨⟨ih h₁.1.1, h₁.1.2⟩, Or.inl h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
a✝ : SyntacticSemiformula L 1
h₁ : (isProper l₁ = true ∧ ∀' a✝ ∈ Γ) ∧ (Rew.hom Rew.free) a✝ :: List.map (⇑(Rew.hom ⇑)) Γ ∈ sequents l₁
⊢ (isProper (l₁ ++ l₂) = true ∧ ∀' a✝ ∈ Γ) ∧
    ((Rew.hom Rew.free) a✝ :: List.map (⇑(Rew.hom ⇑)) Γ ∈ sequents l₁ ∨
      (Rew.hom Rew.free) a✝ :: List.map (⇑(Rew.hom ⇑)) Γ ∈ l₂.sequents)
Tactic:
case all => exact ⟨⟨ih h₁.1.1, h₁.1.2⟩, Or.inl h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
a✝¹ : SyntacticSemiformula L 1
a✝ : SyntacticTerm L
h₁ : (isProper l₁ = true ∧ ∃' a✝¹ ∈ Γ) ∧ [→ a✝].hom a✝¹ :: Γ ∈ sequents l₁
⊢ (isProper (l₁ ++ l₂) = true ∧ ∃' a✝¹ ∈ Γ) ∧ ([→ a✝].hom a✝¹ :: Γ ∈ sequents l₁ ∨ [→ a✝].hom a✝¹ :: Γ ∈ l₂.sequents)
Tactic:
case ex => exact ⟨⟨ih h₁.1.1, h₁.1.2⟩, Or.inl h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ a✝ : List (SyntacticFormula L)
h₁ : (isProper l₁ = true ∧ a✝ ⊆ Γ) ∧ a✝ ∈ sequents l₁
⊢ (isProper (l₁ ++ l₂) = true ∧ a✝ ⊆ Γ) ∧ (a✝ ∈ sequents l₁ ∨ a✝ ∈ l₂.sequents)
Tactic:
case wk => exact ⟨⟨ih h₁.1.1, h₁.1.2⟩, Or.inl h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h₁ : (isProper l₁ = true ∧ Semiformula.rel r v ∈ Γ) ∧ Semiformula.nrel r v ∈ Γ
⊢ (isProper (l₁ ++ l₂) = true ∧ Semiformula.rel r v ∈ Γ) ∧ Semiformula.nrel r v ∈ Γ
Tactic:
exact ⟨⟨ih h₁.1.1, h₁.1.2⟩, h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
h₁ : isProper l₁ = true ∧ ⊤ ∈ Γ
⊢ isProper (l₁ ++ l₂) = true ∧ ⊤ ∈ Γ
Tactic:
exact ⟨ih h₁.1, h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
h₁ : ((isProper l₁ = true ∧ p ⋏ q ∈ Γ) ∧ p :: Γ ∈ sequents l₁) ∧ q :: Γ ∈ sequents l₁
⊢ ((isProper (l₁ ++ l₂) = true ∧ p ⋏ q ∈ Γ) ∧ (p :: Γ ∈ sequents l₁ ∨ p :: Γ ∈ l₂.sequents)) ∧
    (q :: Γ ∈ sequents l₁ ∨ q :: Γ ∈ l₂.sequents)
Tactic:
exact ⟨⟨⟨ih h₁.1.1.1, h₁.1.1.2⟩, Or.inl h₁.1.2⟩, Or.inl h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
h₁ : (isProper l₁ = true ∧ p ⋎ q ∈ Γ) ∧ p :: q :: Γ ∈ sequents l₁
⊢ (isProper (l₁ ++ l₂) = true ∧ p ⋎ q ∈ Γ) ∧ (p :: q :: Γ ∈ sequents l₁ ∨ p :: q :: Γ ∈ l₂.sequents)
Tactic:
exact ⟨⟨ih h₁.1.1, h₁.1.2⟩, Or.inl h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
a✝ : SyntacticSemiformula L 1
h₁ : (isProper l₁ = true ∧ ∀' a✝ ∈ Γ) ∧ (Rew.hom Rew.free) a✝ :: List.map (⇑(Rew.hom ⇑)) Γ ∈ sequents l₁
⊢ (isProper (l₁ ++ l₂) = true ∧ ∀' a✝ ∈ Γ) ∧
    ((Rew.hom Rew.free) a✝ :: List.map (⇑(Rew.hom ⇑)) Γ ∈ sequents l₁ ∨
      (Rew.hom Rew.free) a✝ :: List.map (⇑(Rew.hom ⇑)) Γ ∈ l₂.sequents)
Tactic:
exact ⟨⟨ih h₁.1.1, h₁.1.2⟩, Or.inl h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ : List (SyntacticFormula L)
a✝¹ : SyntacticSemiformula L 1
a✝ : SyntacticTerm L
h₁ : (isProper l₁ = true ∧ ∃' a✝¹ ∈ Γ) ∧ [→ a✝].hom a✝¹ :: Γ ∈ sequents l₁
⊢ (isProper (l₁ ++ l₂) = true ∧ ∃' a✝¹ ∈ Γ) ∧ ([→ a✝].hom a✝¹ :: Γ ∈ sequents l₁ ∨ [→ a✝].hom a✝¹ :: Γ ∈ l₂.sequents)
Tactic:
exact ⟨⟨ih h₁.1.1, h₁.1.2⟩, Or.inl h₁.2⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_append
Proof state before:
μ : Type ?u.466511
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₂ : ProofList L
h₂ : l₂.isProper = true
l₁ : List (Code L × List (SyntacticFormula L))
ih : isProper l₁ = true → (l₁ ++ l₂).isProper = true
Γ a✝ : List (SyntacticFormula L)
h₁ : (isProper l₁ = true ∧ a✝ ⊆ Γ) ∧ a✝ ∈ sequents l₁
⊢ (isProper (l₁ ++ l₂) = true ∧ a✝ ⊆ Γ) ∧ (a✝ ∈ sequents l₁ ∨ a✝ ∈ l₂.sequents)
Tactic:
exact ⟨⟨ih h₁.1.1, h₁.1.2⟩, Or.inl h₁.2⟩
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 μ
x✝ : isProper [] = true
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents []
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
simp[sequents] at 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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
H : isProper ((Code.axL r v, Γ) :: l) = true
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.axL r v, Γ) :: 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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.axL r v, Γ) :: l)
H : (isProper l = true ∧ Semiformula.rel r v ∈ Γ) ∧ Semiformula.nrel r v ∈ Γ
⊢ 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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.axL r v, Γ) :: l)
H : (isProper l = true ∧ Semiformula.rel r v ∈ Γ) ∧ Semiformula.nrel r v ∈ Γ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases H with ⟨⟨ih, 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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.axL r v, Γ) :: l)
h₂ : Semiformula.nrel r v ∈ Γ
ih : isProper l = true
h₁ : Semiformula.rel r v ∈ Γ
⊢ 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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.axL r v, Γ) :: l)
h₂ : Semiformula.nrel r v ∈ Γ
ih : isProper l = true
h₁ : Semiformula.rel r v ∈ Γ
⊢ 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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h₂ : Semiformula.nrel r v ∈ Γ
ih : isProper l = true
h₁ : Semiformula.rel r v ∈ Γ
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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h₂ : Semiformula.nrel r v ∈ Γ
ih : isProper l = true
h₁ : Semiformula.rel r v ∈ Γ
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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h₂ : Semiformula.nrel r v ∈ Δ
h₁ : Semiformula.rel r v ∈ Δ
⊢ 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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h₂ : Semiformula.nrel r v ∈ Γ
ih : isProper l = true
h₁ : Semiformula.rel r v ∈ Γ
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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h₂ : Semiformula.nrel r v ∈ Δ
h₁ : Semiformula.rel r v ∈ Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
exact ⟨axL' r v (by simpa using h₁) (by simpa 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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h₂ : Semiformula.nrel r v ∈ Δ
h₁ : Semiformula.rel r v ∈ Δ
⊢ Semiformula.rel r v ∈ Δ
Tactic:
simpa 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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
ih : isProper l = true
h₂ : Semiformula.nrel r v ∈ Δ
h₁ : Semiformula.rel r v ∈ Δ
⊢ Semiformula.nrel r v ∈ Δ
Tactic:
simpa using 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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h₂ : Semiformula.nrel r v ∈ Γ
ih : isProper l = true
h₁ : Semiformula.rel r v ∈ Γ
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 μ
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
h₂ : Semiformula.nrel r v ∈ Γ
ih : isProper l = true
h₁ : Semiformula.rel r v ∈ Γ
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 μ
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
H : isProper ((Code.verum, Γ) :: l) = true
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.verum, Γ) :: 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 μ
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.verum, Γ) :: l)
H : isProper l = true ∧ ⊤ ∈ Γ
⊢ Nonempty ( ⊢¹ Δ)