Theorem: LO.FirstOrder.Derivation.ProofList.derivation_of_isProper (Logic/FirstOrder/Computability/Calculus.lean)

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Δ
State after:
no goals

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
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 ( ⊢¹ Δ)

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₂⟩
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 ( ⊢¹ Δ)

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Δ
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 ( ⊢¹ Δ)

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Δ)
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 ( ⊢¹ Δ)

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₂)⟩
State after:
no goals

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₁
State after:
no goals

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₂
State after:
no goals

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Δ)
State after:
no goals

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Δ
State after:
no goals

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
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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Δ
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 ( ⊢¹ Δ)

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Δ)
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 ( ⊢¹ Δ)

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])⟩
State after:
no goals

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]
State after:
no goals

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Δ)
State after:
no goals

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Δ
State after:
no goals

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
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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Δ
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 ( ⊢¹ Δ)

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Δ)
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 ( ⊢¹ Δ)

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
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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)
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 ( ⊢¹ Δ)

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])⟩
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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Δ)
State after:
no goals

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Δ
State after:
no goals

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
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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Δ
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 ( ⊢¹ Δ)

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Δ)
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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)
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 ( ⊢¹ Δ)

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])⟩
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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Δ)
State after:
no goals

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Δ
State after:
no goals

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
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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Δ
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 ( ⊢¹ Δ)

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Δ)
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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)
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 ( ⊢¹ Δ)

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])⟩
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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Δ)
State after:
no goals

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Δ
State after:
no goals

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
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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Δ
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 ( ⊢¹ Δ)

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Δ)
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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)
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 ( ⊢¹ Δ)

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])⟩
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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Δ)
State after:
no goals

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Δ
State after:
no goals

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
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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Δ
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 ( ⊢¹ Δ)

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Δ)
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 ( ⊢¹ Δ)

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⟩
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 ( ⊢¹ Δ)

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⟩
State after:
no goals

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Δ)
State after:
no goals

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Δ
State after:
no goals