internlm/Lean-Github huggingface dataset:
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:
rw [CutRestricted.cast, CutRestricted.all', CutRestricted.cast]
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 (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✝) :: Δ✝)
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.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 _
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 (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✝) :: Δ✝)
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
⊢ (∀' (Rew.rewrite (⇑Rew.bShift ∘ f)).hom p✝) :: List.map (⇑(Rew.rewrite f).hom) Δ✝ =
    List.map (⇑(Rew.rewrite f).hom) ((∀' p✝) :: Δ✝)
Tactic:
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:
rw [CutRestricted.cast, CutRestricted.ex', CutRestricted.cast]
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✝ : 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✝) :: Δ✝)
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.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 _
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✝ : 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✝) :: Δ✝)
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
⊢ (∃' (Rew.rewrite (⇑Rew.bShift ∘ f)).hom p✝) :: List.map (⇑(Rew.rewrite f).hom) Δ✝ =
    List.map (⇑(Rew.rewrite f).hom) ((∃' p✝) :: Δ✝)
Tactic:
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:
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
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)
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
h : CutRestricted C a✝¹
⊢ CutRestricted C (Derivation.rewrite a✝¹ f)
Tactic:
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:
intro hp h hn
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✝ : 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)
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
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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.length_rewrite
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
d :  ⊢¹ Δ
f : ℕ → SyntacticTerm L
⊢ length (rewrite d f) = length d
Tactic:
induction d generalizing f <;> simp[*, Derivation.rewrite, -List.map_cons]
Proof state after:
case axL
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ✝ : List (SyntacticFormula L)
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ℕ 0
f : ℕ → SyntacticTerm L
⊢ length (id (axL (List.map (⇑(Rew.rewrite f).hom) Δ✝) r✝ fun i => (Rew.rewrite f) (v✝ i))) = 0

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

case ex
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), length (rewrite a✝ f) = length a✝
f : ℕ → SyntacticTerm L
⊢ length (Derivation.cast (ex ((Rew.rewrite f) t✝) (Derivation.cast (rewrite a✝ f) ⋯)) ⋯) = length a✝ + 1
Theorem: LO.FirstOrder.Derivation.length_rewrite
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ✝ : List (SyntacticFormula L)
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ℕ 0
f : ℕ → SyntacticTerm L
⊢ length (id (axL (List.map (⇑(Rew.rewrite f).hom) Δ✝) r✝ fun i => (Rew.rewrite f) (v✝ i))) = 0
Tactic:
case axL => simp[Rew.rel, Rew.nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.length_rewrite
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), length (rewrite a✝ f) = length a✝
f : ℕ → SyntacticTerm L
⊢ length (Derivation.cast (all (Derivation.cast (rewrite a✝ (&0 :>ₙ fun x => ⇑ (f x))) ⋯)) ⋯) = length a✝ + 1
Tactic:
case all => rw[length_cast] <;> simp[Rew.q_rewrite, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.length_rewrite
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), length (rewrite a✝ f) = length a✝
f : ℕ → SyntacticTerm L
⊢ length (Derivation.cast (ex ((Rew.rewrite f) t✝) (Derivation.cast (rewrite a✝ f) ⋯)) ⋯) = length a✝ + 1
Tactic:
case ex => rw[length_cast] <;> simp[Rew.q_rewrite, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.length_rewrite
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ✝ : List (SyntacticFormula L)
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ℕ 0
f : ℕ → SyntacticTerm L
⊢ length (id (axL (List.map (⇑(Rew.rewrite f).hom) Δ✝) r✝ fun i => (Rew.rewrite f) (v✝ i))) = 0
Tactic:
simp[Rew.rel, Rew.nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.length_rewrite
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), length (rewrite a✝ f) = length a✝
f : ℕ → SyntacticTerm L
⊢ length (Derivation.cast (all (Derivation.cast (rewrite a✝ (&0 :>ₙ fun x => ⇑ (f x))) ⋯)) ⋯) = length a✝ + 1
Tactic:
rw[length_cast] <;> simp[Rew.q_rewrite, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.length_rewrite
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), length (rewrite a✝ f) = length a✝
f : ℕ → SyntacticTerm L
⊢ length (Derivation.cast (ex ((Rew.rewrite f) t✝) (Derivation.cast (rewrite a✝ f) ⋯)) ⋯) = length a✝ + 1
Tactic:
rw[length_cast] <;> simp[Rew.q_rewrite, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.map_subst_eq_free
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
p : SyntacticSemiformula L 1
h : ¬fvar? p m
⊢ (Rew.rewriteMap fun x => if x = m then 0 else x + 1).hom ([→ &m].hom p) = (Rew.hom Rew.free) p
Tactic:
simp[←Rew.hom_comp_app]
Proof state after:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
p : SyntacticSemiformula L 1
h : ¬fvar? p m
⊢ ((Rew.rewriteMap fun x => if x = m then 0 else x + 1).comp [→ &m]).hom p = (Rew.hom Rew.free) p
Theorem: LO.FirstOrder.Derivation.map_subst_eq_free
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
p : SyntacticSemiformula L 1
h : ¬fvar? p m
⊢ ((Rew.rewriteMap fun x => if x = m then 0 else x + 1).comp [→ &m]).hom p = (Rew.hom Rew.free) p
Tactic:
exact Semiformula.rew_eq_of_funEqOn (by simp[Rew.comp_app, Fin.eq_zero])
  (fun x hx => by simp[Rew.comp_app]; rintro rfl; contradiction)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.map_subst_eq_free
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
p : SyntacticSemiformula L 1
h : ¬fvar? p m
⊢ ∀ (x : Fin 1), ((Rew.rewriteMap fun x => if x = m then 0 else x + 1).comp [→ &m]) #x = Rew.free #x
Tactic:
simp[Rew.comp_app, Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.map_subst_eq_free
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
p : SyntacticSemiformula L 1
h : ¬fvar? p m
x : ℕ
hx : fvar? p x
⊢ (⇑((Rew.rewriteMap fun x => if x = m then 0 else x + 1).comp [→ &m]) ∘ Semiterm.fvar) x =
    (⇑Rew.free ∘ Semiterm.fvar) x
Tactic:
simp[Rew.comp_app]
Proof state after:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
p : SyntacticSemiformula L 1
h : ¬fvar? p m
x : ℕ
hx : fvar? p x
⊢ ¬x = m
Theorem: LO.FirstOrder.Derivation.map_subst_eq_free
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
p : SyntacticSemiformula L 1
h : ¬fvar? p m
x : ℕ
hx : fvar? p x
⊢ ¬x = m
Tactic:
rintro rfl
Proof state after:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
p : SyntacticSemiformula L 1
x : ℕ
hx : fvar? p x
h : ¬fvar? p x
⊢ False
Theorem: LO.FirstOrder.Derivation.map_subst_eq_free
Proof state before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
p : SyntacticSemiformula L 1
x : ℕ
hx : fvar? p x
h : ¬fvar? p x
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.map_rewriteMap_eq_shifts
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
⊢ List.map (⇑(Rew.rewriteMap fun x => if x = m then 0 else x + 1).hom) Δ = Δ⁺
Tactic:
simp[shifts]
Proof state after:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
⊢ List.map (⇑(Rew.rewriteMap fun x => if x = m then 0 else x + 1).hom) Δ = List.map (⇑(Rew.hom ⇑)) Δ
Theorem: LO.FirstOrder.Derivation.map_rewriteMap_eq_shifts
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
⊢ List.map (⇑(Rew.rewriteMap fun x => if x = m then 0 else x + 1).hom) Δ = List.map (⇑(Rew.hom ⇑)) Δ
Tactic:
apply List.map_congr
Proof state after:
case a
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
⊢ ∀ x ∈ Δ, (Rew.rewriteMap fun x => if x = m then 0 else x + 1).hom x = (Rew.hom ⇑) x
Theorem: LO.FirstOrder.Derivation.map_rewriteMap_eq_shifts
Proof state before:
case a
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
⊢ ∀ x ∈ Δ, (Rew.rewriteMap fun x => if x = m then 0 else x + 1).hom x = (Rew.hom ⇑) x
Tactic:
intro p hp
Proof state after:
case a
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
p : Semiformula L ℕ 0
hp : p ∈ Δ
⊢ (Rew.rewriteMap fun x => if x = m then 0 else x + 1).hom p = (Rew.hom ⇑) p
Theorem: LO.FirstOrder.Derivation.map_rewriteMap_eq_shifts
Proof state before:
case a
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
p : Semiformula L ℕ 0
hp : p ∈ Δ
⊢ (Rew.rewriteMap fun x => if x = m then 0 else x + 1).hom p = (Rew.hom ⇑) p
Tactic:
exact rew_eq_of_funEqOn₀ (by intro x hx; simp; rintro rfl; have := h p hp; contradiction)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.map_rewriteMap_eq_shifts
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
p : Semiformula L ℕ 0
hp : p ∈ Δ
⊢ Function.funEqOn p.fvar? (⇑(Rew.rewriteMap fun x => if x = m then 0 else x + 1) ∘ Semiterm.fvar) (⇑⇑ ∘ Semiterm.fvar)
Tactic:
intro x hx
Proof state after:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
p : Semiformula L ℕ 0
hp : p ∈ Δ
x : ℕ
hx : p.fvar? x
⊢ (⇑(Rew.rewriteMap fun x => if x = m then 0 else x + 1) ∘ Semiterm.fvar) x = (⇑⇑ ∘ Semiterm.fvar) x
Theorem: LO.FirstOrder.Derivation.map_rewriteMap_eq_shifts
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
p : Semiformula L ℕ 0
hp : p ∈ Δ
x : ℕ
hx : p.fvar? x
⊢ (⇑(Rew.rewriteMap fun x => if x = m then 0 else x + 1) ∘ Semiterm.fvar) x = (⇑⇑ ∘ Semiterm.fvar) x
Tactic:
simp
Proof state after:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
p : Semiformula L ℕ 0
hp : p ∈ Δ
x : ℕ
hx : p.fvar? x
⊢ ¬x = m
Theorem: LO.FirstOrder.Derivation.map_rewriteMap_eq_shifts
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
p : Semiformula L ℕ 0
hp : p ∈ Δ
x : ℕ
hx : p.fvar? x
⊢ ¬x = m
Tactic:
rintro rfl
Proof state after:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
Δ : Sequent L
p : Semiformula L ℕ 0
hp : p ∈ Δ
x : ℕ
hx : p.fvar? x
h : ∀ p ∈ Δ, ¬fvar? p x
⊢ False
Theorem: LO.FirstOrder.Derivation.map_rewriteMap_eq_shifts
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
Δ : Sequent L
p : Semiformula L ℕ 0
hp : p ∈ Δ
x : ℕ
hx : p.fvar? x
h : ∀ p ∈ Δ, ¬fvar? p x
⊢ False
Tactic:
have := h p hp
Proof state after:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
Δ : Sequent L
p : Semiformula L ℕ 0
hp : p ∈ Δ
x : ℕ
hx : p.fvar? x
h : ∀ p ∈ Δ, ¬fvar? p x
this : ¬p.fvar? x
⊢ False
Theorem: LO.FirstOrder.Derivation.map_rewriteMap_eq_shifts
Proof state before:
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
Δ : Sequent L
p : Semiformula L ℕ 0
hp : p ∈ Δ
x : ℕ
hx : p.fvar? x
h : ∀ p ∈ Δ, ¬fvar? p x
this : ¬p.fvar? x
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.System.inconsistent_lMap
Proof state before:
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
⊢ System.Inconsistent T → System.Inconsistent (Theory.lMap Φ T)
Tactic:
simp [System.inconsistent_iff_provable_bot]
Proof state after:
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
⊢ T ⊢! ⊥ → Theory.lMap Φ T ⊢! ⊥
Theorem: LO.FirstOrder.System.inconsistent_lMap
Proof state before:
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
⊢ T ⊢! ⊥ → Theory.lMap Φ T ⊢! ⊥
Tactic:
intro ⟨b⟩
Proof state after:
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
b : T ⊢ ⊥
⊢ Theory.lMap Φ T ⊢! ⊥
Theorem: LO.FirstOrder.System.inconsistent_lMap
Proof state before:
L₁ : Language
L₂ : Language
L : Language
T✝ : Theory L
Γ Δ : Sequent L
Φ : L₁ →ᵥ L₂
T : Theory L₁
b : T ⊢ ⊥
⊢ Theory.lMap Φ T ⊢! ⊥
Tactic:
exact ⟨by simpa using lMap Φ b⟩
Proof state after:
no goals