Theorem: MulAction.IsBlock.iInter (Jordan/Blocks.lean)

State before:
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
⊢ IsBlock G (⋂ i, B i)
Tactic:
rw [IsBlock.def_one]
State after:
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
⊢ ∀ (g : G), g • ⋂ i, B i = ⋂ i, B i ∨ Disjoint (g • ⋂ i, B i) (⋂ i, B i)

State before:
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
⊢ ∀ (g : G), g • ⋂ i, B i = ⋂ i, B i ∨ Disjoint (g • ⋂ i, B i) (⋂ i, B i)
Tactic:
cases' em (IsEmpty ι) with hι hι
State after:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
⊢ ∀ (g : G), g • ⋂ i, B i = ⋂ i, B i ∨ Disjoint (g • ⋂ i, B i) (⋂ i, B i)

case inr
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
⊢ ∀ (g : G), g • ⋂ i, B i = ⋂ i, B i ∨ Disjoint (g • ⋂ i, B i) (⋂ i, B i)

State before:
case inr
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
⊢ ∀ (g : G), g • ⋂ i, B i = ⋂ i, B i ∨ Disjoint (g • ⋂ i, B i) (⋂ i, B i)
Tactic:
intro g
State after:
case inr
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
⊢ g • ⋂ i, B i = ⋂ i, B i ∨ Disjoint (g • ⋂ i, B i) (⋂ i, B i)

State before:
case inr
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
⊢ g • ⋂ i, B i = ⋂ i, B i ∨ Disjoint (g • ⋂ i, B i) (⋂ i, B i)
Tactic:
rw [smul_set_iInter]
State after:
case inr
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
⊢ ⋂ i, g • B i = ⋂ i, B i ∨ Disjoint (⋂ i, g • B i) (⋂ i, B i)

State before:
case inr
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
⊢ ⋂ i, g • B i = ⋂ i, B i ∨ Disjoint (⋂ i, g • B i) (⋂ i, B i)
Tactic:
cases' em (∃ i : ι, Disjoint (g • B i) (B i)) with h h
State after:
case inr.inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
h : ∃ i, Disjoint (g • B i) (B i)
⊢ ⋂ i, g • B i = ⋂ i, B i ∨ Disjoint (⋂ i, g • B i) (⋂ i, B i)

case inr.inr
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
h : ¬∃ i, Disjoint (g • B i) (B i)
⊢ ⋂ i, g • B i = ⋂ i, B i ∨ Disjoint (⋂ i, g • B i) (⋂ i, B i)

State before:
case inr.inr
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
h : ¬∃ i, Disjoint (g • B i) (B i)
⊢ ⋂ i, g • B i = ⋂ i, B i ∨ Disjoint (⋂ i, g • B i) (⋂ i, B i)
Tactic:
simp only [not_exists] at h
State after:
case inr.inr
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
h : ∀ (x : ι), ¬Disjoint (g • B x) (B x)
⊢ ⋂ i, g • B i = ⋂ i, B i ∨ Disjoint (⋂ i, g • B i) (⋂ i, B i)

State before:
case inr.inr
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
h : ∀ (x : ι), ¬Disjoint (g • B x) (B x)
⊢ ⋂ i, g • B i = ⋂ i, B i ∨ Disjoint (⋂ i, g • B i) (⋂ i, B i)
Tactic:
apply Or.intro_left
State after:
case inr.inr.h
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
h : ∀ (x : ι), ¬Disjoint (g • B x) (B x)
⊢ ⋂ i, g • B i = ⋂ i, B i

State before:
case inr.inr.h
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
h : ∀ (x : ι), ¬Disjoint (g • B x) (B x)
⊢ ⋂ i, g • B i = ⋂ i, B i
Tactic:
have : ∀ i : ι, g • B i = B i := fun i => Or.resolve_right (IsBlock.def_one.mp (hB i) g) (h i)
State after:
case inr.inr.h
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
h : ∀ (x : ι), ¬Disjoint (g • B x) (B x)
this : ∀ (i : ι), g • B i = B i
⊢ ⋂ i, g • B i = ⋂ i, B i

State before:
case inr.inr.h
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
h : ∀ (x : ι), ¬Disjoint (g • B x) (B x)
this : ∀ (i : ι), g • B i = B i
⊢ ⋂ i, g • B i = ⋂ i, B i
Tactic:
rw [Set.iInter_congr this]
State after:
no goals

