internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ x ∈ ∅
Tactic:
simp only [Set.mem_empty_iff_false]
Proof state after:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ False
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ False
Tactic:
suffices g'⁻¹ • x ∈ (g'⁻¹ * g) • B ⊓ B by
  apply h this
Proof state after:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ g'⁻¹ • x ∈ (g'⁻¹ * g) • B ⊓ B
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ g'⁻¹ • x ∈ (g'⁻¹ * g) • B ⊓ B
Tactic:
simp only [Set.inf_eq_inter, Set.mem_inter_iff]
Proof state after:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ g'⁻¹ • x ∈ (g'⁻¹ * g) • B ∧ g'⁻¹ • x ∈ B
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ g'⁻¹ • x ∈ (g'⁻¹ * g) • B ∧ g'⁻¹ • x ∈ B
Tactic:
simp only [← Set.mem_smul_set_iff_inv_smul_mem]
Proof state after:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ x ∈ g' • (g'⁻¹ * g) • B ∧ x ∈ g' • B
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ x ∈ g' • (g'⁻¹ * g) • B ∧ x ∈ g' • B
Tactic:
rw [← smul_smul]
Proof state after:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ x ∈ g' • g'⁻¹ • g • B ∧ x ∈ g' • B
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ x ∈ g' • g'⁻¹ • g • B ∧ x ∈ g' • B
Tactic:
rw [smul_inv_smul]
Proof state after:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ x ∈ g • B ∧ x ∈ g' • B
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ x ∈ g • B ∧ x ∈ g' • B
Tactic:
exact ⟨hx, hx'⟩
Proof state after:
no goals
Theorem: MulAction.IsBlock.def_one
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
this : g'⁻¹ • x ∈ (g'⁻¹ * g) • B ⊓ B
⊢ False
Tactic:
apply h this
Proof state after:
no goals
Theorem: MulAction.IsBlock.mk_notempty_one
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_notempty_one
Proof 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'
Proof 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
Theorem: MulAction.IsBlock.mk_notempty_one
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_notempty_one
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_notempty_one
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.mk_mem
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.mk_mem
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_mem
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.mk_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_subset
Proof 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)]
Proof state after:
no goals
Theorem: MulAction.IsBlock.mk_subset
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.mk_subset
Proof 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)
Proof state after:
no goals
Theorem: MulAction.IsBlock.mk_subset
Proof 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'
Proof state after:
no goals
Theorem: MulAction.IsBlock.mk_subset
Proof 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 ⊢
Proof 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
Theorem: MulAction.IsBlock.mk_subset
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.mk_subset
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock_of_invariant
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
⊢ IsBlock G B
Tactic:
rw [IsBlock.def_one]
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
⊢ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Theorem: MulAction.IsBlock_of_invariant
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
⊢ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
intro g
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B = B ∨ Disjoint (g • B) B
Theorem: MulAction.IsBlock_of_invariant
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B = B ∨ Disjoint (g • B) B
Tactic:
apply Or.intro_left
Proof state after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B = B
Theorem: MulAction.IsBlock_of_invariant
Proof state before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B = B
Tactic:
apply le_antisymm
Proof state after:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B ≤ B

case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ B ≤ g • B
Theorem: MulAction.IsBlock_of_invariant
Proof state before:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B ≤ B

case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ B ≤ g • B
Tactic:
exact hfB g
Proof state after:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ B ≤ g • B
Theorem: MulAction.IsBlock_of_invariant
Proof state before:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ B ≤ g • B
Tactic:
intro x hx
Proof state after:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ x ∈ g • B
Theorem: MulAction.IsBlock_of_invariant
Proof state before:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ x ∈ g • B
Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem]
Proof state after:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ g⁻¹ • x ∈ B
Theorem: MulAction.IsBlock_of_invariant
Proof state before:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ g⁻¹ • x ∈ B
Tactic:
apply hfB g⁻¹
Proof state after:
case h.a.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ g⁻¹ • x ∈ g⁻¹ • B