Theorem: LO.FirstOrder.Rew.q_comp_bShift_app (Logic/FirstOrder/Basic/Syntax/Rew.lean)

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ₁ n₁
⊢ ω.q (bShift t) = bShift (ω t)
Tactic:
have := ext' (ω.q_comp_bShift) t
State after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ₁ n₁
this : (ω.q.comp bShift) t = (bShift.comp ω) t
⊢ ω.q (bShift t) = bShift (ω t)

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ₁ n₁
this : (ω.q.comp bShift) t = (bShift.comp ω) t
⊢ ω.q (bShift t) = bShift (ω t)
Tactic:
simpa only [comp_app] using this
State after:
no goals