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

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
⊢ IsBlock G (B₁ ∩ B₂)
Tactic:
rw [IsBlock.def_one]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
⊢ ∀ (g : G), g • (B₁ ∩ B₂) = B₁ ∩ B₂ ∨ Disjoint (g • (B₁ ∩ B₂)) (B₁ ∩ B₂)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
⊢ ∀ (g : G), g • (B₁ ∩ B₂) = B₁ ∩ B₂ ∨ Disjoint (g • (B₁ ∩ B₂)) (B₁ ∩ B₂)
Tactic:
intro g
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
⊢ g • (B₁ ∩ B₂) = B₁ ∩ B₂ ∨ Disjoint (g • (B₁ ∩ B₂)) (B₁ ∩ B₂)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
⊢ g • (B₁ ∩ B₂) = B₁ ∩ B₂ ∨ Disjoint (g • (B₁ ∩ B₂)) (B₁ ∩ B₂)
Tactic:
rw [Set.smul_set_inter]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)
Tactic:
cases' IsBlock.def_one.mp h₁ g with h₁ h₁
State after:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)

case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
h₁ : Disjoint (g • B₁) B₁
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)

State before:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)
Tactic:
cases' IsBlock.def_one.mp h₂ g with h₂ h₂
State after:
case inl.inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : g • B₂ = B₂
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)

case inl.inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : Disjoint (g • B₂) B₂
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)

State before:
case inl.inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : Disjoint (g • B₂) B₂
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)
Tactic:
apply Or.intro_right
State after:
case inl.inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : Disjoint (g • B₂) B₂
⊢ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)

State before:
case inl.inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : Disjoint (g • B₂) B₂
⊢ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)
Tactic:
apply Disjoint.inter_left'
State after:
case inl.inr.h.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : Disjoint (g • B₂) B₂
⊢ Disjoint (g • B₂) (B₁ ∩ B₂)

State before:
case inl.inr.h.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : Disjoint (g • B₂) B₂
⊢ Disjoint (g • B₂) (B₁ ∩ B₂)
Tactic:
apply Disjoint.inter_right'
State after:
case inl.inr.h.h.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : Disjoint (g • B₂) B₂
⊢ Disjoint (g • B₂) B₂

State before:
case inl.inr.h.h.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : Disjoint (g • B₂) B₂
⊢ Disjoint (g • B₂) B₂
Tactic:
exact h₂
State after:
no goals

State before:
case inl.inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : g • B₂ = B₂
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)
Tactic:
apply Or.intro_left
State after:
case inl.inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : g • B₂ = B₂
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂

State before:
case inl.inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂✝ : IsBlock G B₂
g : G
h₁ : g • B₁ = B₁
h₂ : g • B₂ = B₂
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂
Tactic:
rw [h₁, h₂]
State after:
no goals

State before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
h₁ : Disjoint (g • B₁) B₁
⊢ g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)
Tactic:
apply Or.intro_right
State after:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
h₁ : Disjoint (g • B₁) B₁
⊢ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)

State before:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
h₁ : Disjoint (g • B₁) B₁
⊢ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)
Tactic:
apply Disjoint.inter_left
State after:
case inr.h.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
h₁ : Disjoint (g • B₁) B₁
⊢ Disjoint (g • B₁) (B₁ ∩ B₂)

State before:
case inr.h.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
h₁ : Disjoint (g • B₁) B₁
⊢ Disjoint (g • B₁) (B₁ ∩ B₂)
Tactic:
apply Disjoint.inter_right
State after:
case inr.h.h.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
h₁ : Disjoint (g • B₁) B₁
⊢ Disjoint (g • B₁) B₁

State before:
case inr.h.h.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁✝ : IsBlock G B₁
h₂ : IsBlock G B₂
g : G
h₁ : Disjoint (g • B₁) B₁
⊢ Disjoint (g • B₁) B₁
Tactic:
exact h₁
State after:
no goals