Theorem: Set.preimage_smul_setₑ' (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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
⊢ ⇑f ⁻¹' (φ m • t) = m • ⇑f ⁻¹' t
Tactic:
apply Set.Subset.antisymm
State after:
case h₁
α : 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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
⊢ ⇑f ⁻¹' (φ m • t) ⊆ m • ⇑f ⁻¹' t

case h₂
α : 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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
⊢ m • ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (φ m • t)

State before:
case h₂
α : 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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
⊢ m • ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (φ m • t)
Tactic:
exact preimage_smul_setₑ_le t
State after:
no goals

State before:
case h₁
α : 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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
⊢ ⇑f ⁻¹' (φ m • t) ⊆ m • ⇑f ⁻¹' t
Tactic:
rintro x ⟨y, yt, hy⟩
State after:
case h₁.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : (fun x => φ m • x) y = f x
⊢ x ∈ m • ⇑f ⁻¹' t

State before:
case h₁.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : (fun x => φ m • x) y = f x
⊢ x ∈ m • ⇑f ⁻¹' t
Tactic:
dsimp at hy
State after:
case h₁.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
⊢ x ∈ m • ⇑f ⁻¹' t

State before:
case h₁.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
⊢ x ∈ m • ⇑f ⁻¹' t
Tactic:
obtain ⟨x', hx' : m • x' = x⟩ := hmα.surjective x
State after:
case h₁.intro.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
x' : α
hx' : m • x' = x
⊢ x ∈ m • ⇑f ⁻¹' t

State before:
case h₁.intro.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
x' : α
hx' : m • x' = x
⊢ x ∈ m • ⇑f ⁻¹' t
Tactic:
refine ⟨x',  ?_, hx'⟩
State after:
case h₁.intro.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
x' : α
hx' : m • x' = x
⊢ x' ∈ ⇑f ⁻¹' t

State before:
case h₁.intro.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
x' : α
hx' : m • x' = x
⊢ x' ∈ ⇑f ⁻¹' t
Tactic:
simp only [← hx', map_smulₛₗ] at hy
State after:
case h₁.intro.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ x' ∈ ⇑f ⁻¹' t

State before:
case h₁.intro.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ x' ∈ ⇑f ⁻¹' t
Tactic:
simp only [mem_preimage]
State after:
case h₁.intro.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ f x' ∈ t

State before:
case h₁.intro.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ f x' ∈ t
Tactic:
rw [← hmβ.injective hy]
State after:
case h₁.intro.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ y ∈ t

State before:
case h₁.intro.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.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ y ∈ t
Tactic:
exact yt
State after:
no goals