internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.eval_rel₂
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 2
t₁ t₂ : Semiterm L μ n
⊢ (Structure.rel r fun i => Semiterm.val s e ε (![t₁, t₂] i)) =
    Structure.rel r ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
congr
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 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₂]
Theorem: LO.FirstOrder.Semiformula.eval_rel₂
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 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
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 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
Theorem: LO.FirstOrder.Semiformula.eval_rel₂
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_nrel₀
Proof 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
r : L.Rel 0
⊢ (Eval s e ε) (nrel r ![]) ↔ ¬Structure.rel r ![]
Tactic:
simp [eval_nrel, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_nrel₁
Proof 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
r : L.Rel 1
t : Semiterm L μ n
⊢ (Eval s e ε) (nrel r ![t]) ↔ ¬Structure.rel r ![Semiterm.val s e ε t]
Tactic:
simp [eval_nrel]
Proof 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
r : L.Rel 1
t : Semiterm L μ n
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε t) ↔ ¬Structure.rel r ![Semiterm.val s e ε t]
Theorem: LO.FirstOrder.Semiformula.eval_nrel₁
Proof 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
r : L.Rel 1
t : Semiterm L μ n
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε t) ↔ ¬Structure.rel r ![Semiterm.val s e ε t]
Tactic:
apply of_eq
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 1
t : Semiterm L μ n
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε t) = ¬Structure.rel r ![Semiterm.val s e ε t]
Theorem: LO.FirstOrder.Semiformula.eval_nrel₁
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 1
t : Semiterm L μ n
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε t) = ¬Structure.rel r ![Semiterm.val s e ε t]
Tactic:
congr
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 1
t : Semiterm L μ n
⊢ (fun i => Semiterm.val s e ε t) = ![Semiterm.val s e ε t]
Theorem: LO.FirstOrder.Semiformula.eval_nrel₁
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 1
t : Semiterm L μ n
⊢ (fun i => Semiterm.val s e ε t) = ![Semiterm.val s e ε t]
Tactic:
funext i
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 1
t : Semiterm L μ n
i : Fin 1
⊢ Semiterm.val s e ε t = ![Semiterm.val s e ε t] i
Theorem: LO.FirstOrder.Semiformula.eval_nrel₁
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 1
t : Semiterm L μ n
i : Fin 1
⊢ Semiterm.val s e ε t = ![Semiterm.val s e ε t] i
Tactic:
cases' i using Fin.cases with i <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_nrel₂
Proof 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
r : L.Rel 2
t₁ t₂ : Semiterm L μ n
⊢ (Eval s e ε) (nrel r ![t₁, t₂]) ↔ ¬Structure.rel r ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
simp [eval_nrel]
Proof 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
r : L.Rel 2
t₁ t₂ : Semiterm L μ n
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (![t₁, t₂] i)) ↔
    ¬Structure.rel r ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Theorem: LO.FirstOrder.Semiformula.eval_nrel₂
Proof 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
r : L.Rel 2
t₁ t₂ : Semiterm L μ n
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (![t₁, t₂] i)) ↔
    ¬Structure.rel r ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
apply of_eq
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 2
t₁ t₂ : Semiterm L μ n
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (![t₁, t₂] i)) =
    ¬Structure.rel r ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Theorem: LO.FirstOrder.Semiformula.eval_nrel₂
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 2
t₁ t₂ : Semiterm L μ n
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (![t₁, t₂] i)) =
    ¬Structure.rel r ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
