Theorem: isTrivialBlock_of_block_iff (Jordan/Primitive.lean)

State before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock B ↔ IsTrivialBlock (g • B)
Tactic:
constructor
State after:
case mp
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock B → IsTrivialBlock (g • B)

case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B

State before:
case mp
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock B → IsTrivialBlock (g • B)

case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B
Tactic:
exact isTrivialBlock_of_block g
State after:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B

State before:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B
Tactic:
intro hgB
State after:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock B

State before:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock B
Tactic:
rw [← inv_smul_smul g B]
State after:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g⁻¹ • g • B)

State before:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g⁻¹ • g • B)
Tactic:
apply isTrivialBlock_of_block
State after:
case mpr.hB
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g • B)

State before:
case mpr.hB
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g • B)
Tactic:
exact hgB
State after:
no goals