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 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 ( ⊢¹ Δ)
Tactic:
rcases H with ⟨⟨hl, H⟩, hpq⟩
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 q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.or p q, Γ) :: l)
hpq : p :: q :: Γ ∈ sequents l
hl : isProper l = true
H : p ⋎ q ∈ Γ
⊢ 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 q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.or p q, Γ) :: l)
hpq : p :: q :: Γ ∈ sequents l
hl : isProper l = true
H : p ⋎ q ∈ Γ
⊢ 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 q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hpq : p :: q :: Γ ∈ 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
μ : 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)
hpq : p :: q :: Γ ∈ 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.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
hpq : p :: q :: Δ ∈ sequents l
H : p ⋎ q ∈ Δ
⊢ 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 q : SyntacticFormula L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hpq : p :: q :: Γ ∈ 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.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
hpq : p :: q :: Δ ∈ sequents l
H : p ⋎ q ∈ Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
rcases derivation_of_isProper l hl _ hpq 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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hpq : p :: q :: Δ ∈ sequents l
H : p ⋎ q ∈ Δ
b :  ⊢¹ p :: q :: Δ
⊢ 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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hpq : p :: q :: Δ ∈ sequents l
H : p ⋎ q ∈ Δ
b :  ⊢¹ p :: q :: Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
have : ⊢¹ p ⋎ q :: Δ := Derivation.or (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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hpq : p :: q :: Δ ∈ sequents l
H : p ⋎ q ∈ Δ
b :  ⊢¹ p :: q :: Δ
this :  ⊢¹ p ⋎ q :: Δ
⊢ 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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hpq : p :: q :: Δ ∈ sequents l
H : p ⋎ q ∈ Δ
b :  ⊢¹ p :: 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
hpq : p :: q :: Δ ∈ sequents l
H : p ⋎ q ∈ Δ
b :  ⊢¹ p :: q :: Δ
⊢ Derivation (p :: q :: Δ)
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 q : SyntacticFormula L
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hpq : p :: q :: Δ ∈ sequents l
H : p ⋎ q ∈ Δ
b :  ⊢¹ p :: 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.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)
hpq : p :: q :: Γ ∈ 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)
hpq : p :: q :: Γ ∈ 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 : SyntacticSemiformula L 1
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
H : isProper ((Code.all p, Γ) :: l) = true
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.all p, Γ) :: 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 : SyntacticSemiformula L 1
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.all p, Γ) :: l)
H : (isProper l = true ∧ ∀' p ∈ Γ) ∧ (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Γ ∈ 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 : SyntacticSemiformula L 1
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.all p, Γ) :: l)
H : (isProper l = true ∧ ∀' p ∈ Γ) ∧ (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Γ ∈ 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
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.all p, Γ) :: l)
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Γ ∈ 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
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.all p, Γ) :: l)
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Γ ∈ 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
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Γ ∈ 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
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Γ ∈ 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
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ ∈ 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
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Γ ∈ 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
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ ∈ 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
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ ∈ sequents l
H : ∀' p ∈ Δ
b :  ⊢¹ (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ
⊢ 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
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ ∈ sequents l
H : ∀' p ∈ Δ
b :  ⊢¹ (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ
⊢ Nonempty ( ⊢¹ Δ)
Tactic:
have : ⊢¹ (∀' p) :: Δ :=
  Derivation.all (by simpa[shifts, List.toFinset_map, Finset.map_eq_image] 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
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ ∈ sequents l
H : ∀' p ∈ Δ
b :  ⊢¹ (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ
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
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ ∈ sequents l
H : ∀' p ∈ Δ
b :  ⊢¹ (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ
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
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ ∈ sequents l
H : ∀' p ∈ Δ
b :  ⊢¹ (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ
⊢ Derivation ((Rew.hom Rew.free) p :: shifts Δ)
Tactic:
simpa[shifts, List.toFinset_map, Finset.map_eq_image] 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
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hl : isProper l = true
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ ∈ sequents l
H : ∀' p ∈ Δ
b :  ⊢¹ (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Δ
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
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Γ ∈ 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
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
Δ : List (SyntacticFormula L)
hp : (Rew.hom Rew.free) p :: List.map (⇑(Rew.hom ⇑)) Γ ∈ 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 μ
p : SyntacticSemiformula L 1
t : SyntacticTerm L
Γ : List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
H : isProper ((Code.ex p t, Γ) :: l) = true
Δ : List (SyntacticFormula L)
hΔ : Δ ∈ sequents ((Code.ex p t, Γ) :: 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 : 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 ( ⊢¹ Δ)