Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited (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
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
⊢ (Evalf s Empty.elim) (∀ᶠ* p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
simp [Formula.fvUnivClosure, eval_rewriteMap]
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
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) ↔ ∀ (ε : μ → M), (Evalf s ε) 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
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
haveI : Inhabited μ := ⟨Classical.ofNonempty⟩
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
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) ↔ ∀ (ε : μ → M), (Evalf s ε) 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
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
constructor
State after:
case 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
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) → ∀ (ε : μ → M), (Evalf s ε) p

case 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
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (ε : μ → M), (Evalf s ε) p) → ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p

State before:
case 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
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) → ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
intro h ε
State after:
case 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
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
⊢ (Evalf s ε) p

State before:
case 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
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
⊢ (Evalf s ε) p
Tactic:
have := h (fun i ↦ ε $ Semiformula.fvListingInv _ i)
State after:
case 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
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
⊢ (Evalf s ε) p

State before:
case 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
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
⊢ (Evalf s ε) p
Tactic:
exact (eval_iff_of_funEqOn p (by intro x hx; simp [fvListingInv_fvListing hx])).mp this
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
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
⊢ Function.funEqOn (fvar? p) (fun x => ε (fvListingInv p (fvListing p x))) ε
Tactic:
intro x hx
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
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
x : μ
hx : fvar? p x
⊢ (fun x => ε (fvListingInv p (fvListing p x))) x = ε x

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
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
x : μ
hx : fvar? p x
⊢ (fun x => ε (fvListingInv p (fvListing p x))) x = ε x
Tactic:
simp [fvListingInv_fvListing hx]
State after:
no goals

State before:
case 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
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (ε : μ → M), (Evalf s ε) p) → ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
Tactic:
intro h e
State after:
case 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
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
h : ∀ (ε : μ → M), (Evalf s ε) p
e : Fin ((fvarList p).length + 1) → M
⊢ (Eval s ![] fun x => e (fvListing p x)) p

State before:
case 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
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
h : ∀ (ε : μ → M), (Evalf s ε) p
e : Fin ((fvarList p).length + 1) → M
⊢ (Eval s ![] fun x => e (fvListing p x)) p
Tactic:
exact h (fun x ↦ e $ Semiformula.fvListing p x)
State after:
no goals