Theorem: MulAction.IsBlock.def_one (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), g • B = B ∨ Disjoint (g • B) B
Tactic:
rw [IsBlock.def]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) ↔ ∀ (g : 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), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) ↔ ∀ (g : 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), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) → ∀ (g : 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), g • B = B ∨ Disjoint (g • B) B) → ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • 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
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
intro hB g
State after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • 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
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g : G
⊢ g • B = B ∨ Disjoint (g • B) B
Tactic:
simpa only [one_smul] using hB g 1
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), g • B = B ∨ Disjoint (g • B) B) → ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
intro hB
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), g • B = B ∨ Disjoint (g • B) B
⊢ ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • 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
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
⊢ ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
intro g g'
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), g • B = B ∨ Disjoint (g • B) B
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • 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
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
cases hB (g'⁻¹ * g) with
| inl h =>
  apply Or.intro_left
  rw [← inv_inv g', eq_inv_smul_iff, smul_smul]
  exact h
| inr h =>
  apply Or.intro_right
  rw [Set.disjoint_iff] at h ⊢
  rintro x ⟨hx, hx'⟩
  simp only [Set.mem_empty_iff_false]
  suffices g'⁻¹ • x ∈ (g'⁻¹ * g) • B ⊓ B by
    apply h this
  simp only [Set.inf_eq_inter, Set.mem_inter_iff]
  simp only [← Set.mem_smul_set_iff_inv_smul_mem]
  rw [← smul_smul]; rw [smul_inv_smul]
  exact ⟨hx, hx'⟩
State after:
no goals

State before:
case mpr.inl
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
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
apply Or.intro_left
State after:
case mpr.inl.h
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
⊢ g • B = g' • B

State before:
case mpr.inl.h
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
⊢ g • B = g' • B
Tactic:
rw [← inv_inv g', eq_inv_smul_iff, smul_smul]
State after:
case mpr.inl.h
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
⊢ (g'⁻¹ * g) • B = B

State before:
case mpr.inl.h
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
⊢ (g'⁻¹ * g) • B = B
Tactic:
exact h
State after:
no goals

State before:
case mpr.inr
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 : Disjoint ((g'⁻¹ * g) • B) B
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
apply Or.intro_right
State after:
case mpr.inr.h
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 : Disjoint ((g'⁻¹ * g) • B) B
⊢ Disjoint (g • B) (g' • B)

State before:
case mpr.inr.h
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 : Disjoint ((g'⁻¹ * g) • B) B
⊢ Disjoint (g • B) (g' • B)
Tactic:
rw [Set.disjoint_iff] at h ⊢
State after:
case mpr.inr.h
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 ⊆ ∅
⊢ g • B ∩ g' • B ⊆ ∅

State before:
case mpr.inr.h
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 ⊆ ∅
⊢ g • B ∩ g' • B ⊆ ∅
Tactic:
rintro x ⟨hx, hx'⟩
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 ∈ ∅

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]
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

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
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

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]
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

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]
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

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]
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

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]
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

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'⟩
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), 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
State after:
no goals