Theorem: Set.preimage_smul_setₑ_le (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 : α →ₑ[φ] β
β₁ : Type ?u.2413
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
t : Set β
⊢ m • ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (φ m • t)
Tactic:
rintro x ⟨y, hy, rfl⟩
State after:
case intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.2413
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
t : Set β
y : α
hy : y ∈ ⇑f ⁻¹' t
⊢ (fun x => m • x) y ∈ ⇑f ⁻¹' (φ m • t)

State before:
case intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.2413
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
t : Set β
y : α
hy : y ∈ ⇑f ⁻¹' t
⊢ (fun x => m • x) y ∈ ⇑f ⁻¹' (φ m • t)
Tactic:
refine ⟨f y, hy, (by rw [map_smulₛₗ])⟩
State after:
no goals

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 : α →ₑ[φ] β
β₁ : Type ?u.2413
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
t : Set β
y : α
hy : y ∈ ⇑f ⁻¹' t
⊢ (fun x => φ m • x) (f y) = f ((fun x => m • x) y)
Tactic:
rw [map_smulₛₗ]
State after:
no goals