Theorem: MulAction.IsBlock.of_top_iff (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 ↔ IsBlock (↥⊤) B
Tactic:
simp only [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 • B = B ∨ Disjoint (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 • B = B ∨ Disjoint (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), g • B = B ∨ Disjoint (g • B) B) → ∀ (g : ↥⊤), g • B = B ∨ Disjoint (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 • B = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (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), g • B = B ∨ Disjoint (g • B) B) → ∀ (g : ↥⊤), g • B = B ∨ Disjoint (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 • B = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
intro h g
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), g • B = B ∨ Disjoint (g • B) B
g : ↥⊤
⊢ g • B = B ∨ Disjoint (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 • B = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (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), g • B = B ∨ Disjoint (g • B) B
g : ↥⊤
⊢ g • B = B ∨ Disjoint (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 • B = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
exact h g
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : ↥⊤), g • B = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (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
⊢ (∀ (g : ↥⊤), g • B = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
intro h g
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 • B = B ∨ Disjoint (g • B) B
g : G
⊢ g • B = B ∨ Disjoint (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 • B = B ∨ Disjoint (g • B) B
g : G
⊢ g • B = B ∨ Disjoint (g • B) B
Tactic:
exact h ⟨g, Subgroup.mem_top g⟩
State after:
no goals