internlm/Lean-Github huggingface dataset:
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.left
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑z ∈ Subtype.val '' B

case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z = g • ↑z
Tactic:
exact ⟨z, hz, rfl⟩
Proof state after:
case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z = g • ↑z
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z = g • ↑z
Tactic:
rfl
Proof state after:
no goals
Theorem: MulAction.SubMulAction.IsBlock_coe
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
⊢ MulAction.IsBlock G B ↔ MulAction.IsBlock G (Subtype.val '' B)
Tactic:
simp only [IsBlock.def_one]
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
⊢ (∀ (g : G), g • B = B ∨ Disjoint (g • B) B) ↔
    ∀ (g : G), g • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (g • Subtype.val '' B) (Subtype.val '' B)
Theorem: MulAction.SubMulAction.IsBlock_coe
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
⊢ (∀ (g : G), g • B = B ∨ Disjoint (g • B) B) ↔
    ∀ (g : G), g • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (g • Subtype.val '' B) (Subtype.val '' B)
Tactic:
apply forall_congr'
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
⊢ ∀ (a : G),
    a • B = B ∨ Disjoint (a • B) B ↔
      a • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (a • Subtype.val '' B) (Subtype.val '' B)
Theorem: MulAction.SubMulAction.IsBlock_coe
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
⊢ ∀ (a : G),
    a • B = B ∨ Disjoint (a • B) B ↔
      a • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (a • Subtype.val '' B) (Subtype.val '' B)
Tactic:
intro g
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ g • B = B ∨ Disjoint (g • B) B ↔
    g • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (g • Subtype.val '' B) (Subtype.val '' B)
Theorem: MulAction.SubMulAction.IsBlock_coe
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ g • B = B ∨ Disjoint (g • B) B ↔
    g • Subtype.val '' B = Subtype.val '' B ∨ Disjoint (g • Subtype.val '' B) (Subtype.val '' B)
Tactic:
rw [SubMulAction.smul_coe_eq_coe_smul]
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ g • B = B ∨ Disjoint (g • B) B ↔
    Subtype.val '' (g • B) = Subtype.val '' B ∨ Disjoint (Subtype.val '' (g • B)) (Subtype.val '' B)
Theorem: MulAction.SubMulAction.IsBlock_coe
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ g • B = B ∨ Disjoint (g • B) B ↔
    Subtype.val '' (g • B) = Subtype.val '' B ∨ Disjoint (Subtype.val '' (g • B)) (Subtype.val '' B)
Tactic:
apply or_congr (Set.image_eq_image Subtype.coe_injective).symm
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ Disjoint (g • B) B ↔ Disjoint (Subtype.val '' (g • B)) (Subtype.val '' B)
Theorem: MulAction.SubMulAction.IsBlock_coe
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ Disjoint (g • B) B ↔ Disjoint (Subtype.val '' (g • B)) (Subtype.val '' B)
Tactic:
simp only [Set.disjoint_iff, Set.subset_empty_iff]
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ g • B ∩ B = ∅ ↔ Subtype.val '' (g • B) ∩ Subtype.val '' B = ∅
Theorem: MulAction.SubMulAction.IsBlock_coe
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ g • B ∩ B = ∅ ↔ Subtype.val '' (g • B) ∩ Subtype.val '' B = ∅
Tactic:
rw [←
  Set.InjOn.image_inter (Set.injOn_of_injective Subtype.coe_injective _) (Set.subset_univ _)
    (Set.subset_univ _)]
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ g • B ∩ B = ∅ ↔ (fun a => ↑a) '' (g • B ∩ B) = ∅
Theorem: MulAction.SubMulAction.IsBlock_coe
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ g • B ∩ B = ∅ ↔ (fun a => ↑a) '' (g • B ∩ B) = ∅
Tactic:
simp only [Set.image_eq_empty]
Proof state after:
no goals
Theorem: MulAction.IsBlock.of_top_iff
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ IsBlock G B ↔ IsBlock (↥⊤) B
Tactic:
simp only [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 • B = B ∨ Disjoint (g • B) B
Theorem: MulAction.IsBlock.of_top_iff
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 • B = B ∨ Disjoint (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), g • B = B ∨ Disjoint (g • B) B) → ∀ (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 • B = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Theorem: MulAction.IsBlock.of_top_iff
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), g • B = B ∨ Disjoint (g • B) B) → ∀ (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 • B = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
intro h g
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), g • B = B ∨ Disjoint (g • B) B
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 • B = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Theorem: MulAction.IsBlock.of_top_iff
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), g • B = B ∨ Disjoint (g • B) B
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 • B = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
exact h g
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 = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Theorem: MulAction.IsBlock.of_top_iff
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 = B ∨ Disjoint (g • B) B) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
intro h g
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 • B = B ∨ Disjoint (g • B) B
g : G
⊢ g • B = B ∨ Disjoint (g • B) B
Theorem: MulAction.IsBlock.of_top_iff
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 • B = B ∨ Disjoint (g • B) B
g : G
⊢ g • B = B ∨ Disjoint (g • B) B
Tactic:
exact h ⟨g, Subgroup.mem_top g⟩
Proof state after:
no goals
Theorem: MulAction.orbit.equal_or_disjoint
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)
Tactic:
cases' em (Disjoint (orbit G a) (orbit G b)) with h h
Proof state after:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)

