Theorem: LO.FirstOrder.Derivation.CutRestricted.and' (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 :: Δ
dq :  ⊢¹ q :: Δ
⊢ CutRestricted C (Derivation.and dp dq) → CutRestricted C dp ∧ CutRestricted C dq
Tactic:
rintro ⟨⟩
State after:
case and
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dq :  ⊢¹ q :: Δ✝
Δ : Sequent L
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dq
⊢ CutRestricted C dp ∧ CutRestricted C dq

State before:
case and
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dq :  ⊢¹ q :: Δ✝
Δ : Sequent L
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dq
⊢ CutRestricted C dp ∧ CutRestricted C dq
Tactic:
constructor <;> 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 :: Δ
dq :  ⊢¹ q :: Δ
⊢ CutRestricted C dp ∧ CutRestricted C dq → CutRestricted C (Derivation.and dp dq)
Tactic:
rintro ⟨dp, dq⟩
State after:
case intro
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp✝ :  ⊢¹ p :: Δ
dq✝ :  ⊢¹ q :: Δ
dp : CutRestricted C dp✝
dq : CutRestricted C dq✝
⊢ CutRestricted C (Derivation.and dp✝ dq✝)

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