Theorem: LO.FirstOrder.Derivation.CutRestricted.cut' (Logic/FirstOrder/Basic/Calculus.lean)

State before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ
dn :  ⊢¹ ~p :: Δ
⊢ CutRestricted C (Derivation.cut dp dn) → p ∈ C ∧ CutRestricted C dp ∧ CutRestricted C dn
Tactic:
rintro ⟨⟩
State after:
case cut
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ p ∈ C ∧ CutRestricted C dp ∧ CutRestricted C dn

State before:
case cut
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ p ∈ C ∧ CutRestricted C dp ∧ CutRestricted C dn
Tactic:
constructor
State after:
case cut.left
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ p ∈ C

case cut.right
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ CutRestricted C dp ∧ CutRestricted C dn

State before:
case cut.left
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ p ∈ C

case cut.right
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ CutRestricted C dp ∧ CutRestricted C dn
Tactic:
{ assumption }
State after:
case cut.right
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ CutRestricted C dp ∧ CutRestricted C dn

State before:
case cut.right
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ CutRestricted C dp ∧ CutRestricted C dn
Tactic:
constructor <;> assumption
State after:
no goals

State before:
case cut.left
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ p ∈ C
Tactic:
assumption
State after:
no goals

State before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ
dn :  ⊢¹ ~p :: Δ
⊢ p ∈ C ∧ CutRestricted C dp ∧ CutRestricted C dn → CutRestricted C (Derivation.cut dp dn)
Tactic:
rintro ⟨h, dp, dq⟩
State after:
case intro.intro
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp✝ :  ⊢¹ p :: Δ
dn :  ⊢¹ ~p :: Δ
h : p ∈ C
dp : CutRestricted C dp✝
dq : CutRestricted C dn
⊢ CutRestricted C (Derivation.cut dp✝ dn)

State before:
case intro.intro
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp✝ :  ⊢¹ p :: Δ
dn :  ⊢¹ ~p :: Δ
h : p ∈ C
dp : CutRestricted C dp✝
dq : CutRestricted C dn
⊢ CutRestricted C (Derivation.cut dp✝ dn)
Tactic:
exact CutRestricted.cut dp dq h
State after:
no goals