awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock.{u_3, u_4} (↥H) B
g : G
h' :
  ↥(AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      H)
h : G
hH : h ∈ H
hh : g + h + -g = (↑h' : G)
suffices : (↑h' : G) +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
⊢ h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B

Tactic:
suffices (h' : G) +ᵥ (g +ᵥ B) = g +ᵥ (h +ᵥ B) by
    exact this
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock.{u_3, u_4} (↥H) B
g : G
h' :
  ↥(AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      H)
h : G
hH : h ∈ H
hh : g + h + -g = (↑h' : G)
rw : (g + h + -g + g) +ᵥ B = (g + h) +ᵥ B
⊢ (↑h' : G) +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B

Tactic:
rw [← hh, vadd_vadd, vadd_vadd]

Premises used: vadd_vadd
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock.{u_3, u_4} (↥H) B
g : G
h' :
  ↥(AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      H)
h : G
hH : h ∈ H
hh : g + h + -g = (↑h' : G)
⊢ (g + h + -g + g) +ᵥ B = (g + h) +ᵥ B

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
rw :
  ∀ (g_1 : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)),
    g_1 • g • B = g • B ∨ Disjoint (g_1 • g • B) (g • B)
⊢ IsBlock.{u_1, u_2} (↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)) (g • B)

Tactic:
rw [isBlock_iff_smul_eq_or_disjoint]

Premises used: MulAction.isBlock_iff_smul_eq_or_disjoint
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
obtain :
  ∀ (h : G) (hH : h ∈ H)
    (hh : (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g) : (a : G) → G) h = (↑h' : G)),
    h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)

Tactic:
obtain ⟨h, hH, hh⟩ := Subgroup.mem_map.mp (SetLike.coe_mem h')

Premises used: SetLike.coe_mem, Iff.mp, Subgroup.mem_map
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
this : h' • g • B = g • h • B
simp : g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)

Tactic:
simp only [this]
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
this : h' • g • B = g • h • B
f : Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hH • B = B → g • h • B = g • B
g₁ : Disjoint (Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hH • B) B → Disjoint (g • h • B) (g • B)
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)

Tactic:
apply (hB.smul_eq_or_disjoint ⟨h, hH⟩).imp

Premises used: Subtype.mk, MulAction.IsBlock.smul_eq_or_disjoint, Or.imp
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
this : h' • g • B = g • h • B
h_1 : Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hH • B = B
⊢ g • h • B = g • B

Tactic:
congr
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
this : h' • g • B = g • h • B
⊢ Disjoint (Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hH • B) B → Disjoint (g • h • B) (g • B)

Tactic:
Set.disjoint_image_of_injective (MulAction.injective g)

Premises used: MulAction.injective, Set.disjoint_image_of_injective
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
this : h' • g • B = g • h • B
⊢ Disjoint (Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hH • B) B → Disjoint (g • h • B) (g • B)

Tactic:
exact Set.disjoint_image_of_injective (MulAction.injective g)

Premises used: MulAction.injective, Set.disjoint_image_of_injective
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
suffices : h' • g • B = g • h • B
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)

Tactic:
suffices h' • g • B = g • h • B by
    simp only [this]
    apply (hB.smul_eq_or_disjoint ⟨h, hH⟩).imp
    · intro; congr
    · exact Set.disjoint_image_of_injective (MulAction.injective g)
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
this : (↑h' : G) • g • B = g • h • B
rw : h' • g • B = (↑h' : G) • g • B
⊢ h' • g • B = g • h • B

Tactic:
rw [← this]
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
this : (↑h' : G) • g • B = g • h • B
⊢ h' • g • B = (↑h' : G) • g • B

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
suffices : (↑h' : G) • g • B = g • h • B
⊢ h' • g • B = g • h • B

Tactic:
suffices (h' : G) • g • B = g • h • B by
    rw [← this]; rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
rw : (g * h * g⁻¹) • g • B = g • h • B
rw₁ : (g * h * g⁻¹ * g) • B = g • h • B
rw₂ : (g * h * g⁻¹ * g) • B = (g * h) • B
rw₃ rw₄ : (g * h) • B = (g * h) • B
⊢ (↑h' : G) • g • B = g • h • B

Tactic:
rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_right]

Premises used: HMul.hMul, smul_smul, Inv.inv, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock G B
rw : ∀ (hB : AddAction.IsBlock.{u_3, u_4} (↥⊤) B), AddAction.IsBlock.{u_3, u_4} (↥⊤) (g +ᵥ B)
⊢ AddAction.IsBlock G (g +ᵥ B)

Tactic:
rw [← AddAction.isBlock_top] at hB ⊢

Premises used: AddAction.isBlock_top
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock.{u_3, u_4} (↥⊤) B
rw :
  AddAction.IsBlock.{u_3, u_4}
    (↥(AddSubgroup.map (G := G)
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (AddSubgroup.comap (N := G)
          (AddEquiv.toAddMonoidHom
            ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
          ⊤)))
    (g +ᵥ B)
rw₁ : G →+ G
rw₂ :
  Function.Surjective.{u_3 + 1, u_3 + 1} (α := G) (β := G)
    (⇑(AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g))) :
      (a : G) → G)
⊢ AddAction.IsBlock.{u_3, u_4} (↥⊤) (g +ᵥ B)

Tactic:
rw [← AddSubgroup.map_comap_eq_self_of_surjective (G := G) ?_ ⊤]

Premises used: AddSubgroup.map_comap_eq_self_of_surjective, Top.top
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock.{u_3, u_4} (↥⊤) B
hB₁ :
  AddAction.IsBlock.{u_3, u_4}
    (↥(AddSubgroup.comap (N := G)
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        ⊤))
    B
⊢ AddAction.IsBlock.{u_3, u_4}
    (↥(AddSubgroup.map (G := G)
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (AddSubgroup.comap (N := G)
          (AddEquiv.toAddMonoidHom
            ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
          ⊤)))
    (g +ᵥ B)

Tactic:
apply AddAction.IsBlock.of_addSubgroup_of_conjugate

Premises used: AddAction.IsBlock.of_addSubgroup_of_conjugate
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
g : G
hB hB₁ hB₂ hB₃ hB₄ : AddAction.IsBlock.{u_3, u_4} (↥⊤) B
⊢ AddAction.IsBlock.{u_3, u_4}
    (↥(AddSubgroup.comap (N := G)
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        ⊤))
    B

Tactic:
rwa [AddSubgroup.comap_top]

Premises used: AddSubgroup.comap_top
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock.{u_3, u_4} (↥⊤) B
⊢ Function.Surjective.{u_3 + 1, u_3 + 1} (α := G) (β := G)
    (⇑(AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g))) :
      (a : G) → G)

Tactic:
(AddAut.conj g).surjective

Premises used: AddEquiv.surjective, DFunLike.coe, AddAut.conj
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock.{u_3, u_4} (↥⊤) B
⊢ Function.Surjective.{u_3 + 1, u_3 + 1} (α := G) (β := G)
    (⇑(AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g))) :
      (a : G) → G)

