Theorem: LO.FirstOrder.Semiformula.eval_operator₂ (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (Eval s e ε) (o.operator ![t₁, t₂]) ↔ o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
simp [eval_operator]
State after:
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (o.val fun i => Semiterm.val s e ε (![t₁, t₂] i)) ↔ o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]

State before:
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (o.val fun i => Semiterm.val s e ε (![t₁, t₂] i)) ↔ o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
apply of_eq
State after:
case a
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (o.val fun i => Semiterm.val s e ε (![t₁, t₂] i)) = o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]

State before:
case a
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (o.val fun i => Semiterm.val s e ε (![t₁, t₂] i)) = o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
congr
State after:
case a.e_v
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (fun i => Semiterm.val s e ε (![t₁, t₂] i)) = ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]

State before:
case a.e_v
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (fun i => Semiterm.val s e ε (![t₁, t₂] i)) = ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
funext i
State after:
case a.e_v.h
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
i : Fin 2
⊢ Semiterm.val s e ε (![t₁, t₂] i) = ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂] i

State before:
case a.e_v.h
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
i : Fin 2
⊢ Semiterm.val s e ε (![t₁, t₂] i) = ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂] i
Tactic:
cases' i using Fin.cases with i <;> simp
State after:
no goals