Theorem: LeanSAT.Model.PropFun.satisfies_subst (LeanSAT/Model/Subst.lean)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ subst φ f ↔ PropAssignment.subst f τ ⊨ φ
Tactic:
unfold subst
State after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)) ↔
    PropAssignment.subst f τ ⊨ φ

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)) ↔
    PropAssignment.subst f τ ⊨ φ
Tactic:
generalize hq : φ.prod (Quotient.choice f) = q
State after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
q : Quotient (Setoid.prod (setoid ν₁) inferInstance)
hq : Quotient.prod φ (Quotient.choice f) = q
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ q ↔
    PropAssignment.subst f τ ⊨ φ

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
q : Quotient (Setoid.prod (setoid ν₁) inferInstance)
hq : Quotient.prod φ (Quotient.choice f) = q
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ q ↔
    PropAssignment.subst f τ ⊨ φ
Tactic:
rcases q.exists_rep with ⟨⟨p, f'⟩, rfl⟩
State after:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ ⟦(p, f')⟧ ↔
    PropAssignment.subst f τ ⊨ φ

State before:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ ⟦(p, f')⟧ ↔
    PropAssignment.subst f τ ⊨ φ
Tactic:
simp [Quotient.lift_mk (s := .prod _ _)]
State after:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ τ ⊨ ⟦PropForm.subst p f'⟧ ↔ PropAssignment.subst f τ ⊨ φ

State before:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ τ ⊨ ⟦PropForm.subst p f'⟧ ↔ PropAssignment.subst f τ ⊨ φ
Tactic:
rw [satisfies_mk, PropForm.satisfies_subst, ← satisfies_mk]
State after:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ φ

State before:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ φ
Tactic:
rw [Quotient.prod_eq_mk] at hq
State after:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : φ = ⟦p⟧ ∧ Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ φ

State before:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : φ = ⟦p⟧ ∧ Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ φ
Tactic:
rcases hq with ⟨rfl,hq⟩
State after:
case intro.mk.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ ⟦p⟧

State before:
case intro.mk.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ ⟦p⟧
Tactic:
apply iff_of_eq
State after:
case intro.mk.intro.a
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ = PropAssignment.subst f τ ⊨ ⟦p⟧

State before:
case intro.mk.intro.a
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ = PropAssignment.subst f τ ⊨ ⟦p⟧
Tactic:
congr
State after:
case intro.mk.intro.a.e_a
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ = PropAssignment.subst f τ

State before:
case intro.mk.intro.a.e_a
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ = PropAssignment.subst f τ
Tactic:
apply congrFun
State after:
case intro.mk.intro.a.e_a.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ (PropAssignment.subst fun x => ⟦f' x⟧) = fun {τ} => PropAssignment.subst f τ

State before:
case intro.mk.intro.a.e_a.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ (PropAssignment.subst fun x => ⟦f' x⟧) = fun {τ} => PropAssignment.subst f τ
Tactic:
apply congrArg
State after:
case intro.mk.intro.a.e_a.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ (fun x => ⟦f' x⟧) = f

State before:
case intro.mk.intro.a.e_a.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ (fun x => ⟦f' x⟧) = f
Tactic:
funext x
State after:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
x : ν₁
⊢ ⟦f' x⟧ = f x

State before:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
x : ν₁
⊢ ⟦f' x⟧ = f x
Tactic:
simp [Quotient.choice] at hq
State after:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
⊢ ⟦f' x⟧ = f x

State before:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
⊢ ⟦f' x⟧ = f x
Tactic:
have := Quotient.sound (hq x)
State after:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
this : ⟦(fun i => Quotient.out (f i)) x⟧ = ⟦f' x⟧
⊢ ⟦f' x⟧ = f x

State before:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
this : ⟦(fun i => Quotient.out (f i)) x⟧ = ⟦f' x⟧
⊢ ⟦f' x⟧ = f x
Tactic:
simp at this
State after:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
this : f x = ⟦f' x⟧
⊢ ⟦f' x⟧ = f x

State before:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
this : f x = ⟦f' x⟧
⊢ ⟦f' x⟧ = f x
Tactic:
exact this.symm
State after:
no goals