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

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]
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

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]
State after:
no goals

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, *]
State after:
no goals

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, *]
State after:
no goals

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]
State after:
no goals

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, *]
State after:
no goals

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, *]
State after:
no goals