internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = f v1
Tactic:
simp [hf.eq_iff]
Proof state after:
case a.mp.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Tactic:
have := by rw [PropFun.mem_semVars] at h; exact h
Proof state after:
case a.mp.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
this : ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
this : ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Tactic:
rcases this with ⟨τ,hpos,hneg⟩
Proof state after:
case a.mp.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : τ ⊨ ⟦map f φ⟧
hneg : ¬(PropAssignment.set τ (f v1) !τ (f v1)) ⊨ ⟦map f φ⟧
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : τ ⊨ ⟦map f φ⟧
hneg : ¬(PropAssignment.set τ (f v1) !τ (f v1)) ⊨ ⟦map f φ⟧
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Tactic:
rw [PropFun.satisfies_mk] at hpos hneg
Proof state after:
case a.mp.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : τ ⊨ map f φ
hneg : ¬(PropAssignment.set τ (f v1) !τ (f v1)) ⊨ map f φ
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : τ ⊨ map f φ
hneg : ¬(PropAssignment.set τ (f v1) !τ (f v1)) ⊨ map f φ
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Tactic:
simp [satisfies_map] at hpos hneg
Proof state after:
case a.mp.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬PropAssignment.map f (PropAssignment.set τ (f v1) !τ (f v1)) ⊨ φ
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬PropAssignment.map f (PropAssignment.set τ (f v1) !τ (f v1)) ⊨ φ
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Tactic:
rw [PropAssignment.map_set (finj := hf)] at hneg
Proof state after:
case a.mp.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
⊢ v1 ∈ PropFun.semVars ⟦φ⟧
Tactic:
rw [PropFun.mem_semVars]
Proof state after:
case a.mp.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
⊢ ∃ τ, τ ⊨ ⟦φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v1 !τ v1) ⟦φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
⊢ ∃ τ, τ ⊨ ⟦φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v1 !τ v1) ⟦φ⟧
Tactic:
use PropAssignment.map f τ
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
⊢ PropAssignment.map f τ ⊨ ⟦φ⟧ ∧
    (fun M φ => ¬M ⊨ φ) (PropAssignment.set (PropAssignment.map f τ) v1 !PropAssignment.map f τ v1) ⟦φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
⊢ PropAssignment.map f τ ⊨ ⟦φ⟧ ∧
    (fun M φ => ¬M ⊨ φ) (PropAssignment.set (PropAssignment.map f τ) v1 !PropAssignment.map f τ v1) ⟦φ⟧
