Theorem: MulAction.SubMulAction.IsBlock_coe (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
⊢ MulAction.IsBlock G B ↔ MulAction.IsBlock G (Subtype.val '' B)
Tactic:
simp only [IsBlock.def_one]
State after:
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 • B = B ∨ Disjoint (g • B) B) ↔
    ∀ (g : G), g • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (g • Subtype.val '' B) (Subtype.val '' B)

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 • B = B ∨ Disjoint (g • B) B) ↔
    ∀ (g : G), g • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (g • Subtype.val '' B) (Subtype.val '' B)
Tactic:
apply forall_congr'
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
⊢ ∀ (a : G),
    a • B = B ∨ Disjoint (a • B) B ↔
      a • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (a • Subtype.val '' B) (Subtype.val '' 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
⊢ ∀ (a : G),
    a • B = B ∨ Disjoint (a • B) B ↔
      a • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (a • Subtype.val '' B) (Subtype.val '' B)
Tactic:
intro g
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
⊢ g • B = B ∨ Disjoint (g • B) B ↔
    g • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (g • Subtype.val '' B) (Subtype.val '' 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
⊢ g • B = B ∨ Disjoint (g • B) B ↔
    g • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (g • Subtype.val '' B) (Subtype.val '' B)
Tactic:
rw [SubMulAction.smul_coe_eq_coe_smul]
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
⊢ g • B = B ∨ Disjoint (g • B) B ↔
    Subtype.val '' (g • B) = Subtype.val '' B ∨ Disjoint (Subtype.val '' (g • B)) (Subtype.val '' 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
⊢ g • B = B ∨ Disjoint (g • B) B ↔
    Subtype.val '' (g • B) = Subtype.val '' B ∨ Disjoint (Subtype.val '' (g • B)) (Subtype.val '' B)
Tactic:
apply or_congr (Set.image_eq_image Subtype.coe_injective).symm
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
⊢ Disjoint (g • B) B ↔ Disjoint (Subtype.val '' (g • B)) (Subtype.val '' 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
⊢ Disjoint (g • B) B ↔ Disjoint (Subtype.val '' (g • B)) (Subtype.val '' B)
Tactic:
simp only [Set.disjoint_iff, Set.subset_empty_iff]
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
⊢ g • B ∩ B = ∅ ↔ Subtype.val '' (g • B) ∩ Subtype.val '' 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
⊢ g • B ∩ B = ∅ ↔ Subtype.val '' (g • B) ∩ Subtype.val '' B = ∅
Tactic:
rw [←
  Set.InjOn.image_inter (Set.injOn_of_injective Subtype.coe_injective _) (Set.subset_univ _)
    (Set.subset_univ _)]
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
⊢ g • B ∩ B = ∅ ↔ (fun a => ↑a) '' (g • B ∩ 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
⊢ g • B ∩ B = ∅ ↔ (fun a => ↑a) '' (g • B ∩ B) = ∅
Tactic:
simp only [Set.image_eq_empty]
State after:
no goals