Theorem: MulAction.IsBlock.mk_subset (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} {b : X}, b ∈ B → b ∈ g • 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
⊢ IsBlock G B → ∀ {g : G} {b : X}, b ∈ B → b ∈ g • 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} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B) → IsBlock G B

State before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ IsBlock G B → ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
Tactic:
intro hB g b hb hgb
State after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
g : G
b : X
hb : b ∈ B
hgb : b ∈ g • 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
hB : IsBlock G B
g : G
b : X
hb : b ∈ B
hgb : b ∈ g • B
⊢ g • B ≤ B
Tactic:
rw [Set.le_iff_subset, Set.set_smul_subset_iff,
  IsBlock.def_mem hB hb (Set.mem_smul_set_iff_inv_smul_mem.mp hgb)]
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} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B) → IsBlock G B
Tactic:
rw [IsBlock.mk_notempty_one]
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 : X}, b ∈ B → b ∈ g • B → g • B ≤ B) → ∀ (g : G), g • B ∩ 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
⊢ (∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B) → ∀ (g : G), g • B ∩ B ≠ ∅ → g • B = B
Tactic:
intro hB g hg
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : g • B ∩ 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
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : g • B ∩ B ≠ ∅
⊢ g • B = B
Tactic:
rw [← Set.nonempty_iff_ne_empty] at hg
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ 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
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
⊢ g • B = B
Tactic:
obtain ⟨b : X, hb' : b ∈ g • B, hb : b ∈ B⟩ := Set.nonempty_def.mp hg
State after:
case mpr.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
⊢ g • B = B

State before:
case mpr.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
⊢ g • B = B
Tactic:
apply le_antisymm
State after:
case mpr.intro.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
⊢ g • B ≤ B

case mpr.intro.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
⊢ B ≤ g • B

State before:
case mpr.intro.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
⊢ B ≤ g • B
Tactic:
suffices g⁻¹ • B ≤ B by
  rw [Set.le_iff_subset] at this ⊢
  rw [← inv_inv g, ← Set.set_smul_subset_iff]; exact this
State after:
case mpr.intro.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
⊢ g⁻¹ • B ≤ B

State before:
case mpr.intro.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
⊢ g⁻¹ • B ≤ B
Tactic:
exact
  hB (Set.mem_smul_set_iff_inv_smul_mem.mp hb') (Set.smul_mem_smul_set_iff.mpr hb)
State after:
no goals

State before:
case mpr.intro.intro.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
⊢ g • B ≤ B
Tactic:
exact hB hb hb'
State after:
no goals

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
this : g⁻¹ • B ≤ B
⊢ B ≤ g • B
Tactic:
rw [Set.le_iff_subset] at this ⊢
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
this : g⁻¹ • B ⊆ B
⊢ B ⊆ g • B

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
this : g⁻¹ • B ⊆ B
⊢ B ⊆ g • B
Tactic:
rw [← inv_inv g, ← Set.set_smul_subset_iff]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
this : 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
hB : ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ≤ B
g : G
hg : Set.Nonempty (g • B ∩ B)
b : X
hb' : b ∈ g • B
hb : b ∈ B
this : g⁻¹ • B ⊆ B
⊢ g⁻¹ • B ⊆ B
Tactic:
exact this
State after:
no goals