Theorem: MulAction.IsBlock.mk_notempty_one (Jordan/Blocks.lean)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ IsBlock G B ↔ ∀ (g : G), g • B ∩ B ≠ ∅ → g • B = B
Tactic:
rw [IsBlock.def_one]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G), g • B = B ∨ Disjoint (g • B) B) ↔ ∀ (g : G), g • B ∩ B ≠ ∅ → g • B = B

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G), g • B = B ∨ Disjoint (g • B) B) ↔ ∀ (g : G), g • B ∩ B ≠ ∅ → g • B = B
Tactic:
apply forall_congr'
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ ∀ (a : G), a • B = B ∨ Disjoint (a • B) B ↔ a • B ∩ B ≠ ∅ → a • B = B

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ ∀ (a : G), a • B = B ∨ Disjoint (a • B) B ↔ a • B ∩ B ≠ ∅ → a • B = B
Tactic:
intro g
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
⊢ g • B = B ∨ Disjoint (g • B) B ↔ g • B ∩ B ≠ ∅ → g • B = B

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
⊢ g • B = B ∨ Disjoint (g • B) B ↔ g • B ∩ B ≠ ∅ → g • B = B
Tactic:
rw [Set.disjoint_iff_inter_eq_empty]
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
⊢ g • B = B ∨ g • B ∩ B = ∅ ↔ g • B ∩ B ≠ ∅ → g • B = B

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
⊢ g • B = B ∨ g • B ∩ B = ∅ ↔ g • B ∩ B ≠ ∅ → g • B = B
Tactic:
exact or_iff_not_imp_right
State after:
no goals