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

State before:
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
b : { d // CutFree d }
⊢ Γ ∈ (ofDerivation b).sequents
Tactic:
rcases b with ⟨b, hb⟩
State after:
case mk
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
b :  ⊢¹ Γ
hb : CutFree b
⊢ Γ ∈ (ofDerivation ⟨b, hb⟩).sequents

State before:
case mk
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
b :  ⊢¹ Γ
hb : CutFree b
⊢ Γ ∈ (ofDerivation ⟨b, hb⟩).sequents
Tactic:
cases b <;> simp[ofDerivation, sequents]
State after:
case mk.cut
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Γ)
a✝ : Derivation (~p✝ :: Γ)
hb : CutFree (a✝¹.cut a✝)
⊢ ∃ a, (a, Γ) ∈ ofDerivation ⟨a✝¹.cut a✝, hb⟩

State before:
case mk.cut
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Γ)
a✝ : Derivation (~p✝ :: Γ)
hb : CutFree (a✝¹.cut a✝)
⊢ ∃ a, (a, Γ) ∈ ofDerivation ⟨a✝¹.cut a✝, hb⟩
Tactic:
{ contradiction }
State after:
no goals

State before:
case mk.cut
μ : Type ?u.778856
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : Sequent L
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Γ)
a✝ : Derivation (~p✝ :: Γ)
hb : CutFree (a✝¹.cut a✝)
⊢ ∃ a, (a, Γ) ∈ ofDerivation ⟨a✝¹.cut a✝, hb⟩
Tactic:
contradiction
State after:
no goals