congr
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 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₂]
Theorem: LO.FirstOrder.Semiformula.eval_nrel₂
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 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
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 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
Theorem: LO.FirstOrder.Semiformula.eval_nrel₂
Proof 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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_ball
Proof 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
p q : Semiformula L μ (n + 1)
⊢ (Eval s e ε) (∀[p] q) ↔ ∀ (x : M), (Eval s (x :> e) ε) p → (Eval s (x :> e) ε) q
Tactic:
simp [LogicalConnective.ball]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_bex
Proof 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
p q : Semiformula L μ (n + 1)
⊢ (Eval s e ε) (∃[p] q) ↔ ∃ x, (Eval s (x :> e) ε) p ⋏ (Eval s (x :> e) ε) q
Tactic:
simp [LogicalConnective.bex]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_univClosure
Proof 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' : ℕ
e' : Fin 0 → M
p : Semiformula L μ n'
⊢ (Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (Eval s e ε) p
Tactic:
induction' n' with n' ih generalizing e' <;> simp [*, eq_finZeroElim, univClosure_succ]
Proof state after:
case succ
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∀ (e : Fin n' → M) (x : M), (Eval s (x :> e) ε) p) ↔ ∀ (e : Fin (n' + 1) → M), (Eval s e ε) p
Theorem: LO.FirstOrder.Semiformula.eval_univClosure
Proof state before:
case succ
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∀ (e : Fin n' → M) (x : M), (Eval s (x :> e) ε) p) ↔ ∀ (e : Fin (n' + 1) → M), (Eval s e ε) p
Tactic:
constructor
Proof state after:
case succ.mp
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∀ (e : Fin n' → M) (x : M), (Eval s (x :> e) ε) p) → ∀ (e : Fin (n' + 1) → M), (Eval s e ε) p

case succ.mpr
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∀ (e : Fin (n' + 1) → M), (Eval s e ε) p) → ∀ (e : Fin n' → M) (x : M), (Eval s (x :> e) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_univClosure
Proof state before:
case succ.mp
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∀ (e : Fin n' → M) (x : M), (Eval s (x :> e) ε) p) → ∀ (e : Fin (n' + 1) → M), (Eval s e ε) p
Tactic:
intro h e
Proof state after:
case succ.mp
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
h : ∀ (e : Fin n' → M) (x : M), (Eval s (x :> e) ε) p
e : Fin (n' + 1) → M
⊢ (Eval s e ε) p
Theorem: LO.FirstOrder.Semiformula.eval_univClosure
Proof state before:
case succ.mp
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
h : ∀ (e : Fin n' → M) (x : M), (Eval s (x :> e) ε) p
e : Fin (n' + 1) → M
⊢ (Eval s e ε) p
Tactic:
simpa using h (Matrix.vecTail e) (Matrix.vecHead e)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_univClosure
Proof state before:
case succ.mpr
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∀ (e : Fin (n' + 1) → M), (Eval s e ε) p) → ∀ (e : Fin n' → M) (x : M), (Eval s (x :> e) ε) p
Tactic:
intro h e x
Proof state after:
case succ.mpr
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
h : ∀ (e : Fin (n' + 1) → M), (Eval s e ε) p
e : Fin n' → M
x : M
⊢ (Eval s (x :> e) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_univClosure
Proof state before:
case succ.mpr
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
h : ∀ (e : Fin (n' + 1) → M), (Eval s e ε) p
e : Fin n' → M
x : M
⊢ (Eval s (x :> e) ε) p
Tactic:
exact h (x :> e)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_exClosure
Proof 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' : ℕ
e' : Fin 0 → M
p : Semiformula L μ n'
⊢ (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
Tactic:
induction' n' with n' ih generalizing e' <;> simp [*, eq_finZeroElim, exClosure_succ]
Proof state after:
case succ
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∃ e x, (Eval s (x :> e) ε) p) ↔ ∃ e, (Eval s e ε) p
Theorem: LO.FirstOrder.Semiformula.eval_exClosure
Proof state before:
case succ
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∃ e x, (Eval s (x :> e) ε) p) ↔ ∃ e, (Eval s e ε) p
Tactic:
constructor
Proof state after:
case succ.mp
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∃ e x, (Eval s (x :> e) ε) p) → ∃ e, (Eval s e ε) p

case succ.mpr
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∃ e, (Eval s e ε) p) → ∃ e x, (Eval s (x :> e) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_exClosure
Proof state before:
case succ.mp
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∃ e x, (Eval s (x :> e) ε) p) → ∃ e, (Eval s e ε) p
Tactic:
rintro ⟨e, x, h⟩
Proof state after:
case succ.mp.intro.intro
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
e : Fin n' → M
x : M
h : (Eval s (x :> e) ε) p
⊢ ∃ e, (Eval s e ε) p
Theorem: LO.FirstOrder.Semiformula.eval_exClosure
Proof state before:
case succ.mp.intro.intro
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
e : Fin n' → M
x : M
h : (Eval s (x :> e) ε) p
⊢ ∃ e, (Eval s e ε) p
Tactic:
exact ⟨x :> e, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_exClosure
Proof state before:
case succ.mpr
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
⊢ (∃ e, (Eval s e ε) p) → ∃ e x, (Eval s (x :> e) ε) p
Tactic:
rintro ⟨e, h⟩
Proof state after:
case succ.mpr.intro
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
e : Fin (n' + 1) → M
h : (Eval s e ε) p
⊢ ∃ e x, (Eval s (x :> e) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_exClosure
Proof state before:
case succ.mpr.intro
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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
e : Fin (n' + 1) → M
h : (Eval s e ε) p
⊢ ∃ e x, (Eval s (x :> e) ε) p
Tactic:
exact ⟨Matrix.vecTail e, Matrix.vecHead e, by simpa using h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_exClosure
Proof 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' : ℕ
ih : ∀ {e' : Fin 0 → M} {p : Semiformula L μ n'}, (Eval s e' ε) (∃* p) ↔ ∃ e, (Eval s e ε) p
e' : Fin 0 → M
p : Semiformula L μ (n' + 1)
e : Fin (n' + 1) → M
h : (Eval s e ε) p
⊢ (Eval s (Matrix.vecHead e :> Matrix.vecTail e) ε) p
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_univItr
Proof 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
k : ℕ
e : Fin n → M
p : Semiformula L μ (n + k)
⊢ (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
Tactic:
induction' k with k ih generalizing e <;> simp [*, Matrix.empty_eq, univItr_succ]
Proof state after:
case succ
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
k : ℕ
ih :
  ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)},
    (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∀ (e' : Fin k → M) (x : M), (Eval s (x :> Matrix.appendr e' e) ε) p) ↔
    ∀ (e' : Fin (k + 1) → M), (Eval s (Matrix.appendr e' e) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_univItr
Proof state before:
case succ
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
k : ℕ
ih :
  ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)},
    (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∀ (e' : Fin k → M) (x : M), (Eval s (x :> Matrix.appendr e' e) ε) p) ↔
    ∀ (e' : Fin (k + 1) → M), (Eval s (Matrix.appendr e' e) ε) p
Tactic:
constructor
Proof state after:
case succ.mp
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
k : ℕ
ih :
  ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)},
    (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∀ (e' : Fin k → M) (x : M), (Eval s (x :> Matrix.appendr e' e) ε) p) →
    ∀ (e' : Fin (k + 1) → M), (Eval s (Matrix.appendr e' e) ε) p

case succ.mpr
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
k : ℕ
ih :
  ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)},
    (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∀ (e' : Fin (k + 1) → M), (Eval s (Matrix.appendr e' e) ε) p) →
    ∀ (e' : Fin k → M) (x : M), (Eval s (x :> Matrix.appendr e' e) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_univItr
Proof state before:
case succ.mp
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
k : ℕ
ih :
  ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)},
    (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∀ (e' : Fin k → M) (x : M), (Eval s (x :> Matrix.appendr e' e) ε) p) →
    ∀ (e' : Fin (k + 1) → M), (Eval s (Matrix.appendr e' e) ε) p
