case a
F : Type ?u.755717
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
a✝ : γ
⊢ a✝ ∈ (op a • s) • t ↔ a✝ ∈ s • a • t
F : Type ?u.755717
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t
ext
no goals
case a
F : Type ?u.755717
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
a✝ : γ
⊢ a✝ ∈ (op a • s) • t ↔ a✝ ∈ s • a • t
simp [mem_smul, mem_smul_finset, h]