Theorem: Set.image_smul_setₑ (Jordan/EquivariantMap.lean)

State before:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ ⇑f '' (m • s) = φ m • ⇑f '' s
Tactic:
change f.toFun '' ((fun a => m • a) '' s) = (fun b => φ m • b) '' (f.toFun '' s)
State after:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ f.toFun '' ((fun a => m • a) '' s) = (fun b => φ m • b) '' (f.toFun '' s)

State before:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ f.toFun '' ((fun a => m • a) '' s) = (fun b => φ m • b) '' (f.toFun '' s)
Tactic:
simp only [Set.image_image]
State after:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ (fun x => f.toFun (m • x)) '' s = (fun x => φ m • f.toFun x) '' s

State before:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ (fun x => f.toFun (m • x)) '' s = (fun x => φ m • f.toFun x) '' s
Tactic:
apply Set.image_congr
State after:
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ ∀ a ∈ s, f.toFun (m • a) = φ m • f.toFun a

State before:
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ ∀ a ∈ s, f.toFun (m • a) = φ m • f.toFun a
Tactic:
intro a _
State after:
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
a : α
a✝ : a ∈ s
⊢ f.toFun (m • a) = φ m • f.toFun a

State before:
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
a : α
a✝ : a ∈ s
⊢ f.toFun (m • a) = φ m • f.toFun a
Tactic:
rw [f.map_smul']
State after:
no goals