case h
α : Type u_3
β : Type u_2
γ : Type u_1
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
f : β → γ
x : β
⊢ (x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f
α : Type u_3
β : Type u_2
γ : Type u_1
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
f : β → γ
⊢ (support fun x => f (c⁻¹ • x)) = c • support f
ext x
no goals
case h
α : Type u_3
β : Type u_2
γ : Type u_1
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
f : β → γ
x : β
⊢ (x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f
simp only [mem_smul_set_iff_inv_smul_mem, mem_support]