Tactic:
simp
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
⊢ PropAssignment.map f τ ⊨ ⟦φ⟧ ∧ ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ ⟦φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
⊢ PropAssignment.map f τ ⊨ ⟦φ⟧ ∧ ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ ⟦φ⟧
Tactic:
rw [PropFun.satisfies_mk, PropFun.satisfies_mk]
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
⊢ PropAssignment.map f τ ⊨ φ ∧ ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
⊢ PropAssignment.map f τ ⊨ φ ∧ ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
⊢ ?m.68983
Tactic:
rw [PropFun.mem_semVars] at h
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h✝ : f v1 ∈ PropFun.semVars ⟦map f φ⟧
h : ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
⊢ ?m.68983
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h✝ : f v1 ∈ PropFun.semVars ⟦map f φ⟧
h : ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
⊢ ?m.68983
Tactic:
exact h
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mpr
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ (∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2) → v2 ∈ PropFun.semVars ⟦map f φ⟧
Tactic:
rintro ⟨v1,hv1,rfl⟩
Proof state after:
case a.mpr.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
hv1 : v1 ∈ PropFun.semVars ⟦φ⟧
⊢ f v1 ∈ PropFun.semVars ⟦map f φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mpr.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
hv1 : v1 ∈ PropFun.semVars ⟦φ⟧
⊢ f v1 ∈ PropFun.semVars ⟦map f φ⟧
Tactic:
rw [PropFun.mem_semVars] at hv1 ⊢
Proof state after:
case a.mpr.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
hv1 : ∃ τ, τ ⊨ ⟦φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v1 !τ v1) ⟦φ⟧
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mpr.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
hv1 : ∃ τ, τ ⊨ ⟦φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v1 !τ v1) ⟦φ⟧
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Tactic:
rcases hv1 with ⟨τ,hpos,hneg⟩
Proof state after:
case a.mpr.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
τ : PropAssignment ν₁
hpos : τ ⊨ ⟦φ⟧
hneg : ¬(PropAssignment.set τ v1 !τ v1) ⊨ ⟦φ⟧
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mpr.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
τ : PropAssignment ν₁
hpos : τ ⊨ ⟦φ⟧
hneg : ¬(PropAssignment.set τ v1 !τ v1) ⊨ ⟦φ⟧
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Tactic:
rw [PropFun.satisfies_mk] at hpos hneg
Proof state after:
case a.mpr.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
τ : PropAssignment ν₁
hpos : τ ⊨ φ
hneg : ¬(PropAssignment.set τ v1 !τ v1) ⊨ φ
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mpr.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
τ : PropAssignment ν₁
hpos : τ ⊨ φ
hneg : ¬(PropAssignment.set τ v1 !τ v1) ⊨ φ
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Tactic:
have ⟨σ,h⟩ := τ.exists_preimage ⟨f,hf⟩
Proof state after:
case a.mpr.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
τ : PropAssignment ν₁
hpos : τ ⊨ φ
hneg : ¬(PropAssignment.set τ v1 !τ v1) ⊨ φ
σ : PropAssignment ν₂
h : τ = PropAssignment.map (⇑{ toFun := f, inj' := hf }) σ
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mpr.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
τ : PropAssignment ν₁
hpos : τ ⊨ φ
hneg : ¬(PropAssignment.set τ v1 !τ v1) ⊨ φ
σ : PropAssignment ν₂
h : τ = PropAssignment.map (⇑{ toFun := f, inj' := hf }) σ
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Tactic:
cases h
Proof state after:
case a.mpr.intro.intro.intro.intro.refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map (⇑{ toFun := f, inj' := hf }) σ ⊨ φ
hneg :
  ¬(PropAssignment.set (PropAssignment.map (⇑{ toFun := f, inj' := hf }) σ) v1
        !PropAssignment.map (⇑{ toFun := f, inj' := hf }) σ v1) ⊨
      φ
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mpr.intro.intro.intro.intro.refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map (⇑{ toFun := f, inj' := hf }) σ ⊨ φ
hneg :
  ¬(PropAssignment.set (PropAssignment.map (⇑{ toFun := f, inj' := hf }) σ) v1
        !PropAssignment.map (⇑{ toFun := f, inj' := hf }) σ v1) ⊨
      φ
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Tactic:
simp at hpos hneg
Proof state after:
case a.mpr.intro.intro.intro.intro.refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mpr.intro.intro.intro.intro.refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
Tactic:
use σ
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ σ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set σ (f v1) !σ (f v1)) ⟦map f φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ σ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set σ (f v1) !σ (f v1)) ⟦map f φ⟧
Tactic:
dsimp
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ σ ⊨ ⟦map f φ⟧ ∧ ¬(PropAssignment.set σ (f v1) !σ (f v1)) ⊨ ⟦map f φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ σ ⊨ ⟦map f φ⟧ ∧ ¬(PropAssignment.set σ (f v1) !σ (f v1)) ⊨ ⟦map f φ⟧
Tactic:
rw [PropFun.satisfies_mk, PropFun.satisfies_mk]
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ σ ⊨ map f φ ∧ ¬(PropAssignment.set σ (f v1) !σ (f v1)) ⊨ map f φ
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ σ ⊨ map f φ ∧ ¬(PropAssignment.set σ (f v1) !σ (f v1)) ⊨ map f φ
Tactic:
simp [satisfies_map, hpos]
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ ¬PropAssignment.map f (PropAssignment.set σ (f v1) !σ (f v1)) ⊨ φ
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ ¬PropAssignment.map f (PropAssignment.set σ (f v1) !σ (f v1)) ⊨ φ
Tactic:
rw [PropAssignment.map_set]
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ

case h.finj
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ Function.Injective f
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
Tactic:
exact hneg
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case h.finj
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
σ : PropAssignment ν₂
hpos : PropAssignment.map f σ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f σ) v1 !σ (f v1)) ⊨ φ
⊢ Function.Injective f
Tactic:
assumption
Proof state after:
no goals