Theorem: LeanSAT.Model.PropFun.entails_ofFun (LeanSAT/Model/OfFun.lean)

State before:
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ τ ⊨ ofFun p ↔ p τ = true
Tactic:
simp [SemanticEntails.entails, satisfies, ofFun]
State after:
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ

State before:
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ
Tactic:
apply Fintype.elim_elems_eq_forall (V := V)
State after:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L),
    Fintype.elim_elems ?f ?h = ?f L h1 h2 → eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ

case f
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → ?m.15443

case h
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), ?f L1 h1 h11 = ?f L2 h2 h22

V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ Type ?u.15442

State before:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L),
    Fintype.elim_elems ?f ?h = ?f L h1 h2 → eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ

case f
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → ?m.15443

case h
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), ?f L1 h1 h11 = ?f L2 h2 h22

V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ Type ?u.15442
Tactic:
intro L h1 h2 h'
State after:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
L : List V
h1 : ∀ (v : V), v ∈ L
h2 : List.Nodup L
h' : Fintype.elim_elems ?f ?h = ?f L h1 h2
⊢ eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ

case f
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → ?m.15443

case h
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), ?f L1 h1 h11 = ?f L2 h2 h22

V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ Type ?u.15442

State before:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
L : List V
h1 : ∀ (v : V), v ∈ L
h2 : List.Nodup L
h' : Fintype.elim_elems ?f ?h = ?f L h1 h2
⊢ eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ

case f
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → ?m.15443

case h
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), ?f L1 h1 h11 = ?f L2 h2 h22

V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ Type ?u.15442
Tactic:
rw [h']
State after:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
L : List V
h1 : ∀ (v : V), v ∈ L
h2 : List.Nodup L
h' : Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯ = ⟦PropForm.ofFun p L h1⟧
⊢ eval τ ⟦PropForm.ofFun p L h1⟧ = p τ

State before:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
L : List V
h1 : ∀ (v : V), v ∈ L
h2 : List.Nodup L
h' : Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯ = ⟦PropForm.ofFun p L h1⟧
⊢ eval τ ⟦PropForm.ofFun p L h1⟧ = p τ
Tactic:
simp
State after:
no goals