Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset (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
d :  ⊢¹ Δ
ss : C ⊆ C'
⊢ CutRestricted C d → CutRestricted C' d
Tactic:
induction d <;> simp[*]
State after:
case or
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝¹ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
a_ih✝ : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝

case and
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝¹ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
a_ih✝¹ : CutRestricted C a✝¹ → CutRestricted C' a✝¹
a_ih✝ : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝¹ → CutRestricted C a✝ → CutRestricted C' a✝¹ ∧ CutRestricted C' a✝

case all
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
a_ih✝ : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝

case ex
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
a_ih✝ : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝

case wk
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝¹ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ Γ✝ : Sequent L
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
a_ih✝ : CutRestricted C a✝¹ → CutRestricted C' a✝¹
⊢ CutRestricted C a✝¹ → CutRestricted C' a✝¹

case cut
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
a_ih✝¹ : CutRestricted C a✝¹ → CutRestricted C' a✝¹
a_ih✝ : CutRestricted C a✝ → CutRestricted C' a✝
⊢ p✝ ∈ C → CutRestricted C a✝¹ → CutRestricted C a✝ → p✝ ∈ C' ∧ CutRestricted C' a✝¹ ∧ CutRestricted C' a✝

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝¹ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
ihp : CutRestricted C a✝¹ → CutRestricted C' a✝¹
ihq : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝¹ → CutRestricted C a✝ → CutRestricted C' a✝¹ ∧ CutRestricted C' a✝
Tactic:
case and _ _ _ _ ihp ihq => intro hp hq; exact ⟨ihp hp, ihq hq⟩
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
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
ih : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝
Tactic:
case or _ _ _ _ ih => exact ih
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
ss : C ⊆ C'
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝
Tactic:
case all _ _ _ _ ih => exact ih
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
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝
Tactic:
case ex _ _ _ _ ih => exact ih
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
ss : C ⊆ C'
Δ✝ Γ✝ : Sequent L
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
ih : CutRestricted C a✝¹ → CutRestricted C' a✝¹
⊢ CutRestricted C a✝¹ → CutRestricted C' a✝¹
Tactic:
case wk _ _ _ _ ih => exact ih
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
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
ihp : CutRestricted C a✝¹ → CutRestricted C' a✝¹
ihn : CutRestricted C a✝ → CutRestricted C' a✝
⊢ p✝ ∈ C → CutRestricted C a✝¹ → CutRestricted C a✝ → p✝ ∈ C' ∧ CutRestricted C' a✝¹ ∧ CutRestricted C' a✝
Tactic:
case cut _ _ _ ihp ihn =>
  intro h hp hn; exact ⟨ss h, ihp hp, ihn hn⟩
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
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
ihp : CutRestricted C a✝¹ → CutRestricted C' a✝¹
ihq : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝¹ → CutRestricted C a✝ → CutRestricted C' a✝¹ ∧ CutRestricted C' a✝
Tactic:
intro hp hq
State after:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝¹ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
ihp : CutRestricted C a✝¹ → CutRestricted C' a✝¹
ihq : CutRestricted C a✝ → CutRestricted C' a✝
hp : CutRestricted C a✝¹
hq : CutRestricted C a✝
⊢ CutRestricted C' a✝¹ ∧ CutRestricted C' a✝

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝¹ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
ihp : CutRestricted C a✝¹ → CutRestricted C' a✝¹
ihq : CutRestricted C a✝ → CutRestricted C' a✝
hp : CutRestricted C a✝¹
hq : CutRestricted C a✝
⊢ CutRestricted C' a✝¹ ∧ CutRestricted C' a✝
Tactic:
exact ⟨ihp hp, ihq hq⟩
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
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
ih : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝
Tactic:
exact ih
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
ss : C ⊆ C'
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝
Tactic:
exact ih
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
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝
Tactic:
exact ih
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
ss : C ⊆ C'
Δ✝ Γ✝ : Sequent L
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
ih : CutRestricted C a✝¹ → CutRestricted C' a✝¹
⊢ CutRestricted C a✝¹ → CutRestricted C' a✝¹
Tactic:
exact ih
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
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
ihp : CutRestricted C a✝¹ → CutRestricted C' a✝¹
ihn : CutRestricted C a✝ → CutRestricted C' a✝
⊢ p✝ ∈ C → CutRestricted C a✝¹ → CutRestricted C a✝ → p✝ ∈ C' ∧ CutRestricted C' a✝¹ ∧ CutRestricted C' a✝
Tactic:
intro h hp hn
State after:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
ihp : CutRestricted C a✝¹ → CutRestricted C' a✝¹
ihn : CutRestricted C a✝ → CutRestricted C' a✝
h : p✝ ∈ C
hp : CutRestricted C a✝¹
hn : CutRestricted C a✝
⊢ p✝ ∈ C' ∧ CutRestricted C' a✝¹ ∧ CutRestricted C' a✝

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
ihp : CutRestricted C a✝¹ → CutRestricted C' a✝¹
ihn : CutRestricted C a✝ → CutRestricted C' a✝
h : p✝ ∈ C
hp : CutRestricted C a✝¹
hn : CutRestricted C a✝
⊢ p✝ ∈ C' ∧ CutRestricted C' a✝¹ ∧ CutRestricted C' a✝
Tactic:
exact ⟨ss h, ihp hp, ihn hn⟩
State after:
no goals