Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn (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
ε' : μ → M
p : Semiformula L μ n
h : Function.funEqOn p.fvar? ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p
Tactic:
unfold fvar? at h
State after:
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
ε' : μ → M
p : Semiformula L μ n
h : Function.funEqOn (fun x => x ∈ p.fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p

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
ε' : μ → M
p : Semiformula L μ n
h : Function.funEqOn (fun x => x ∈ p.fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p
Tactic:
induction p using Semiformula.rec'
State after:
case hverum
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊤.fvarList) ε ε'
⊢ (Eval s e ε) ⊤ ↔ (Eval s e ε') ⊤

case hfalsum
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊥.fvarList) ε ε'
⊢ (Eval s e ε) ⊥ ↔ (Eval s e ε') ⊥

case hrel
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r✝ v✝).fvarList) ε ε'
⊢ (Eval s e ε) (rel r✝ v✝) ↔ (Eval s e ε') (rel r✝ v✝)

case hnrel
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r✝ v✝).fvarList) ε ε'
⊢ (Eval s e ε) (nrel r✝ v✝) ↔ (Eval s e ε') (nrel r✝ v✝)

case hand
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p✝.fvarList) ε ε' → ((Eval s e ε) p✝ ↔ (Eval s e ε') p✝)
a✝ : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q✝.fvarList) ε ε' → ((Eval s e ε) q✝ ↔ (Eval s e ε') q✝)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p✝ ⋏ q✝).fvarList) ε ε'
⊢ (Eval s e ε) (p✝ ⋏ q✝) ↔ (Eval s e ε') (p✝ ⋏ q✝)

case hor
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p✝.fvarList) ε ε' → ((Eval s e ε) p✝ ↔ (Eval s e ε') p✝)
a✝ : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q✝.fvarList) ε ε' → ((Eval s e ε) q✝ ↔ (Eval s e ε') q✝)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p✝ ⋎ q✝).fvarList) ε ε'
⊢ (Eval s e ε) (p✝ ⋎ q✝) ↔ (Eval s e ε') (p✝ ⋎ q✝)

case hall
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p✝.fvarList) ε ε' → ((Eval s e ε) p✝ ↔ (Eval s e ε') p✝)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p✝).fvarList) ε ε'
⊢ (Eval s e ε) (∀' p✝) ↔ (Eval s e ε') (∀' p✝)

case hex
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p✝.fvarList) ε ε' → ((Eval s e ε) p✝ ↔ (Eval s e ε') p✝)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p✝).fvarList) ε ε'
⊢ (Eval s e ε) (∃' p✝) ↔ (Eval s e ε') (∃' p✝)

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊤.fvarList) ε ε'
⊢ (Eval s e ε) ⊤ ↔ (Eval s e ε') ⊤
Tactic:
case hverum => simp
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊥.fvarList) ε ε'
⊢ (Eval s e ε) ⊥ ↔ (Eval s e ε') ⊥
Tactic:
case hfalsum => simp
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Eval s e ε) (rel r v) ↔ (Eval s e ε') (rel r v)
Tactic:
case hrel k r v =>
  simp [eval_rel]; apply iff_of_eq; congr
  funext i
  exact Semiterm.val_eq_of_funEqOn (v i) (fun x hx ↦ h x (by simp [fvarList]; exact ⟨i, hx⟩))
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (Eval s e ε) (nrel r v) ↔ (Eval s e ε') (nrel r v)
Tactic:
case hnrel k r v =>
  simp [eval_nrel]; apply iff_of_eq; congr
  funext i
  exact Semiterm.val_eq_of_funEqOn (v i) (fun x hx ↦ h x (by simp [fvarList]; exact ⟨i, hx⟩))
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
⊢ (Eval s e ε) (∀' p) ↔ (Eval s e ε') (∀' p)
Tactic:
case hall p ih =>
  simp; apply forall_congr'; intro x
  exact ih (fun x hx ↦ h _ $ by simp [fvar?]; exact hx)
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
⊢ (Eval s e ε) (∃' p) ↔ (Eval s e ε') (∃' p)
Tactic:
case hex p ih =>
  simp; apply exists_congr; intro x
  exact ih (fun x hx ↦ h _ $ by simp [fvar?]; exact hx)
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊤.fvarList) ε ε'
⊢ (Eval s e ε) ⊤ ↔ (Eval s e ε') ⊤
Tactic:
simp
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊥.fvarList) ε ε'
⊢ (Eval s e ε) ⊥ ↔ (Eval s e ε') ⊥
Tactic:
simp
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Eval s e ε) (rel r v) ↔ (Eval s e ε') (rel r v)
Tactic:
simp [eval_rel]
State after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Structure.rel r fun i => Semiterm.val s e ε (v i)) ↔ Structure.rel r fun i => Semiterm.val s e ε' (v i)

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Structure.rel r fun i => Semiterm.val s e ε (v i)) ↔ Structure.rel r fun i => Semiterm.val s e ε' (v i)
Tactic:
apply iff_of_eq
State after:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Structure.rel r fun i => Semiterm.val s e ε (v i)) = Structure.rel r fun i => Semiterm.val s e ε' (v i)

State before:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Structure.rel r fun i => Semiterm.val s e ε (v i)) = Structure.rel r fun i => Semiterm.val s e ε' (v i)
Tactic:
congr
State after:
case a.e_a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (fun i => Semiterm.val s e ε (v i)) = fun i => Semiterm.val s e ε' (v i)

