internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof 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
Proof 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✝
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof 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
Proof 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✝
Theorem: LO.FirstOrder.Derivation.CutRestricted.of_subset
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.length_cast
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
d :  ⊢¹ Δ
e : Δ = Γ
⊢ length (Derivation.cast d e) = length d
Tactic:
rcases e with rfl
Proof state after:
L : Language
Δ Δ₁ Δ₂ : Sequent L
p q r : SyntacticFormula L
d :  ⊢¹ Δ
⊢ length (Derivation.cast d ⋯) = length d
Theorem: LO.FirstOrder.Derivation.length_cast
Proof state before:
L : Language
Δ Δ₁ Δ₂ : Sequent L
p q r : SyntacticFormula L
d :  ⊢¹ Δ
⊢ length (Derivation.cast d ⋯) = length d
Tactic:
simp[Derivation.cast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.length_cast'
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
d :  ⊢¹ Δ
e : Δ = Γ
⊢ length (cast ⋯ d) = length d
Tactic:
rcases e with rfl
Proof state after:
L : Language
Δ Δ₁ Δ₂ : Sequent L
p q r : SyntacticFormula L
d :  ⊢¹ Δ
⊢ length (cast ⋯ d) = length d
Theorem: LO.FirstOrder.Derivation.length_cast'
Proof state before:
L : Language
Δ Δ₁ Δ₂ : Sequent L
p q r : SyntacticFormula L
d :  ⊢¹ Δ
⊢ length (cast ⋯ d) = length d
Tactic:
simp[Derivation.cast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.cast
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
Δ Γ : Sequent L
e : Δ = Γ
d :  ⊢¹ Δ
⊢ CutRestricted C (Derivation.cast d e) ↔ CutRestricted C d
Tactic:
rcases e with ⟨rfl⟩
Proof state after:
case refl
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
Δ : Sequent L
d :  ⊢¹ Δ
⊢ CutRestricted C (Derivation.cast d ⋯) ↔ CutRestricted C d
Theorem: LO.FirstOrder.Derivation.CutRestricted.cast
Proof state before:
case refl
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
Δ : Sequent L
d :  ⊢¹ Δ
⊢ CutRestricted C (Derivation.cast d ⋯) ↔ CutRestricted C d
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutFree.cast
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p q r : SyntacticFormula L
Δ Γ : Sequent L
e : Δ = Γ
d :  ⊢¹ Δ
⊢ CutFree (Derivation.cast d e) ↔ CutFree d
Tactic:
rcases e with ⟨rfl⟩
Proof state after:
case refl
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ : Sequent L
d :  ⊢¹ Δ
⊢ CutFree (Derivation.cast d ⋯) ↔ CutFree d
Theorem: LO.FirstOrder.Derivation.CutFree.cast
Proof state before:
case refl
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ : Sequent L
d :  ⊢¹ Δ
⊢ CutFree (Derivation.cast d ⋯) ↔ CutFree d
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ne_step_max
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
n m : ℕ
⊢ n ≤ max n m
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ne_step_max'
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
n m : ℕ
⊢ n ≤ max m n
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.neg_ne_and
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q✝ r p q : SyntacticFormula L
⊢ complexity (~p) ≠ complexity (p ⋏ q)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.shifts_image
Proof state before:
L : Language
Δ✝ Δ₁✝ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
L₁ : Language
L₂ : Language
Δ₁ Γ₁ : Finset (SyntacticFormula L₁)
Φ : L₁ →ᵥ L₂
Δ : List (SyntacticFormula L₁)
⊢ (List.map (⇑(lMap Φ)) Δ)⁺ = List.map (⇑(lMap Φ)) Δ⁺
Tactic:
simp[shifts, shiftEmb, Finset.map_eq_image, Finset.image_image, Function.comp, Semiformula.lMap_shift]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.lMap
Proof state before:
L : Language
Δ✝ Δ₁✝ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
L₁ : Language
L₂ : Language
Δ₁ Γ₁ : Finset (SyntacticFormula L₁)
C : Set (SyntacticFormula L₂)
Δ : Sequent L₁
Φ : L₁ →ᵥ L₂
d :  ⊢¹ Δ
⊢ CutRestricted C (Derivation.lMap Φ d) ↔ CutRestricted (⇑(Semiformula.lMap Φ) ⁻¹' C) d
Tactic:
induction d <;> simp[Derivation.lMap, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutFree.lMap
Proof state before:
L : Language
Δ✝ Δ₁✝ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
L₁ : Language
L₂ : Language
Δ₁ Γ₁ : Finset (SyntacticFormula L₁)
Δ : Sequent L₁
Φ : L₁ →ᵥ L₂
d :  ⊢¹ Δ
⊢ CutFree (Derivation.lMap Φ d) ↔ CutFree d
Tactic:
simp[CutFree, CutRestricted.lMap]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.free_rewrite_eq
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticSemiformula L 1
⊢ (Rew.hom Rew.free) ((Rew.rewrite fun x => Rew.bShift (f x)).hom p) =
    (Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).hom ((Rew.hom Rew.free) p)
Tactic:
simp[←Rew.hom_comp_app]
Proof state after:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticSemiformula L 1
⊢ (Rew.comp Rew.free (Rew.rewrite fun x => Rew.bShift (f x))).hom p =
    ((Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).comp Rew.free).hom p
Theorem: LO.FirstOrder.Derivation.free_rewrite_eq
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticSemiformula L 1
⊢ (Rew.comp Rew.free (Rew.rewrite fun x => Rew.bShift (f x))).hom p =
    ((Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).comp Rew.free).hom p
Tactic:
exact Rew.hom_ext' (by ext x <;> simp[Rew.comp_app, Fin.eq_zero])
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.free_rewrite_eq
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticSemiformula L 1
⊢ Rew.comp Rew.free (Rew.rewrite fun x => Rew.bShift (f x)) = (Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).comp Rew.free
Tactic:
ext x <;> simp[Rew.comp_app, Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.shift_rewrite_eq
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticFormula L
⊢ (Rew.hom ⇑) ((Rew.rewrite f).hom p) = (Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).hom ((Rew.hom ⇑) p)
Tactic:
simp[←Rew.hom_comp_app]
Proof state after:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticFormula L
⊢ (Rew.comp ⇑ (Rew.rewrite f)).hom p = ((Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).comp ⇑).hom p
Theorem: LO.FirstOrder.Derivation.shift_rewrite_eq
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticFormula L
⊢ (Rew.comp ⇑ (Rew.rewrite f)).hom p = ((Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).comp ⇑).hom p
Tactic:
exact Rew.hom_ext' (by ext x <;> simp[Rew.comp_app])
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.shift_rewrite_eq
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticFormula L
⊢ Rew.comp ⇑ (Rew.rewrite f) = (Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).comp ⇑
Tactic:
ext x <;> simp[Rew.comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.rewrite_subst_eq
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
t : Semiterm L ℕ 0
p : SyntacticSemiformula L 1
⊢ (Rew.rewrite f).hom ([→ t].hom p) = [→ (Rew.rewrite f) t].hom ((Rew.rewrite (⇑Rew.bShift ∘ f)).hom p)
Tactic:
simp[←Rew.hom_comp_app]
Proof state after:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
t : Semiterm L ℕ 0
p : SyntacticSemiformula L 1
⊢ ((Rew.rewrite f).comp [→ t]).hom p = ([→ (Rew.rewrite f) t].comp (Rew.rewrite (⇑Rew.bShift ∘ f))).hom p
Theorem: LO.FirstOrder.Derivation.rewrite_subst_eq
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
t : Semiterm L ℕ 0
p : SyntacticSemiformula L 1
⊢ ((Rew.rewrite f).comp [→ t]).hom p = ([→ (Rew.rewrite f) t].comp (Rew.rewrite (⇑Rew.bShift ∘ f))).hom p
Tactic:
exact Rew.hom_ext' (by ext x <;> simp[Rew.comp_app])
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.rewrite_subst_eq
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
t : Semiterm L ℕ 0
p : SyntacticSemiformula L 1
⊢ (Rew.rewrite f).comp [→ t] = [→ (Rew.rewrite f) t].comp (Rew.rewrite (⇑Rew.bShift ∘ f))
Tactic:
ext x <;> simp[Rew.comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Derivation.CutRestricted.rewrite
Proof 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
Proof state after:
no goals