Lean4
/-- If `G` acts on `A`, then it acts also on `A → B`, by `(g • F) a = F (g⁻¹ • a)`. -/
@[to_additive (attr := simps) arrowAddAction /--
If `G` acts on `A`, then it acts also on `A → B`, by `(g +ᵥ F) a = F (g⁻¹ +ᵥ a)` -/
]
def arrowAction : MulAction G (A → B) where
smul g F a := F (g⁻¹ • a)
one_smul
f := by
change (fun x => f ((1 : G)⁻¹ • x)) = f
simp only [inv_one, one_smul]
mul_smul x y
f := by
change (fun a => f ((x * y)⁻¹ • a)) = (fun a => f (y⁻¹ • x⁻¹ • a))
simp only [mul_smul, mul_inv_rev]