Tactic:
exact (AddAut.conj g).surjective

Premises used: AddEquiv.surjective, DFunLike.coe, AddAut.conj
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
g : G
hB : IsBlock G B
rw : ∀ (hB : IsBlock.{u_1, u_2} (↥⊤) B), IsBlock.{u_1, u_2} (↥⊤) (g • B)
⊢ IsBlock G (g • B)

Tactic:
rw [← isBlock_top] at hB ⊢

Premises used: MulAction.isBlock_top
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
g : G
hB : IsBlock.{u_1, u_2} (↥⊤) B
rw :
  IsBlock.{u_1, u_2}
    (↥(Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G)
        (Subgroup.comap (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) ⊤)))
    (g • B)
⊢ IsBlock.{u_1, u_2} (↥⊤) (g • B)

Tactic:
rw [← Subgroup.map_comap_eq_self_of_surjective
          (G := G) (f := MulAut.conj g) (MulAut.conj g).surjective ⊤]

Premises used: Subgroup.map_comap_eq_self_of_surjective, Top.top
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
g : G
hB : IsBlock.{u_1, u_2} (↥⊤) B
hB₁ : IsBlock.{u_1, u_2} (↥(Subgroup.comap (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) ⊤)) B
⊢ IsBlock.{u_1, u_2}
    (↥(Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G)
        (Subgroup.comap (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) ⊤)))
    (g • B)

