Theorem: LeanSAT.Model.PropAssignment.map_eq_map (LeanSAT/Model/PropAssn.lean)

State before:
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
⊢ map f τ = map f' τ' ↔ ∀ (v : ν), τ (f v) = τ' (f' v)
Tactic:
simp [map]
State after:
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
⊢ τ ∘ f = τ' ∘ f' ↔ ∀ (v : ν), τ (f v) = τ' (f' v)

State before:
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
⊢ τ ∘ f = τ' ∘ f' ↔ ∀ (v : ν), τ (f v) = τ' (f' v)
Tactic:
constructor <;> intro h
State after:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
⊢ ∀ (v : ν), τ (f v) = τ' (f' v)

case mpr
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : ∀ (v : ν), τ (f v) = τ' (f' v)
⊢ τ ∘ f = τ' ∘ f'

State before:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
⊢ ∀ (v : ν), τ (f v) = τ' (f' v)
Tactic:
intro v
State after:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
v : ν
⊢ τ (f v) = τ' (f' v)

State before:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
v : ν
⊢ τ (f v) = τ' (f' v)
Tactic:
have := congrFun h v
State after:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
v : ν
this : (τ ∘ f) v = (τ' ∘ f') v
⊢ τ (f v) = τ' (f' v)

State before:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
v : ν
this : (τ ∘ f) v = (τ' ∘ f') v
⊢ τ (f v) = τ' (f' v)
Tactic:
simp_all
State after:
no goals

State before:
case mpr
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : ∀ (v : ν), τ (f v) = τ' (f' v)
⊢ τ ∘ f = τ' ∘ f'
Tactic:
ext v
State after:
case mpr.h
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : ∀ (v : ν), τ (f v) = τ' (f' v)
v : ν
⊢ (τ ∘ f) v = (τ' ∘ f') v

State before:
case mpr.h
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : ∀ (v : ν), τ (f v) = τ' (f' v)
v : ν
⊢ (τ ∘ f) v = (τ' ∘ f') v
Tactic:
simp [*]
State after:
no goals