internlm/Lean-Github huggingface dataset:
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)
this : ∀ (i : ι), g • B i = B i
⊢ ⋂ i, g • B i = ⋂ i, B i
Tactic:
rw [Set.iInter_congr this]
Proof state after:
no goals
Theorem: MulAction.IsBlock.iInter
Proof 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)
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 ι
⊢ ⋂ i, B i = Set.univ
Theorem: MulAction.IsBlock.iInter
Proof 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]
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 ι
⊢ ∀ (i : ι), B i = Set.univ
Theorem: MulAction.IsBlock.iInter
Proof 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
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 ι
i : ι
⊢ B i = Set.univ
Theorem: MulAction.IsBlock.iInter
Proof 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
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 ι
i : ι
⊢ False
Theorem: MulAction.IsBlock.iInter
Proof 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
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 ι
i : ι
⊢ ι
Theorem: MulAction.IsBlock.iInter
Proof 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
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)
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]
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)
hι : IsEmpty ι
this : ⋂ i, B i = Set.univ
⊢ ∀ (g : G), g • Set.univ = Set.univ ∨ Disjoint (g • Set.univ) Set.univ
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)
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)
Proof state after:
no goals
Theorem: MulAction.IsBlock.iInter
Proof 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
Proof 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)
Theorem: MulAction.IsBlock.iInter
Proof 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
Proof 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)
Theorem: MulAction.IsBlock.iInter
Proof 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
Proof 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
Theorem: MulAction.IsBlock.iInter
Proof 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
Proof 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
Theorem: MulAction.IsBlock.iInter
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
⊢ IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)) (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
H : Subgroup G
hB : IsBlock (↥H) B
g : G
⊢ ∀ (g_1 : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)),
    g_1 • g • B = g • B ∨ Disjoint (g_1 • g • B) (g • B)
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
⊢ ∀ (g_1 : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)),
    g_1 • g • B = g • B ∨ Disjoint (g_1 • g • B) (g • B)
Tactic:
intro h'
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
Tactic:
obtain ⟨h, hH, hh⟩ := Subgroup.mem_map.mp (SetLike.coe_mem h')
Proof state after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : (MulEquiv.toMonoidHom (MulAut.conj g)) h = ↑h'
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : (MulEquiv.toMonoidHom (MulAut.conj g)) h = ↑h'
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
Tactic:
simp only [MulEquiv.coe_toMonoidHom, MulAut.conj_apply] at hh
Proof state after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ h' • g • B = g • h • B
Tactic:
suffices (h' : G) • g • B = g • h • B by
  rw [← this]; rfl
Proof state after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ ↑h' • g • B = g • h • B
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ ↑h' • g • B = g • h • B
Tactic:
rw [← hh]
Proof state after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹) • g • B = g • h • B
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹) • g • B = g • h • B
Tactic:
rw [smul_smul (g * h * g⁻¹) g B]
Proof state after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹ * g) • B = g • h • B
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹ * g) • B = g • h • B
Tactic:
rw [smul_smul g h B]
Proof state after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹ * g) • B = (g * h) • B
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹ * g) • B = (g * h) • B
Tactic:
simp only [inv_mul_cancel_right]
Proof state after:
no goals
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
Tactic:
simp only [this]
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
Tactic:
cases' IsBlock.def_one.mp hB ⟨h, hH⟩ with heq hdis
Proof state after:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
heq : { val := h, property := hH } • B = B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)

case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
hdis : Disjoint ({ val := h, property := hH } • B) B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
heq : { val := h, property := hH } • B = B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
Tactic:
left
Proof state after:
case inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
heq : { val := h, property := hH } • B = B
⊢ g • h • B = g • B
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
case inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
heq : { val := h, property := hH } • B = B
⊢ g • h • B = g • B
Tactic:
congr
Proof state after:
no goals
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
hdis : Disjoint ({ val := h, property := hH } • B) B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
Tactic:
right
Proof state after:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
hdis : Disjoint ({ val := h, property := hH } • B) B
⊢ Disjoint (g • h • B) (g • B)
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
hdis : Disjoint ({ val := h, property := hH } • B) B
⊢ Disjoint (g • h • B) (g • B)
Tactic:
exact Set.disjoint_image_of_injective (MulAction.injective g) hdis
Proof state after:
no goals
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : ↑h' • g • B = g • h • B
⊢ h' • g • B = g • h • B
Tactic:
rw [← this]
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : ↑h' • g • B = g • h • B
⊢ h' • g • B = ↑h' • g • B
Theorem: MulAction.IsBlock.of_subgroup_of_conjugate
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : ↑h' • g • B = g • h • B
⊢ h' • g • B = ↑h' • g • B
Tactic:
rfl
Proof state after:
no goals
Theorem: MulAction.IsBlock_of_block
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock G B
⊢ IsBlock G (g • B)
Tactic:
rw [IsBlock.of_top_iff] at hB ⊢
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥⊤) (g • B)
Theorem: MulAction.IsBlock_of_block
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥⊤) (g • B)
Tactic:
suffices Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤ by
  rw [← this]
  exact IsBlock.of_subgroup_of_conjugate hB g
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤
Theorem: MulAction.IsBlock_of_block
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤
Tactic:
suffices ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ by
  rw [this]
  refine Subgroup.map_comap_eq_self_of_surjective ?_ _
  exact MulEquiv.surjective (MulAut.conj g)
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
Theorem: MulAction.IsBlock_of_block
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
Tactic:
rw [Subgroup.comap_top]
Proof state after:
no goals
Theorem: MulAction.IsBlock_of_block
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤
⊢ IsBlock (↥⊤) (g • B)
Tactic:
rw [← this]
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤
⊢ IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤)) (g • B)
Theorem: MulAction.IsBlock_of_block
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤
⊢ IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤)) (g • B)
Tactic:
exact IsBlock.of_subgroup_of_conjugate hB g
Proof state after:
no goals
Theorem: MulAction.IsBlock_of_block
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤
Tactic:
rw [this]
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤) =
    Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
Theorem: MulAction.IsBlock_of_block
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤) =
    Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
Tactic:
refine Subgroup.map_comap_eq_self_of_surjective ?_ _
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
⊢ Function.Surjective ⇑(MulEquiv.toMonoidHom (MulAut.conj g))
Theorem: MulAction.IsBlock_of_block
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
⊢ Function.Surjective ⇑(MulEquiv.toMonoidHom (MulAut.conj g))
Tactic:
exact MulEquiv.surjective (MulAut.conj g)
Proof state after:
no goals
Theorem: MulAction.IsBlockSystem.of_block
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ IsBlockSystem G (Set.range fun g => g • B)
Tactic:
constructor
Proof state after:
case left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ Setoid.IsPartition (Set.range fun g => g • B)

case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∀ b ∈ Set.range fun g => g • B, IsBlock G b
Theorem: MulAction.IsBlockSystem.of_block
Proof state before:
case left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ Setoid.IsPartition (Set.range fun g => g • B)

case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∀ b ∈ Set.range fun g => g • B, IsBlock G b
Tactic:
constructor
Proof state after:
case left.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∅ ∉ Set.range fun g => g • B

case left.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∀ (a : X), ∃! b x, a ∈ b

case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
hBe : Set.Nonempty B
⊢ ∀ b ∈ Set.range fun g => g • B, IsBlock G b