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

State before:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
f : ℕ → SyntacticTerm L
d :  ⊢¹ Δ
⊢ CutRestricted C d → CutRestricted C (Derivation.rewrite d f)
Tactic:
induction d generalizing f <;> simp[-List.map_cons, Derivation.rewrite, *]
State after:
case axL
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ℕ 0
f : ℕ → SyntacticTerm L
⊢ CutRestricted C (id (Derivation.axL (List.map (⇑(Rew.rewrite f).hom) Δ✝) r✝ fun i => (Rew.rewrite f) (v✝ i)))

case or
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)

case and
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
a_ih✝¹ : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝¹ →
    CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝¹ f) ∧ CutRestricted C (Derivation.rewrite a✝ f)

case all
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ →
    CutRestricted C
      (Derivation.cast (Derivation.all (Derivation.cast (Derivation.rewrite a✝ (&0 :>ₙ fun x => ⇑ (f x))) ⋯)) ⋯)

case ex
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ →
    CutRestricted C
      (Derivation.cast (Derivation.ex ((Rew.rewrite f) t✝) (Derivation.cast (Derivation.rewrite a✝ f) ⋯)) ⋯)

case wk
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ Δ✝ Γ✝ : Sequent L
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)

case cut
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
a_ih✝¹ : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ p✝ ∈ C →
    CutRestricted C a✝¹ →
      CutRestricted C a✝ →
        (Rew.rewrite f).hom p✝ ∈ C ∧
          CutRestricted C (Derivation.rewrite a✝¹ f) ∧ CutRestricted C (Derivation.rewrite a✝ f)

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ℕ 0
f : ℕ → SyntacticTerm L
⊢ CutRestricted C (id (Derivation.axL (List.map (⇑(Rew.rewrite f).hom) Δ✝) r✝ fun i => (Rew.rewrite f) (v✝ i)))
Tactic:
case axL _ _ _ _ => simp[Rew.rel, Rew.nrel]
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
ihp : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
ihq : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝¹ →
    CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝¹ f) ∧ CutRestricted C (Derivation.rewrite a✝ f)
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 : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
Tactic:
case or _ _ ih => intro h; exact ih _ h
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ →
    CutRestricted C
      (Derivation.cast (Derivation.all (Derivation.cast (Derivation.rewrite a✝ (&0 :>ₙ fun x => ⇑ (f x))) ⋯)) ⋯)
