Theorem: LeanSAT.Model.PropFun.var.inj (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
⊢ Function.Injective var
Tactic:
intro v1 v2 h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : var v1 = var v2
⊢ v1 = v2

State before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : var v1 = var v2
⊢ v1 = v2
Tactic:
rw [ext_iff] at h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ var v2
⊢ v1 = v2

State before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ var v2
⊢ v1 = v2
Tactic:
have := h (fun v => v = v1)
State after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ var v2
this : (fun v => decide (v = v1)) ⊨ var v1 ↔ (fun v => decide (v = v1)) ⊨ var v2
⊢ v1 = v2

State before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ var v2
this : (fun v => decide (v = v1)) ⊨ var v1 ↔ (fun v => decide (v = v1)) ⊨ var v2
⊢ v1 = v2
Tactic:
aesop
State after:
no goals