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

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
⊢ semVars (subst φ f) ⊆ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)
Tactic:
intro v2 hv2
State after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 : v2 ∈ semVars (subst φ f)
⊢ v2 ∈ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 : v2 ∈ semVars (subst φ f)
⊢ v2 ∈ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)
Tactic:
unfold subst at hv2
State after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
⊢ v2 ∈ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
⊢ v2 ∈ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)
Tactic:
rw [Finset.mem_biUnion]
State after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
⊢ ∃ a ∈ semVars φ, v2 ∈ semVars (f a)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
⊢ ∃ a ∈ semVars φ, v2 ∈ semVars (f a)
Tactic:
have ⟨p,hp⟩ := φ.exists_rep
State after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
p : PropForm ν₁
hp : ⟦p⟧ = φ
⊢ ∃ a ∈ semVars φ, v2 ∈ semVars (f a)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
p : PropForm ν₁
hp : ⟦p⟧ = φ
⊢ ∃ a ∈ semVars φ, v2 ∈ semVars (f a)
Tactic:
cases hp
State after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ (Quotient.choice f)))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ (Quotient.choice f)))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
generalize hf' : Quotient.choice f = f' at hv2
State after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f' : Quotient inferInstance
hf' : Quotient.choice f = f'
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ f'))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f' : Quotient inferInstance
hf' : Quotient.choice f = f'
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ f'))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
have ⟨f'', hf''⟩ := f'.exists_rep
State after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f' : Quotient inferInstance
hf' : Quotient.choice f = f'
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ f'))
f'' : ν₁ → PropForm ν₂
hf'' : ⟦f''⟧ = f'
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f' : Quotient inferInstance
hf' : Quotient.choice f = f'
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ f'))
f'' : ν₁ → PropForm ν₂
hf'' : ⟦f''⟧ = f'
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
cases hf''
State after:
case refl.refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ ⟦f''⟧))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ ⟦f''⟧))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
simp [Quotient.lift_mk (s := .prod _ _)] at hv2
State after:
case refl.refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
hv2 : v2 ∈ semVars ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
hv2 : v2 ∈ semVars ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
rw [mem_semVars] at hv2
State after:
case refl.refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
hv2 : ∃ τ, τ ⊨ ⟦PropForm.subst p f''⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
hv2 : ∃ τ, τ ⊨ ⟦PropForm.subst p f''⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
rcases hv2 with ⟨τ,hsat,hunsat⟩
State after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : τ ⊨ ⟦PropForm.subst p f''⟧
hunsat : ¬(PropAssignment.set τ v2 !τ v2) ⊨ ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : τ ⊨ ⟦PropForm.subst p f''⟧
hunsat : ¬(PropAssignment.set τ v2 !τ v2) ⊨ ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
rw [satisfies_mk] at hsat hunsat
State after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : τ ⊨ PropForm.subst p f''
hunsat : ¬(PropAssignment.set τ v2 !τ v2) ⊨ PropForm.subst p f''
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : τ ⊨ PropForm.subst p f''
hunsat : ¬(PropAssignment.set τ v2 !τ v2) ⊨ PropForm.subst p f''
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
simp at hsat hunsat
State after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
have : ∀ x, ⟦f'' x⟧ = f x := by
  simp [Quotient.choice, piSetoid, instHasEquiv, Setoid.r] at hf'
  intro x; have := sound (hf' x); simp at this; simp [this]
State after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
this : ∀ (x : ν₁), ⟦f'' x⟧ = f x
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
this : ∀ (x : ν₁), ⟦f'' x⟧ = f x
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
simp [this] at hsat hunsat
State after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
this : ∀ (x : ν₁), ⟦f'' x⟧ = f x
hsat : PropAssignment.subst (fun x => f x) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
this : ∀ (x : ν₁), ⟦f'' x⟧ = f x
hsat : PropAssignment.subst (fun x => f x) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
clear this hf' f''
State after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
rw [← satisfies_mk] at hsat hunsat
State after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ ⟦p⟧
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ ⟦p⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ ⟦p⟧
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ ⟦p⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
have ⟨x,h1,h2⟩ := exists_semVar hsat hunsat
State after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ ⟦p⟧
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ ⟦p⟧
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ ⟦p⟧
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ ⟦p⟧
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
clear hsat hunsat
State after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)

State before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
use x
State after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ x ∈ semVars ⟦p⟧ ∧ v2 ∈ semVars (f x)

State before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ x ∈ semVars ⟦p⟧ ∧ v2 ∈ semVars (f x)
Tactic:
simp [h2]
State after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ v2 ∈ semVars (f x)

State before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ v2 ∈ semVars (f x)
Tactic:
clear h2
State after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
⊢ v2 ∈ semVars (f x)

State before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
⊢ v2 ∈ semVars (f x)
Tactic:
rw [mem_semVars]
State after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)

State before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
simp [PropAssignment.subst] at h1
State after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)

State before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
by_cases h : τ ⊨ f x
State after:
case pos
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : τ ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)

case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : ¬τ ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∀ (x : ν₁), ⟦f'' x⟧ = f x
Tactic:
simp [Quotient.choice, piSetoid, instHasEquiv, Setoid.r] at hf'
State after:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
⊢ ∀ (x : ν₁), ⟦f'' x⟧ = f x

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
⊢ ∀ (x : ν₁), ⟦f'' x⟧ = f x
Tactic:
intro x
State after:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
⊢ ⟦f'' x⟧ = f x

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
⊢ ⟦f'' x⟧ = f x
Tactic:
have := sound (hf' x)
State after:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
this : ⟦Quotient.out (f x)⟧ = ⟦f'' x⟧
⊢ ⟦f'' x⟧ = f x

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
this : ⟦Quotient.out (f x)⟧ = ⟦f'' x⟧
⊢ ⟦f'' x⟧ = f x
Tactic:
simp at this
State after:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
this : f x = ⟦f'' x⟧
⊢ ⟦f'' x⟧ = f x

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
this : f x = ⟦f'' x⟧
⊢ ⟦f'' x⟧ = f x
Tactic:
simp [this]
State after:
no goals

State before:
case pos
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : τ ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
use τ
State after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : τ ⊨ f x
⊢ τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)

State before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : τ ⊨ f x
⊢ τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
simp [h] at h1
State after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : τ ⊨ f x
h1 : ¬(PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)

State before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : τ ⊨ f x
h1 : ¬(PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
simp [*]
State after:
no goals

State before:
case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : ¬τ ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
simp [h] at h1
State after:
case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : ¬τ ⊨ f x
h1 : (PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)

State before:
case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : ¬τ ⊨ f x
h1 : (PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
refine ⟨_, h1, ?_⟩
State after:
case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : ¬τ ⊨ f x
h1 : (PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ (fun M φ => ¬M ⊨ φ) (PropAssignment.set (PropAssignment.set τ v2 !τ v2) v2 !PropAssignment.set τ v2 (!τ v2) v2) (f x)

State before:
case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : ¬τ ⊨ f x
h1 : (PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ (fun M φ => ¬M ⊨ φ) (PropAssignment.set (PropAssignment.set τ v2 !τ v2) v2 !PropAssignment.set τ v2 (!τ v2) v2) (f x)
Tactic:
simp [h]
State after:
no goals