Theorem: LeanSAT.Model.PropForm.semVars_map (LeanSAT/Model/Subst.lean)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
⊢ PropFun.semVars ⟦map f φ⟧ = Finset.map { toFun := f, inj' := hf } (PropFun.semVars ⟦φ⟧)
Tactic:
ext v2
State after:
case a
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ ↔ v2 ∈ Finset.map { toFun := f, inj' := hf } (PropFun.semVars ⟦φ⟧)

State before:
case a
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ ↔ v2 ∈ Finset.map { toFun := f, inj' := hf } (PropFun.semVars ⟦φ⟧)
Tactic:
simp
State after:
case a
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ ↔ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2

State before:
case a
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ ↔ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Tactic:
constructor
State after:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ → ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2

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 φ⟧

State before:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ → ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Tactic:
intro h
State after:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2

State before:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Tactic:
have isVar : v2 ∈ vars (map f φ) := semVars_subset_vars _ h
State after:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
isVar : v2 ∈ vars (map f φ)
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2

State before:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
isVar : v2 ∈ vars (map f φ)
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Tactic:
simp at isVar
State after:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
isVar : ∃ a ∈ vars φ, f a = v2
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2

State before:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
isVar : ∃ a ∈ vars φ, f a = v2
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Tactic:
rcases isVar with ⟨v1, _, rfl⟩
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 φ⟧
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = f v1

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]
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 ⟦φ⟧

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
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 ⟦φ⟧

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⟩
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 ⟦φ⟧

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
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 ⟦φ⟧

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
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 ⟦φ⟧

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
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 ⟦φ⟧

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]
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) ⟦φ⟧

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 τ
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) ⟦φ⟧

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
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)) ⊨ ⟦φ⟧

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]
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)) ⊨ φ

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 [*]
State after:
no goals

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
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

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
State after:
no goals

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⟩
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 φ⟧

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 ⊢
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 φ⟧

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⟩
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 φ⟧

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
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 φ⟧

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⟩
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 φ⟧

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
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 φ⟧

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
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 φ⟧

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 σ
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 φ⟧

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
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 φ⟧

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]
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 φ

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]
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)) ⊨ φ

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]
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

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
State after:
no goals

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
State after:
no goals