Tactic:
apply IsBlock.of_subgroup_of_conjugate

Premises used: MulAction.IsBlock.of_subgroup_of_conjugate
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
g : G
hB hB₁ hB₂ hB₃ hB₄ : IsBlock.{u_1, u_2} (↥⊤) B
⊢ IsBlock.{u_1, u_2} (↥(Subgroup.comap (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) ⊤)) B

Tactic:
rwa [Subgroup.comap_top]

Premises used: Subgroup.comap_top
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ IsBlockSystem.{u_1, u_2} G (X := X) (range fun (g : G) ↦ g • B)

Tactic:
⟨⟨?nonempty, ?cover⟩, ?mem_blocks⟩

Premises used: And.intro, MulAction.IsBlockSystem
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
nonempty : ∅ ∉ range fun (g : G) ↦ g • B
cover : ∀ (a : X), ∃! b : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b ∧ a ∈ b
refine : ∀ ⦃B_1 : Set X⦄, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) B_1 → IsBlock G B_1
⊢ IsBlockSystem.{u_1, u_2} G (X := X) (range fun (g : G) ↦ g • B)

Tactic:
refine ⟨⟨?nonempty, ?cover⟩, ?mem_blocks⟩
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
⊢ IsBlock.{u_1, u_2} G (X := X) ((fun (g : G) ↦ g • B) g)

Tactic:
hB.translate g

Premises used: MulAction.IsBlock.translate
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
⊢ IsBlock.{u_1, u_2} G (X := X) ((fun (g : G) ↦ g • B) g)

Tactic:
exact hB.translate g

Premises used: MulAction.IsBlock.translate
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ ⦃B_1 : Set X⦄, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) B_1 → IsBlock G B_1

Tactic:
case mem_blocks => rintro B' ⟨g, rfl⟩; exact hB.translate g

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
nonempty : ∀ (x : G), ¬x • B = ∅
⊢ ∅ ∉ range fun (g : G) ↦ g • B

Tactic:
simp only [Set.mem_range, not_exists]

Premises used: Set.mem_range, not_exists
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
hg : g • B = ∅
nonempty : B = ∅
⊢ False

Tactic:
apply hBe.ne_empty

Premises used: Set.Nonempty.ne_empty
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
hg : g • B = ∅
⊢ B = ∅

Tactic:
simpa only [Set.smul_set_eq_empty] using hg

Premises used: Set.smul_set_eq_empty
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
a : X
cover : ∀ (b : X) (hb : b ∈ B), ∃! b : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b ∧ a ∈ b
⊢ ∃! b : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b ∧ a ∈ b

Tactic:
obtain ⟨b : X, hb : b ∈ B⟩ := hBe
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
a b : X
hb : b ∈ B
cover : ∀ (g : G), ∃! b_1 : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1
⊢ ∃! b : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b ∧ a ∈ b

Tactic:
obtain ⟨g, rfl⟩ := exists_smul_eq G b a

Premises used: MulAction.exists_smul_eq, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
h :
  (fun (b_1 : Set X) ↦ Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1) (g • B) ∧
    ∀ (y : Set X),
      (fun (b_1 : Set X) ↦ Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1) y →
        y = g • B
⊢ ∃! b_1 : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1

Tactic:
use g • B
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
h : ∀ (a : G), g • b ∈ a • B → a • B = g • B
⊢ (fun (b_1 : Set X) ↦ Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1) (g • B) ∧
    ∀ (y : Set X),
      (fun (b_1 : Set X) ↦ Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1) y →
        y = g • B

Tactic:
simp only [Set.smul_mem_smul_set_iff, hb, Set.mem_range,
      exists_apply_eq_apply, and_imp, forall_exists_index,
      forall_apply_eq_imp_iff, true_and]

Premises used: Set.mem_range, and_imp, forall_exists_index, Set.smul_mem_smul_set_iff, forall_apply_eq_imp_iff, true_and, exists_apply_eq_apply
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
⊢ ∀ (a : G), g • b ∈ a • B → a • B = g • B

