Theorem: LO.FirstOrder.Rew.eq_bind (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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
⊢ ω = bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)
Tactic:
ext t
State after:
case hb
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Fin n₁
⊢ ω #t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) #t

case hf
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t

State before:
case hb
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Fin n₁
⊢ ω #t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) #t

case hf
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t
Tactic:
induction t
State after:
case hb.mk
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
val✝ : ℕ
isLt✝ : val✝ < n₁
⊢ ω #⟨val✝, isLt✝⟩ = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) #⟨val✝, isLt✝⟩

case hf
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t

State before:
case hb.mk
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
val✝ : ℕ
isLt✝ : val✝ < n₁
⊢ ω #⟨val✝, isLt✝⟩ = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) #⟨val✝, isLt✝⟩

case hf
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t
Tactic:
simp[Rew.func'']
State after:
case hf
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t

State before:
case hf
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t
Tactic:
simp[*]
State after:
no goals