Tactic:
intro h e'
Proof state after:
case succ.mp
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
k : ℕ
ih :
  ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)},
    (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
h : ∀ (e' : Fin k → M) (x : M), (Eval s (x :> Matrix.appendr e' e) ε) p
e' : Fin (k + 1) → M
⊢ (Eval s (Matrix.appendr e' e) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_univItr
Proof state before:
case succ.mp
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
k : ℕ
ih :
  ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)},
    (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
h : ∀ (e' : Fin k → M) (x : M), (Eval s (x :> Matrix.appendr e' e) ε) p
e' : Fin (k + 1) → M
⊢ (Eval s (Matrix.appendr e' e) ε) p
Tactic:
exact Eval.of_eq (h (Matrix.vecTail e') (Matrix.vecHead e'))
  (by rw [←Matrix.appendr_cons, Matrix.cons_head_tail]) rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_univItr
Proof 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
k : ℕ
ih :
  ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)},
    (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
h : ∀ (e' : Fin k → M) (x : M), (Eval s (x :> Matrix.appendr e' e) ε) p
e' : Fin (k + 1) → M
⊢ Matrix.vecHead e' :> Matrix.appendr (Matrix.vecTail e') e = Matrix.appendr e' e
Tactic:
rw [←Matrix.appendr_cons, Matrix.cons_head_tail]
Proof state after:
no goals