internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
by_cases h₁' : σ₁' ⊨ φ
Proof state after:
case pos
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ

case neg
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : ¬σ₁' ⊨ φ
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : ¬σ₁' ⊨ φ
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
case neg =>
  use x₀, σ₁
  simp [h₁, h₁']
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
case pos =>
  have hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x := fun x hMem => by
    have hX : x₀ ≠ x := fun h => hx₀ (h ▸ hMem)
    simp only [σ₁', σ₁.set_get_of_ne (!σ₁ x₀) hX]
    exact hS _ (Finset.mem_insert_of_mem hMem)
  have hSC' : ∀ x ∈ φ.vars \ s', σ₁' x = σ₂ x := fun x hMem => by
    by_cases hX : x₀ = x
    case pos =>
      have := hS _ (Finset.mem_insert_self _ _)
      simp only [σ₁', ← hX, PropAssignment.set_get, Bool.bnot_eq,
                  this, not_false_eq_true]
    case neg =>
      simp only [σ₁', σ₁.set_get_of_ne _ hX]
      aesop
  have ⟨x, τ, hx, H⟩ := ih h₁' hS' hSC'
  exact ⟨x, τ, Finset.mem_insert_of_mem hx, H⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : ¬σ₁' ⊨ φ
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
use x₀, σ₁
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : ¬σ₁' ⊨ φ
⊢ x₀ ∈ insert x₀ s' ∧ σ₁ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set σ₁ x₀ !σ₁ x₀) φ
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : ¬σ₁' ⊨ φ
⊢ x₀ ∈ insert x₀ s' ∧ σ₁ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set σ₁ x₀ !σ₁ x₀) φ
Tactic:
simp [h₁, h₁']
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
have hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x := fun x hMem => by
  have hX : x₀ ≠ x := fun h => hx₀ (h ▸ hMem)
  simp only [σ₁', σ₁.set_get_of_ne (!σ₁ x₀) hX]
  exact hS _ (Finset.mem_insert_of_mem hMem)
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
have hSC' : ∀ x ∈ φ.vars \ s', σ₁' x = σ₂ x := fun x hMem => by
  by_cases hX : x₀ = x
  case pos =>
    have := hS _ (Finset.mem_insert_self _ _)
    simp only [σ₁', ← hX, PropAssignment.set_get, Bool.bnot_eq,
                this, not_false_eq_true]
  case neg =>
    simp only [σ₁', σ₁.set_get_of_ne _ hX]
    aesop
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
hSC' : ∀ x ∈ vars φ \ s', σ₁' x = σ₂ x
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
hSC' : ∀ x ∈ vars φ \ s', σ₁' x = σ₂ x
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
have ⟨x, τ, hx, H⟩ := ih h₁' hS' hSC'
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
hSC' : ∀ x ∈ vars φ \ s', σ₁' x = σ₂ x
x : ν
τ : PropAssignment ν
hx : x ∈ s'
H : τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
hSC' : ∀ x ∈ vars φ \ s', σ₁' x = σ₂ x
x : ν
τ : PropAssignment ν
hx : x ∈ s'
H : τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
exact ⟨x, τ, Finset.mem_insert_of_mem hx, H⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
x : ν
hMem : x ∈ s'
⊢ σ₁' x ≠ σ₂ x
Tactic:
have hX : x₀ ≠ x := fun h => hx₀ (h ▸ hMem)
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
x : ν
hMem : x ∈ s'
hX : x₀ ≠ x
⊢ σ₁' x ≠ σ₂ x
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
x : ν
hMem : x ∈ s'
hX : x₀ ≠ x
⊢ σ₁' x ≠ σ₂ x
Tactic:
simp only [σ₁', σ₁.set_get_of_ne (!σ₁ x₀) hX]
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
x : ν
hMem : x ∈ s'
hX : x₀ ≠ x
⊢ σ₁ x ≠ σ₂ x
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
x : ν
hMem : x ∈ s'
hX : x₀ ≠ x
⊢ σ₁ x ≠ σ₂ x
Tactic:
exact hS _ (Finset.mem_insert_of_mem hMem)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
x : ν
hMem : x ∈ vars φ \ s'
⊢ σ₁' x = σ₂ x
Tactic:
by_cases hX : x₀ = x
Proof state after:
case pos
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
x : ν
hMem : x ∈ vars φ \ s'
hX : x₀ = x
⊢ σ₁' x = σ₂ x

case neg
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
x : ν
hMem : x ∈ vars φ \ s'
hX : ¬x₀ = x
⊢ σ₁' x = σ₂ x
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
x : ν
hMem : x ∈ vars φ \ s'
hX : x₀ = x
⊢ σ₁' x = σ₂ x
Tactic:
case pos =>
  have := hS _ (Finset.mem_insert_self _ _)
  simp only [σ₁', ← hX, PropAssignment.set_get, Bool.bnot_eq,
              this, not_false_eq_true]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
x : ν
hMem : x ∈ vars φ \ s'
hX : ¬x₀ = x
⊢ σ₁' x = σ₂ x
Tactic:
case neg =>
  simp only [σ₁', σ₁.set_get_of_ne _ hX]
  aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
x : ν
hMem : x ∈ vars φ \ s'
hX : x₀ = x
⊢ σ₁' x = σ₂ x
Tactic:
have := hS _ (Finset.mem_insert_self _ _)
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
x : ν
hMem : x ∈ vars φ \ s'
hX : x₀ = x
this : σ₁ x₀ ≠ σ₂ x₀
⊢ σ₁' x = σ₂ x
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
x : ν
hMem : x ∈ vars φ \ s'
hX : x₀ = x
this : σ₁ x₀ ≠ σ₂ x₀
⊢ σ₁' x = σ₂ x
Tactic:
simp only [σ₁', ← hX, PropAssignment.set_get, Bool.bnot_eq,
            this, not_false_eq_true]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
x : ν
hMem : x ∈ vars φ \ s'
hX : ¬x₀ = x
⊢ σ₁' x = σ₂ x
Tactic:
simp only [σ₁', σ₁.set_get_of_ne _ hX]
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
x : ν
hMem : x ∈ vars φ \ s'
hX : ¬x₀ = x
⊢ σ₁ x = σ₂ x
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
x : ν
hMem : x ∈ vars φ \ s'
hX : ¬x₀ = x
⊢ σ₁ x = σ₂ x
Tactic:
aesop
Proof state after:
no goals