Theorem: LO.FirstOrder.Semiformula.eval_rew (Logic/FirstOrder/Basic/Semantics/Semantics.lean)

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ n₁
⊢ (Eval s e₂ ε₂) (ω.hom p) ↔
    (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p
Tactic:
induction p using rec' generalizing n₂ <;> simp [*, Semiterm.val_rew, eval_rel, eval_nrel, Rew.rel, Rew.nrel]
State after:
case hall
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∀ (x : M),
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∀ (x : M), (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝

case hex
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∃ x,
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∃ x, (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∀ (x : M),
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∀ (x : M), (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
Tactic:
case hall => simp [Function.comp]; exact iff_of_eq $ forall_congr (fun x => by congr; funext i; cases i using Fin.cases <;> simp)
State after:
no goals

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∃ x,
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∃ x, (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
Tactic:
case hex => simp [Function.comp]; exact exists_congr (fun x => iff_of_eq $ by congr; funext i; cases i using Fin.cases <;> simp)
State after:
no goals

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∀ (x : M),
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∀ (x : M), (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
Tactic:
simp [Function.comp]
State after:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∀ (x : M), (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝) ↔
    ∀ (x : M), (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∀ (x : M), (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝) ↔
    ∀ (x : M), (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝
Tactic:
exact iff_of_eq $ forall_congr (fun x => by congr; funext i; cases i using Fin.cases <;> simp)
State after:
no goals

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
x : M
⊢ (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝ =
    (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝
Tactic:
congr
State after:
case e_a.e_e
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
x : M
⊢ (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) = x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)

State before:
case e_a.e_e
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
x : M
⊢ (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) = x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)
Tactic:
funext i
State after:
case e_a.e_e.h
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
x : M
i : Fin (n✝ + 1)
⊢ Semiterm.val s (x :> e₂) ε₂ (ω.q #i) = (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) i

State before:
case e_a.e_e.h
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
x : M
i : Fin (n✝ + 1)
⊢ Semiterm.val s (x :> e₂) ε₂ (ω.q #i) = (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) i
Tactic:
cases i using Fin.cases <;> simp
State after:
no goals

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∃ x,
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∃ x, (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
Tactic:
simp [Function.comp]
State after:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∃ x, (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝) ↔
    ∃ x, (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∃ x, (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝) ↔
    ∃ x, (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝
Tactic:
exact exists_congr (fun x => iff_of_eq $ by congr; funext i; cases i using Fin.cases <;> simp)
State after:
no goals