Tactic:
case all _ _ _ ih =>
  rw [CutRestricted.cast, CutRestricted.all', CutRestricted.cast]
  exact ih _; simp
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ →
    CutRestricted C
      (Derivation.cast (Derivation.ex ((Rew.rewrite f) t✝) (Derivation.cast (Derivation.rewrite a✝ f) ⋯)) ⋯)
Tactic:
case ex _ _ _ ih =>
  rw [CutRestricted.cast, CutRestricted.ex', CutRestricted.cast]
  exact ih _; simp
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ Δ✝ Γ✝ : Sequent L
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
Tactic:
case wk _ _ ih => intro h; exact ih _ h
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
ihn : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ p✝ ∈ C →
    CutRestricted C a✝¹ →
      CutRestricted C a✝ →
        (Rew.rewrite f).hom p✝ ∈ C ∧
          CutRestricted C (Derivation.rewrite a✝¹ f) ∧ CutRestricted C (Derivation.rewrite a✝ f)
Tactic:
case cut _ _ ih ihn => intro hp h hn; exact ⟨hC _ _ hp, ih _ h, ihn _ hn⟩
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ℕ 0
f : ℕ → SyntacticTerm L
⊢ CutRestricted C (id (Derivation.axL (List.map (⇑(Rew.rewrite f).hom) Δ✝) r✝ fun i => (Rew.rewrite f) (v✝ i)))
Tactic:
simp[Rew.rel, Rew.nrel]
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
ihp : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
ihq : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝¹ →
    CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝¹ f) ∧ CutRestricted C (Derivation.rewrite a✝ f)
Tactic:
intro hp hq
State after:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
ihp : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
ihq : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
hp : CutRestricted C a✝¹
hq : CutRestricted C a✝
⊢ CutRestricted C (Derivation.rewrite a✝¹ f) ∧ CutRestricted C (Derivation.rewrite a✝ f)

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
ihp : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
ihq : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
hp : CutRestricted C a✝¹
hq : CutRestricted C a✝
⊢ CutRestricted C (Derivation.rewrite a✝¹ f) ∧ CutRestricted C (Derivation.rewrite a✝ f)
Tactic:
exact ⟨ihp _ hp, ihq _ hq⟩
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
Tactic:
intro h
State after:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
h : CutRestricted C a✝
⊢ CutRestricted C (Derivation.rewrite a✝ f)

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ q✝ : SyntacticFormula L
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
h : CutRestricted C a✝
⊢ CutRestricted C (Derivation.rewrite a✝ f)
Tactic:
exact ih _ h
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ →
    CutRestricted C
      (Derivation.cast (Derivation.all (Derivation.cast (Derivation.rewrite a✝ (&0 :>ₙ fun x => ⇑ (f x))) ⋯)) ⋯)
Tactic:
rw [CutRestricted.cast, CutRestricted.all', CutRestricted.cast]
State after:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ (&0 :>ₙ fun x => ⇑ (f x)))

L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ (∀' (Rew.rewrite (⇑Rew.bShift ∘ f)).hom p✝) :: List.map (⇑(Rew.rewrite f).hom) Δ✝ =
    List.map (⇑(Rew.rewrite f).hom) ((∀' p✝) :: Δ✝)

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ (&0 :>ₙ fun x => ⇑ (f x)))

L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ (∀' (Rew.rewrite (⇑Rew.bShift ∘ f)).hom p✝) :: List.map (⇑(Rew.rewrite f).hom) Δ✝ =
    List.map (⇑(Rew.rewrite f).hom) ((∀' p✝) :: Δ✝)
Tactic:
exact ih _
State after:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ (∀' (Rew.rewrite (⇑Rew.bShift ∘ f)).hom p✝) :: List.map (⇑(Rew.rewrite f).hom) Δ✝ =
    List.map (⇑(Rew.rewrite f).hom) ((∀' p✝) :: Δ✝)

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ (∀' (Rew.rewrite (⇑Rew.bShift ∘ f)).hom p✝) :: List.map (⇑(Rew.rewrite f).hom) Δ✝ =
    List.map (⇑(Rew.rewrite f).hom) ((∀' p✝) :: Δ✝)
Tactic:
simp
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ →
    CutRestricted C
      (Derivation.cast (Derivation.ex ((Rew.rewrite f) t✝) (Derivation.cast (Derivation.rewrite a✝ f) ⋯)) ⋯)
Tactic:
rw [CutRestricted.cast, CutRestricted.ex', CutRestricted.cast]
State after:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)

L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ (∃' (Rew.rewrite (⇑Rew.bShift ∘ f)).hom p✝) :: List.map (⇑(Rew.rewrite f).hom) Δ✝ =
    List.map (⇑(Rew.rewrite f).hom) ((∃' p✝) :: Δ✝)

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)

L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ (∃' (Rew.rewrite (⇑Rew.bShift ∘ f)).hom p✝) :: List.map (⇑(Rew.rewrite f).hom) Δ✝ =
    List.map (⇑(Rew.rewrite f).hom) ((∃' p✝) :: Δ✝)
Tactic:
exact ih _
State after:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ (∃' (Rew.rewrite (⇑Rew.bShift ∘ f)).hom p✝) :: List.map (⇑(Rew.rewrite f).hom) Δ✝ =
    List.map (⇑(Rew.rewrite f).hom) ((∃' p✝) :: Δ✝)

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ (∃' (Rew.rewrite (⇑Rew.bShift ∘ f)).hom p✝) :: List.map (⇑(Rew.rewrite f).hom) Δ✝ =
    List.map (⇑(Rew.rewrite f).hom) ((∃' p✝) :: Δ✝)
Tactic:
simp
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ Δ✝ Γ✝ : Sequent L
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
Tactic:
intro h
State after:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ Δ✝ Γ✝ : Sequent L
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
f : ℕ → SyntacticTerm L
h : CutRestricted C a✝¹
⊢ CutRestricted C (Derivation.rewrite a✝¹ f)

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ Δ✝ Γ✝ : Sequent L
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
f : ℕ → SyntacticTerm L
h : CutRestricted C a✝¹
⊢ CutRestricted C (Derivation.rewrite a✝¹ f)
Tactic:
exact ih _ h
State after:
no goals

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
ihn : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ p✝ ∈ C →
    CutRestricted C a✝¹ →
      CutRestricted C a✝ →
        (Rew.rewrite f).hom p✝ ∈ C ∧
          CutRestricted C (Derivation.rewrite a✝¹ f) ∧ CutRestricted C (Derivation.rewrite a✝ f)
Tactic:
intro hp h hn
State after:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
ihn : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
hp : p✝ ∈ C
h : CutRestricted C a✝¹
hn : CutRestricted C a✝
⊢ (Rew.rewrite f).hom p✝ ∈ C ∧ CutRestricted C (Derivation.rewrite a✝¹ f) ∧ CutRestricted C (Derivation.rewrite a✝ f)

State before:
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
ihn : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
hp : p✝ ∈ C
h : CutRestricted C a✝¹
hn : CutRestricted C a✝
⊢ (Rew.rewrite f).hom p✝ ∈ C ∧ CutRestricted C (Derivation.rewrite a✝¹ f) ∧ CutRestricted C (Derivation.rewrite a✝ f)
Tactic:
exact ⟨hC _ _ hp, ih _ h, ihn _ hn⟩
State after:
no goals