State before:
case a.e_a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (fun i => Semiterm.val s e ε (v i)) = fun i => Semiterm.val s e ε' (v i)
Tactic:
funext i
State after:
case a.e_a.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
i : Fin k
⊢ Semiterm.val s e ε (v i) = Semiterm.val s e ε' (v i)

State before:
case a.e_a.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
i : Fin k
⊢ Semiterm.val s e ε (v i) = Semiterm.val s e ε' (v i)
Tactic:
exact Semiterm.val_eq_of_funEqOn (v i) (fun x hx ↦ h x (by simp [fvarList]; exact ⟨i, hx⟩))
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ (fun x => x ∈ (rel r v).fvarList) x
Tactic:
simp [fvarList]
State after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ∃ a, x ∈ (v a).fvarList

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ∃ a, x ∈ (v a).fvarList
Tactic:
exact ⟨i, hx⟩
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (Eval s e ε) (nrel r v) ↔ (Eval s e ε') (nrel r v)
Tactic:
simp [eval_nrel]
State after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (v i)) ↔ ¬Structure.rel r fun i => Semiterm.val s e ε' (v i)

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (v i)) ↔ ¬Structure.rel r fun i => Semiterm.val s e ε' (v i)
Tactic:
apply iff_of_eq
State after:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (v i)) = ¬Structure.rel r fun i => Semiterm.val s e ε' (v i)

State before:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (v i)) = ¬Structure.rel r fun i => Semiterm.val s e ε' (v i)
Tactic:
congr
State after:
case a.e_a.e_a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (fun i => Semiterm.val s e ε (v i)) = fun i => Semiterm.val s e ε' (v i)

State before:
case a.e_a.e_a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (fun i => Semiterm.val s e ε (v i)) = fun i => Semiterm.val s e ε' (v i)
Tactic:
funext i
State after:
case a.e_a.e_a.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
i : Fin k
⊢ Semiterm.val s e ε (v i) = Semiterm.val s e ε' (v i)

State before:
case a.e_a.e_a.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
i : Fin k
⊢ Semiterm.val s e ε (v i) = Semiterm.val s e ε' (v i)
Tactic:
exact Semiterm.val_eq_of_funEqOn (v i) (fun x hx ↦ h x (by simp [fvarList]; exact ⟨i, hx⟩))
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ (fun x => x ∈ (nrel r v).fvarList) x
Tactic:
simp [fvarList]
State after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ∃ a, x ∈ (v a).fvarList

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ∃ a, x ∈ (v a).fvarList
Tactic:
exact ⟨i, hx⟩
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) (p ⋏ q) ↔ (Eval s e ε') (p ⋏ q)
Tactic:
simp
State after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) p ∧ (Eval s e ε) q ↔ (Eval s e ε') p ∧ (Eval s e ε') q

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) p ∧ (Eval s e ε) q ↔ (Eval s e ε') p ∧ (Eval s e ε') q
Tactic:
apply and_congr
State after:
case h₁
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p

case h₂
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) q ↔ (Eval s e ε') q

State before:
case h₁
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p
Tactic:
exact ihp (fun x (hx : x ∈ p.fvarList) ↦ h x $ by simp [hx, fvarList])
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
x : μ
hx : x ∈ p.fvarList
⊢ (fun x => x ∈ (p ⋏ q).fvarList) x
Tactic:
simp [hx, fvarList]
State after:
no goals

State before:
case h₂
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) q ↔ (Eval s e ε') q
Tactic:
exact ihq (fun x (hx : x ∈ q.fvarList) ↦ h x $ by simp [hx, fvarList])
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
x : μ
hx : x ∈ q.fvarList
⊢ (fun x => x ∈ (p ⋏ q).fvarList) x
Tactic:
simp [hx, fvarList]
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) (p ⋎ q) ↔ (Eval s e ε') (p ⋎ q)
Tactic:
simp
State after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) p ∨ (Eval s e ε) q ↔ (Eval s e ε') p ∨ (Eval s e ε') q

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) p ∨ (Eval s e ε) q ↔ (Eval s e ε') p ∨ (Eval s e ε') q
Tactic:
apply or_congr
State after:
case h₁
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p