Tactic:
fun g' ha ↦ hB.smul_eq_smul_of_nonempty ⟨g • b, ha, ⟨b, hb, rfl⟩⟩

Premises used: And.intro, MulAction.IsBlock.smul_eq_smul_of_nonempty, Exists.intro, HSMul.hSMul, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
⊢ ∀ (a : G), g • b ∈ a • B → a • B = g • B

Tactic:
exact fun g' ha ↦ hB.smul_eq_smul_of_nonempty ⟨g • b, ha, ⟨b, hb, rfl⟩⟩

Premises used: And.intro, MulAction.IsBlock.smul_eq_smul_of_nonempty, Exists.intro, HSMul.hSMul, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
simp : Eq.{u_2 + 1} (α := Set X) (range fun (i : ↥N) ↦ g • i • a) (range fun (m : ↥N) ↦ m • g • a)
⊢ g • orbit.{u_1, u_2} (↥N) a = orbit.{u_1, u_2} (↥N) (g • a)

Tactic:
simp only [orbit, Set.smul_set_range]

Premises used: MulAction.orbit, Set.smul_set_range
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
h :
  ∀ (x : X),
    Membership.mem (γ := Set X) (range fun (i : ↥N) ↦ g • i • a) x ↔
      Membership.mem (γ := Set X) (range fun (m : ↥N) ↦ m • g • a) x
⊢ Eq.{u_2 + 1} (α := Set X) (range fun (i : ↥N) ↦ g • i • a) (range fun (m : ↥N) ↦ m • g • a)

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x : X
h : (∃ (y : ↥N), g • y • a = x) → ∃ (y : ↥N), y • g • a = x
h₁ : (∃ (y : ↥N), y • g • a = x) → ∃ (y : ↥N), g • y • a = x
⊢ (∃ (y : ↥N), g • y • a = x) ↔ ∃ (y : ↥N), y • g • a = x

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
h : Subtype.mk (p := fun (x : G) ↦ x ∈ N) (g * k * g⁻¹) ⋯ • g • a = g • Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • a
⊢ ∃ (y : ↥N), y • g • a = g • Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • a

Tactic:
use ⟨g * k * g⁻¹, nN.conj_mem k hk g⟩
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
h : (g * k * g⁻¹) • g • a = g • k • a
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ N) (g * k * g⁻¹) ⋯ • g • a = g • Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • a

Tactic:
simp only [Subgroup.mk_smul]

Premises used: Subgroup.mk_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
h : (g * k * g⁻¹ * g) • a = g • k • a
h₁ : (g * k) • a = g • k • a
h₂ h₃ : g • k • a = g • k • a
⊢ (g * k * g⁻¹) • g • a = g • k • a

Tactic:
rw [smul_smul, inv_mul_cancel_right, ← smul_smul]

Premises used: smul_smul, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
h : g • Subtype.mk (p := fun (x : G) ↦ x ∈ N) (g⁻¹ * k * g) ⋯ • a = Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • g • a
⊢ ∃ (y : ↥N), g • y • a = Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • g • a

Tactic:
use ⟨g⁻¹ * k * g, nN.conj_mem' k hk g⟩
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
h : g • (g⁻¹ * k * g) • a = k • g • a
⊢ g • Subtype.mk (p := fun (x : G) ↦ x ∈ N) (g⁻¹ * k * g) ⋯ • a = Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • g • a

Tactic:
simp only [Subgroup.mk_smul]

Premises used: Subgroup.mk_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ g • (g⁻¹ * k * g) • a = k • g • a

Tactic:
simp only [← smul_smul, smul_inv_smul]

Premises used: smul_smul, smul_inv_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
N : Subgroup G
inst_2 : N.Normal
a : X
rw :
  ∀ (g : G),
    g • orbit.{u_1, u_2} (↥N) a = orbit.{u_1, u_2} (↥N) a ∨
      Disjoint (g • orbit.{u_1, u_2} (↥N) a) (orbit.{u_1, u_2} (↥N) a)
⊢ IsBlock G (orbit.{u_1, u_2} (↥N) a)

Tactic:
rw [isBlock_iff_smul_eq_or_disjoint]

Premises used: MulAction.isBlock_iff_smul_eq_or_disjoint