[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
f : β → γ
⊢ (mulSupport fun x => f (c⁻¹ • x)) = c • mulSupport f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
f : β → γ
x : β
⊢ (x ∈ mulSupport fun x => f (c⁻¹ • x)) ↔ x ∈ c • mulSupport f
[PROOFSTEP]
simp only [mem_smul_set_iff_inv_smul_mem, mem_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
f : β → γ
⊢ (support fun x => f (c⁻¹ • x)) = c • support f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
f : β → γ
x : β
⊢ (x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f
[PROOFSTEP]
simp only [mem_smul_set_iff_inv_smul_mem, mem_support]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
hc : c ≠ 0
f : β → γ
⊢ (mulSupport fun x => f (c⁻¹ • x)) = c • mulSupport f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
hc : c ≠ 0
f : β → γ
x : β
⊢ (x ∈ mulSupport fun x => f (c⁻¹ • x)) ↔ x ∈ c • mulSupport f
[PROOFSTEP]
simp only [mem_smul_set_iff_inv_smul_mem₀ hc, mem_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
hc : c ≠ 0
f : β → γ
⊢ (support fun x => f (c⁻¹ • x)) = c • support f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
hc : c ≠ 0
f : β → γ
x : β
⊢ (x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f
[PROOFSTEP]
simp only [mem_smul_set_iff_inv_smul_mem₀ hc, mem_support]
