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

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

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

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

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

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

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