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

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

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

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

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

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

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

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