case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ¬Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)
Theorem: MulAction.orbit.equal_or_disjoint
Proof state before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ¬Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)
Tactic:
apply Or.intro_left
Proof state after:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ¬Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b
Theorem: MulAction.orbit.equal_or_disjoint
Proof state before:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ¬Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b
Tactic:
rw [Set.not_disjoint_iff] at h
Proof state after:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ∃ x ∈ orbit G a, x ∈ orbit G b
⊢ orbit G a = orbit G b
Theorem: MulAction.orbit.equal_or_disjoint
Proof state before:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ∃ x ∈ orbit G a, x ∈ orbit G b
⊢ orbit G a = orbit G b
Tactic:
obtain ⟨x, hxa, hxb⟩ := h
Proof state after:
case inr.h.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b x : X
hxa : x ∈ orbit G a
hxb : x ∈ orbit G b
⊢ orbit G a = orbit G b
Theorem: MulAction.orbit.equal_or_disjoint
Proof state before:
case inr.h.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b x : X
hxa : x ∈ orbit G a
hxb : x ∈ orbit G b
⊢ orbit G a = orbit G b
Tactic:
rw [← orbit_eq_iff] at hxa hxb
Proof state after:
case inr.h.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b x : X
hxa : orbit G x = orbit G a
hxb : orbit G x = orbit G b
⊢ orbit G a = orbit G b
Theorem: MulAction.orbit.equal_or_disjoint
Proof state before:
case inr.h.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b x : X
hxa : orbit G x = orbit G a
hxb : orbit G x = orbit G b
⊢ orbit G a = orbit G b
Tactic:
rw [← hxa, ← hxb]
Proof state after:
no goals
Theorem: MulAction.orbit.equal_or_disjoint
Proof state before:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)
Tactic:
apply Or.intro_right
Proof state after:
case inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : Disjoint (orbit G a) (orbit G b)
⊢ Disjoint (orbit G a) (orbit G b)
Theorem: MulAction.orbit.equal_or_disjoint
Proof state before:
case inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : Disjoint (orbit G a) (orbit G b)
⊢ Disjoint (orbit G a) (orbit G b)
Tactic:
exact h
Proof state after:
no goals
Theorem: MulAction.IsBlock.inter
Proof 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]
Proof 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₂)
Theorem: MulAction.IsBlock.inter
Proof 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
Proof 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₂)
Theorem: MulAction.IsBlock.inter
Proof 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]
Proof 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₂)
Theorem: MulAction.IsBlock.inter
Proof 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₁
Proof 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₂)
Theorem: MulAction.IsBlock.inter
Proof 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₂
Proof 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₂)
Theorem: MulAction.IsBlock.inter
Proof 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
Proof 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₂)
Theorem: MulAction.IsBlock.inter
Proof 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'
Proof 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₂)
Theorem: MulAction.IsBlock.inter
Proof 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'
Proof 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₂
Theorem: MulAction.IsBlock.inter
Proof 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₂
Proof state after:
no goals
Theorem: MulAction.IsBlock.inter
Proof 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
Proof 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₂
Theorem: MulAction.IsBlock.inter
Proof 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₂]
Proof state after:
no goals
Theorem: MulAction.IsBlock.inter
Proof 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
Proof 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₂)
Theorem: MulAction.IsBlock.inter
Proof 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
Proof 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₂)
Theorem: MulAction.IsBlock.inter
Proof 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
Proof 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₁
Theorem: MulAction.IsBlock.inter
Proof 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₁
Proof state after:
no goals
Theorem: MulAction.IsBlock.iInter
Proof 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]
Proof 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)
Theorem: MulAction.IsBlock.iInter
Proof 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ι
Proof 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)
Theorem: MulAction.IsBlock.iInter
Proof 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
Proof 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)
Theorem: MulAction.IsBlock.iInter
Proof 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]
Proof 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)
Theorem: MulAction.IsBlock.iInter
Proof 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
Proof 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)
Theorem: MulAction.IsBlock.iInter
Proof 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
Proof 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)
Theorem: MulAction.IsBlock.iInter
Proof 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
Proof 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
Theorem: MulAction.IsBlock.iInter
Proof 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)
Proof 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