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

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]
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 ⇑)) Δ

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

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

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

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

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

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

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

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