Theorem: MulAction.IsBlock.mk_mem (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), ∀ a ∈ B, g • a ∈ B → g • B = B
Tactic:
rw [IsBlock.mk_notempty_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 ≠ ∅ → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ 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 ≠ ∅ → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
Tactic:
simp_rw [← Set.nonempty_iff_ne_empty, Set.nonempty_def]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G), (∃ x, x ∈ g • B ∩ B) → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ 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), (∃ x, x ∈ g • B ∩ B) → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
Tactic:
simp_rw [Set.mem_inter_iff]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G), (∃ x ∈ g • B, x ∈ B) → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ 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), (∃ x ∈ g • B, x ∈ B) → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
Tactic:
simp_rw [exists_imp]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G) (x : X), x ∈ g • B ∧ x ∈ B → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ 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) (x : X), x ∈ g • B ∧ x ∈ B → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
Tactic:
simp_rw [and_imp]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G), ∀ x ∈ g • B, x ∈ B → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ 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), ∀ x ∈ g • B, x ∈ B → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
Tactic:
simp_rw [Set.mem_smul_set_iff_inv_smul_mem]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ 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) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
Tactic:
constructor
State after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B) → ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B

case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B) → ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B

State before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B) → ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
Tactic:
intro H g a ha hga
State after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B
g : G
a : X
ha : a ∈ B
hga : g • a ∈ B
⊢ g • B = B

State before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B
g : G
a : X
ha : a ∈ B
hga : g • a ∈ B
⊢ g • B = B
Tactic:
rw [← eq_inv_smul_iff]
State after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B
g : G
a : X
ha : a ∈ B
hga : g • a ∈ B
⊢ B = g⁻¹ • B

State before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B
g : G
a : X
ha : a ∈ B
hga : g • a ∈ B
⊢ B = g⁻¹ • B
Tactic:
apply symm
State after:
case mp.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B
g : G
a : X
ha : a ∈ B
hga : g • a ∈ B
⊢ g⁻¹ • B = B

State before:
case mp.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B
g : G
a : X
ha : a ∈ B
hga : g • a ∈ B
⊢ g⁻¹ • B = B
Tactic:
apply H g⁻¹ a _ ha
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B
g : G
a : X
ha : a ∈ B
hga : g • a ∈ B
⊢ g⁻¹⁻¹ • a ∈ B

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B
g : G
a : X
ha : a ∈ B
hga : g • a ∈ B
⊢ g⁻¹⁻¹ • a ∈ B
Tactic:
rw [inv_inv]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B
g : G
a : X
ha : a ∈ B
hga : g • a ∈ B
⊢ g • a ∈ B

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B
g : G
a : X
ha : a ∈ B
hga : g • a ∈ B
⊢ g • a ∈ B
Tactic:
exact hga
State after:
no goals

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B) → ∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B
Tactic:
intro H g a ha hga
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
g : G
a : X
ha : g⁻¹ • a ∈ B
hga : a ∈ B
⊢ g • B = B

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
g : G
a : X
ha : g⁻¹ • a ∈ B
hga : a ∈ B
⊢ g • B = B
Tactic:
rw [← eq_inv_smul_iff]
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
g : G
a : X
ha : g⁻¹ • a ∈ B
hga : a ∈ B
⊢ B = g⁻¹ • B

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
g : G
a : X
ha : g⁻¹ • a ∈ B
hga : a ∈ B
⊢ B = g⁻¹ • B
Tactic:
apply symm
State after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
g : G
a : X
ha : g⁻¹ • a ∈ B
hga : a ∈ B
⊢ g⁻¹ • B = B

State before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
g : G
a : X
ha : g⁻¹ • a ∈ B
hga : a ∈ B
⊢ g⁻¹ • B = B
Tactic:
exact H g⁻¹ a hga ha
State after:
no goals