Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul (Jordan/Blocks.lean)

State before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ g • Subtype.val '' B = Subtype.val '' (g • B)
Tactic:
ext
State after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ g • Subtype.val '' B ↔ x✝ ∈ Subtype.val '' (g • B)

State before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ g • Subtype.val '' B ↔ x✝ ∈ Subtype.val '' (g • B)
Tactic:
constructor
State after:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ g • Subtype.val '' B → x✝ ∈ Subtype.val '' (g • B)

case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ Subtype.val '' (g • B) → x✝ ∈ g • Subtype.val '' B

State before:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ g • Subtype.val '' B → x✝ ∈ Subtype.val '' (g • B)
Tactic:
intro hx
State after:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
hx : x✝ ∈ g • Subtype.val '' B
⊢ x✝ ∈ Subtype.val '' (g • B)

State before:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
hx : x✝ ∈ g • Subtype.val '' B
⊢ x✝ ∈ Subtype.val '' (g • B)
Tactic:
obtain ⟨y, hy, rfl⟩ := hx
State after:
case h.mp.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
y : X
hy : y ∈ Subtype.val '' B
⊢ (fun x => g • x) y ∈ Subtype.val '' (g • B)

State before:
case h.mp.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
y : X
hy : y ∈ Subtype.val '' B
⊢ (fun x => g • x) y ∈ Subtype.val '' (g • B)
Tactic:
obtain ⟨z, hz, rfl⟩ := hy
State after:
case h.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z ∈ Subtype.val '' (g • B)

State before:
case h.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z ∈ Subtype.val '' (g • B)
Tactic:
use g • z
State after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • z ∈ g • B ∧ ↑(g • z) = (fun x => g • x) ↑z

State before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • z ∈ g • B ∧ ↑(g • z) = (fun x => g • x) ↑z
Tactic:
constructor
State after:
case h.left
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • z ∈ g • B

case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑(g • z) = (fun x => g • x) ↑z

State before:
case h.left
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • z ∈ g • B

case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑(g • z) = (fun x => g • x) ↑z
Tactic:
exact ⟨z, hz, rfl⟩
State after:
case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑(g • z) = (fun x => g • x) ↑z

State before:
case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑(g • z) = (fun x => g • x) ↑z
Tactic:
rw [SubMulAction.val_smul_of_tower]
State after:
no goals

State before:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ Subtype.val '' (g • B) → x✝ ∈ g • Subtype.val '' B
Tactic:
intro hx
State after:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
hx : x✝ ∈ Subtype.val '' (g • B)
⊢ x✝ ∈ g • Subtype.val '' B

State before:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
hx : x✝ ∈ Subtype.val '' (g • B)
⊢ x✝ ∈ g • Subtype.val '' B
Tactic:
obtain ⟨y, hy, rfl⟩ := hx
State after:
case h.mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
y : ↥C
hy : y ∈ g • B
⊢ ↑y ∈ g • Subtype.val '' B

State before:
case h.mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
y : ↥C
hy : y ∈ g • B
⊢ ↑y ∈ g • Subtype.val '' B
Tactic:
obtain ⟨z, hz, rfl⟩ := hy
State after:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑((fun x => g • x) z) ∈ g • Subtype.val '' B

State before:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑((fun x => g • x) z) ∈ g • Subtype.val '' B
Tactic:
rw [SubMulAction.val_smul_of_tower]
State after:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • ↑z ∈ g • Subtype.val '' B

State before:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • ↑z ∈ g • Subtype.val '' B
Tactic:
use ↑z
State after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑z ∈ Subtype.val '' B ∧ (fun x => g • x) ↑z = g • ↑z

State before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑z ∈ Subtype.val '' B ∧ (fun x => g • x) ↑z = g • ↑z
Tactic:
constructor
State after:
case h.left
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑z ∈ Subtype.val '' B

case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z = g • ↑z

State before:
case h.left
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑z ∈ Subtype.val '' B

case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z = g • ↑z
Tactic:
exact ⟨z, hz, rfl⟩
State after:
case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z = g • ↑z

State before:
case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z = g • ↑z
Tactic:
rfl
State after:
no goals