case h₂
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) q ↔ (Eval s e ε') q

State before:
case h₁
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p
Tactic:
exact ihp (fun x (hx : x ∈ p.fvarList) ↦ h x $ by simp [hx, fvarList])
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
x : μ
hx : x ∈ p.fvarList
⊢ (fun x => x ∈ (p ⋎ q).fvarList) x
Tactic:
simp [hx, fvarList]
State after:
no goals

State before:
case h₂
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) q ↔ (Eval s e ε') q
Tactic:
exact ihq (fun x (hx : x ∈ q.fvarList) ↦ h x $ by simp [hx, fvarList])
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
x : μ
hx : x ∈ q.fvarList
⊢ (fun x => x ∈ (p ⋎ q).fvarList) x
Tactic:
simp [hx, fvarList]
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
⊢ (Eval s e ε) (∀' p) ↔ (Eval s e ε') (∀' p)
Tactic:
simp
State after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
⊢ (∀ (x : M), (Eval s (x :> e) ε) p) ↔ ∀ (x : M), (Eval s (x :> e) ε') p

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
⊢ (∀ (x : M), (Eval s (x :> e) ε) p) ↔ ∀ (x : M), (Eval s (x :> e) ε') p
Tactic:
apply forall_congr'
State after:
case h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
⊢ ∀ (a : M), (Eval s (a :> e) ε) p ↔ (Eval s (a :> e) ε') p

State before:
case h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
⊢ ∀ (a : M), (Eval s (a :> e) ε) p ↔ (Eval s (a :> e) ε') p
Tactic:
intro x
State after:
case h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
x : M
⊢ (Eval s (x :> e) ε) p ↔ (Eval s (x :> e) ε') p

State before:
case h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
x : M
⊢ (Eval s (x :> e) ε) p ↔ (Eval s (x :> e) ε') p
Tactic:
exact ih (fun x hx ↦ h _ $ by simp [fvar?]; exact hx)
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
x✝ : M
x : μ
hx : (fun x => x ∈ p.fvarList) x
⊢ (fun x => x ∈ (∀' p).fvarList) x
Tactic:
simp [fvar?]
State after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
x✝ : M
x : μ
hx : (fun x => x ∈ p.fvarList) x
⊢ x ∈ p.fvarList

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
x✝ : M
x : μ
hx : (fun x => x ∈ p.fvarList) x
⊢ x ∈ p.fvarList
Tactic:
exact hx
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
⊢ (Eval s e ε) (∃' p) ↔ (Eval s e ε') (∃' p)
Tactic:
simp
State after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
⊢ (∃ x, (Eval s (x :> e) ε) p) ↔ ∃ x, (Eval s (x :> e) ε') p

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
⊢ (∃ x, (Eval s (x :> e) ε) p) ↔ ∃ x, (Eval s (x :> e) ε') p
Tactic:
apply exists_congr
State after:
case h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
⊢ ∀ (a : M), (Eval s (a :> e) ε) p ↔ (Eval s (a :> e) ε') p

State before:
case h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
⊢ ∀ (a : M), (Eval s (a :> e) ε) p ↔ (Eval s (a :> e) ε') p
Tactic:
intro x
State after:
case h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
x : M
⊢ (Eval s (x :> e) ε) p ↔ (Eval s (x :> e) ε') p

State before:
case h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
x : M
⊢ (Eval s (x :> e) ε) p ↔ (Eval s (x :> e) ε') p
Tactic:
exact ih (fun x hx ↦ h _ $ by simp [fvar?]; exact hx)
State after:
no goals

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
x✝ : M
x : μ
hx : (fun x => x ∈ p.fvarList) x
⊢ (fun x => x ∈ (∃' p).fvarList) x
Tactic:
simp [fvar?]
State after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
x✝ : M
x : μ
hx : (fun x => x ∈ p.fvarList) x
⊢ x ∈ p.fvarList

State before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
x✝ : M
x : μ
hx : (fun x => x ∈ p.fvarList) x
⊢ x ∈ p.fvarList
Tactic:
exact hx
State after:
no goals