State before:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
⊢ ∀ (g : G), g • ⋂ i, B i = ⋂ i, B i ∨ Disjoint (g • ⋂ i, B i) (⋂ i, B i)
Tactic:
suffices (⋂ i : ι, B i) = Set.univ by
  rw [this]
  exact IsBlock.def_one.mp (top_IsBlock X)
State after:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
⊢ ⋂ i, B i = Set.univ

State before:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
⊢ ⋂ i, B i = Set.univ
Tactic:
simp only [Set.top_eq_univ, Set.iInter_eq_univ]
State after:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
⊢ ∀ (i : ι), B i = Set.univ

State before:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
⊢ ∀ (i : ι), B i = Set.univ
Tactic:
intro i
State after:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
i : ι
⊢ B i = Set.univ

State before:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
i : ι
⊢ B i = Set.univ
Tactic:
exfalso
State after:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
i : ι
⊢ False

State before:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
i : ι
⊢ False
Tactic:
apply hι.false
State after:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
i : ι
⊢ ι

State before:
case inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
i : ι
⊢ ι
Tactic:
exact i
State after:
no goals

State before:
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
this : ⋂ i, B i = Set.univ
⊢ ∀ (g : G), g • ⋂ i, B i = ⋂ i, B i ∨ Disjoint (g • ⋂ i, B i) (⋂ i, B i)
Tactic:
rw [this]
State after:
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
this : ⋂ i, B i = Set.univ
⊢ ∀ (g : G), g • Set.univ = Set.univ ∨ Disjoint (g • Set.univ) Set.univ

State before:
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : IsEmpty ι
this : ⋂ i, B i = Set.univ
⊢ ∀ (g : G), g • Set.univ = Set.univ ∨ Disjoint (g • Set.univ) Set.univ
Tactic:
exact IsBlock.def_one.mp (top_IsBlock X)
State after:
no goals

State before:
case inr.inl
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
h : ∃ i, Disjoint (g • B i) (B i)
⊢ ⋂ i, g • B i = ⋂ i, B i ∨ Disjoint (⋂ i, g • B i) (⋂ i, B i)
Tactic:
obtain ⟨j, hj⟩ := h
State after:
case inr.inl.intro
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
j : ι
hj : Disjoint (g • B j) (B j)
⊢ ⋂ i, g • B i = ⋂ i, B i ∨ Disjoint (⋂ i, g • B i) (⋂ i, B i)

State before:
case inr.inl.intro
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
j : ι
hj : Disjoint (g • B j) (B j)
⊢ ⋂ i, g • B i = ⋂ i, B i ∨ Disjoint (⋂ i, g • B i) (⋂ i, B i)
Tactic:
apply Or.intro_right
State after:
case inr.inl.intro.h
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
j : ι
hj : Disjoint (g • B j) (B j)
⊢ Disjoint (⋂ i, g • B i) (⋂ i, B i)

State before:
case inr.inl.intro.h
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
j : ι
hj : Disjoint (g • B j) (B j)
⊢ Disjoint (⋂ i, g • B i) (⋂ i, B i)
Tactic:
refine' Disjoint.mono _ _ hj
State after:
case inr.inl.intro.h.refine'_1
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
j : ι
hj : Disjoint (g • B j) (B j)
⊢ ⋂ i, g • B i ≤ g • B j

case inr.inl.intro.h.refine'_2
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
j : ι
hj : Disjoint (g • B j) (B j)
⊢ ⋂ i, B i ≤ B j

State before:
case inr.inl.intro.h.refine'_1
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
j : ι
hj : Disjoint (g • B j) (B j)
⊢ ⋂ i, g • B i ≤ g • B j

case inr.inl.intro.h.refine'_2
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
j : ι
hj : Disjoint (g • B j) (B j)
⊢ ⋂ i, B i ≤ B j
Tactic:
apply Set.iInter_subset
State after:
case inr.inl.intro.h.refine'_2
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
j : ι
hj : Disjoint (g • B j) (B j)
⊢ ⋂ i, B i ≤ B j

State before:
case inr.inl.intro.h.refine'_2
G : Type u_3
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Type u_1
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
hι : ¬IsEmpty ι
g : G
j : ι
hj : Disjoint (g • B j) (B j)
⊢ ⋂ i, B i ≤ B j
Tactic:
apply Set.iInter_subset
State after:
no goals