awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_1
X : Type u_2
inst : Monoid M
inst_1 : MulAction M X
B : Set X
s : Set M
hB : IsBlock M B
hs : ¬B ⊆ s • B
⊢ ¬HSMul.hSMul.{u_1, u_2, u_2} (α := M) 1 B ⊆ s • B

Tactic:
simpa using hs
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_1
X : Type u_2
inst : Monoid M
inst_1 : MulAction M X
B : Set X
s : Set M
hB : IsBlock M B
hs : ¬B ⊆ s • B
⊢ Disjoint B (s • B)

Tactic:
simpa using hB.disjoint_smul_set_smul (g := 1) (by simpa using hs)

Premises used: MulAction.IsBlock.disjoint_smul_set_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_1
X : Type u_2
inst : Monoid M
inst_1 : MulAction M X
B : Set X
s : Set M
hB : IsBlock M B
hs : ¬B ⊆ s • B
⊢ Disjoint (s • B) B

Tactic:
(hB.disjoint_smul_right hs).symm

Premises used: MulAction.IsBlock.disjoint_smul_right, Disjoint.symm
-- 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
hB : IsBlock G B
g : G
⊢ g • B ≠ B → Disjoint (g • B) B

Tactic:
simpa using hB (g₂ := 1)
-- 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
refine :
  ∀ (hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B) (g₁ g₂ : G) (h : g₁ • B ≠ g₂ • B), Disjoint (g₁ • B) (g₂ • B)
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B

Tactic:
refine ⟨fun hB g ↦ by simpa using hB (g₂ := 1), fun hB g₁ g₂ h ↦ ?_⟩
-- 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
hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
g₁ g₂ : G
h : g₁ • B ≠ g₂ • B
simp : ∀ (h : ¬(g₂⁻¹ * g₁) • B = B), Disjoint ((g₂⁻¹ * g₁) • B) B
⊢ Disjoint (g₁ • B) (g₂ • B)

Tactic:
simp only [disjoint_smul_set_right, ne_eq, ← inv_smul_eq_iff, smul_smul] at h ⊢

Premises used: inv_smul_eq_iff, smul_smul, ne_eq, Set.disjoint_smul_set_right
-- 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
hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
g₁ g₂ : G
h : ¬(g₂⁻¹ * g₁) • B = B
⊢ Disjoint ((g₂⁻¹ * g₁) • B) B

Tactic:
hB h
-- 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
hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
g₁ g₂ : G
h : ¬(g₂⁻¹ * g₁) • B = B
⊢ Disjoint ((g₂⁻¹ * g₁) • B) B

Tactic:
exact hB h
-- 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
simp_rw : (∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B) ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B
simp_rw₁ : (∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B) ↔ ∀ ⦃g : G⦄, ¬Disjoint (g • B) B → g • B = B
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B

Tactic:
simp_rw [isBlock_iff_disjoint_smul_of_ne, ← not_disjoint_iff_nonempty_inter, not_imp_comm]

Premises used: not_imp_comm, Set.not_disjoint_iff_nonempty_inter, MulAction.isBlock_iff_disjoint_smul_of_ne
-- 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
⊢ IsBlock G B ↔ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B

Tactic:
isBlock_iff_disjoint_smul_of_ne.trans <| forall_congr' fun _ ↦ or_iff_not_imp_left.symm

Premises used: MulAction.isBlock_iff_disjoint_smul_of_ne, Classical.or_iff_not_imp_left, forall_congr', Iff.trans, Iff.symm
-- 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
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g • a ∈ B → g • B = B

Tactic:
simp [isBlock_iff_smul_eq_of_nonempty, Set.Nonempty, mem_smul_set]

Premises used: Set.mem_smul_set, Set.Nonempty, MulAction.isBlock_iff_smul_eq_of_nonempty
-- 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 G B
⊢ IsBlock.{u_1, u_2} (↥H) B

Tactic:
fun _ _ h ↦ hB h

Premises used: MulAction.IsBlock
-- 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
⊢ IsInvariantBlock G B ↔ IsFixedBlock G B

Tactic:
⟨fun hB g ↦ (hB g).antisymm <| subset_smul_set_iff.2 <| hB _, IsFixedBlock.isInvariantBlock⟩

Premises used: Iff.mpr, Set.subset_smul_set_iff, Inv.inv, MulAction.IsFixedBlock.isInvariantBlock, HasSubset.Subset.antisymm, Iff.intro
-- 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
hB : IsInvariantBlock G B
⊢ IsBlock G B

Tactic:
hB.isFixedBlock.isBlock

Premises used: MulAction.IsInvariantBlock.isFixedBlock, MulAction.IsFixedBlock.isBlock
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
x : G
⊢ HSMul.hSMul (β := Set X) x Set.univ = Set.univ

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
⊢ IsBlock.{u_1, u_2} G (X := X) Set.univ

Tactic:
IsFixedBlock.univ.isBlock

Premises used: MulAction.IsFixedBlock.univ, MulAction.IsFixedBlock.isBlock
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
simp :
  ∀ (h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁)
    (h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂) ⦃g₁ g₂ : G⦄,
    (g₁ • B₁ ∩ g₁ • B₂ ∩ (g₂ • B₁ ∩ g₂ • B₂)).Nonempty → g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂
⊢ IsBlock G (B₁ ∩ B₂)

Tactic:
simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_inter] at h₁ h₂ ⊢

Premises used: Set.smul_set_inter, MulAction.isBlock_iff_smul_eq_smul_of_nonempty
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B₁ B₂ : Set X
h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁
h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂
g₁ g₂ : G
a : X
ha₁ : a ∈ g₁ • B₁ ∩ g₁ • B₂
ha₂ : a ∈ g₂ • B₁ ∩ g₂ • B₂
rw : g₂ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂
rw₁ rw₂ : g₂ • B₁ ∩ g₂ • B₂ = g₂ • B₁ ∩ g₂ • B₂
⊢ g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂

Tactic:
rw [h₁ ⟨a, ha₁.1, ha₂.1⟩, h₂ ⟨a, ha₁.2, ha₂.2⟩]

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
ι : Sort u_3
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
simp :
  ∀ (hB : ∀ (i : ι) ⦃g₁ g₂ : G⦄, (g₁ • B i ∩ g₂ • B i).Nonempty → g₁ • B i = g₂ • B i) ⦃g₁ g₂ : G⦄,
    Set.Nonempty.{u_2} (α := X) ((⋂ (i : ι), g₁ • B i) ∩ ⋂ (i : ι), g₂ • B i) →
      Eq.{u_2 + 1} (α := Set X) (⋂ (i : ι), g₁ • B i) (⋂ (i : ι), g₂ • B i)
⊢ IsBlock.{u_1, u_2} G (X := X) (⋂ (i : ι), B i)

Tactic:
simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_iInter] at hB ⊢

Premises used: MulAction.isBlock_iff_smul_eq_smul_of_nonempty, Set.smul_set_iInter
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
ι : Sort u_3
B : ι → Set X
hB : ∀ (i : ι) ⦃g₁ g₂ : G⦄, (g₁ • B i ∩ g₂ • B i).Nonempty → g₁ • B i = g₂ • B i
g₁ g₂ : G
a : X
ha₁ : Membership.mem (γ := Set X) (⋂ (i : ι), g₁ • B i) a
ha₂ : Membership.mem (γ := Set X) (⋂ (i : ι), g₂ • B i) a
⊢ Eq.{u_2 + 1} (α := Set X) (⋂ (i : ι), g₁ • B i) (⋂ (i : ι), g₂ • B i)

Tactic:
simp_rw [fun i ↦ hB i ⟨a, iInter_subset _ i ha₁, iInter_subset _ i ha₂⟩]

Premises used: And.intro, Exists.intro, Set.iInter_subset, HSMul.hSMul
-- 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
hB : IsTrivialBlock B
inl : ∀ (hB : B.Subsingleton), IsBlock G B
inr : IsBlock.{u_1, u_2} G (X := X) univ
⊢ IsBlock G B

Tactic:
obtain hB | rfl := hB

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
hB : B.Subsingleton
⊢ IsBlock G B

Tactic:
.of_subsingleton hB

Premises used: MulAction.IsBlock.of_subsingleton
-- 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
hB : B.Subsingleton
⊢ IsBlock G B

Tactic:
exact .of_subsingleton hB
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
⊢ IsBlock.{u_1, u_2} G (X := X) univ

Tactic:
.univ

Premises used: MulAction.IsBlock.univ
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
⊢ IsBlock.{u_1, u_2} G (X := X) univ

Tactic:
exact .univ
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
⊢ IsFixedBlock G (orbit G a)

Tactic:
(smul_orbit · a)

Premises used: MulAction.IsFixedBlock, MulAction.smul_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
⊢ IsBlock G (orbit G a)

Tactic:
(IsFixedBlock.orbit a).isBlock

Premises used: MulAction.IsFixedBlock.orbit, MulAction.IsFixedBlock.isBlock
-- 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
⊢ IsBlock.{u_1, u_2} (↥⊤) B ↔ IsBlock G B

Tactic:
Subgroup.topEquiv.toEquiv.forall_congr fun _ ↦ Subgroup.topEquiv.toEquiv.forall_congr_left

Premises used: MulAction.IsBlock, Equiv.forall_congr_left, MulEquiv.toEquiv, Equiv.forall_congr, Subgroup.topEquiv
-- 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 : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : HSMul.hSMul (β := Set Y) g₁ ((⇑j : (a : Y) → X) ⁻¹' B) ≠ HSMul.hSMul (β := Set Y) g₂ ((⇑j : (a : Y) → X) ⁻¹' B)
rw :
  ∀ (hg : Ne.{u_4 + 1} (α := Set Y) ((⇑j : (a : Y) → X) ⁻¹' (φ g₁ • B)) ((⇑j : (a : Y) → X) ⁻¹' (φ g₂ • B))),
    Disjoint.{u_4} (α := Set Y) ((⇑j : (a : Y) → X) ⁻¹' (φ g₁ • B)) ((⇑j : (a : Y) → X) ⁻¹' (φ g₂ • B))
⊢ Disjoint (HSMul.hSMul (β := Set Y) g₁ ((⇑j : (a : Y) → X) ⁻¹' B))
    (HSMul.hSMul (β := Set Y) g₂ ((⇑j : (a : Y) → X) ⁻¹' B))

Tactic:
rw [← Group.preimage_smul_setₛₗ, ← Group.preimage_smul_setₛₗ] at hg ⊢

Premises used: Group.preimage_smul_setₛₗ
-- 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 : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : Ne.{u_4 + 1} (α := Set Y) ((⇑j : (a : Y) → X) ⁻¹' (φ g₁ • B)) ((⇑j : (a : Y) → X) ⁻¹' (φ g₂ • B))
⊢ Disjoint.{u_4} (α := Set Y) ((⇑j : (a : Y) → X) ⁻¹' (φ g₁ • B)) ((⇑j : (a : Y) → X) ⁻¹' (φ g₂ • B))

Tactic:
(hB <| ne_of_apply_ne _ hg).preimage _

Premises used: ne_of_apply_ne, Disjoint.preimage
-- 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 : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : Ne.{u_4 + 1} (α := Set Y) ((⇑j : (a : Y) → X) ⁻¹' (φ g₁ • B)) ((⇑j : (a : Y) → X) ⁻¹' (φ g₂ • B))
⊢ Disjoint.{u_4} (α := Set Y) ((⇑j : (a : Y) → X) ⁻¹' (φ g₁ • B)) ((⇑j : (a : Y) → X) ⁻¹' (φ g₂ • B))

Tactic:
exact (hB <| ne_of_apply_ne _ hg).preimage _

Premises used: ne_of_apply_ne, Disjoint.preimage
-- 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 : Type u_3
Y : Type u_4
inst_2 : SMul H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective.{u_2 + 1, u_4 + 1} (α := X) (β := Y) (⇑j : (a : X) → Y)
hB : IsBlock G B
simp :
  ∀ (x x_1 : G),
    Ne.{u_4 + 1} (α := Set Y) ((⇑j : (a : X) → Y) '' (x • B)) ((⇑j : (a : X) → Y) '' (x_1 • B)) →
      Disjoint.{u_4} (α := Set Y) ((⇑j : (a : X) → Y) '' (x • B)) ((⇑j : (a : X) → Y) '' (x_1 • B))
⊢ IsBlock.{u_3, u_4} H (X := Y) ((⇑j : (a : X) → Y) '' B)

Tactic:
simp only [IsBlock, hφ.forall, ← image_smul_setₛₗ]

Premises used: image_smul_setₛₗ, Function.Surjective.forall, MulAction.IsBlock
-- 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 : Type u_3
Y : Type u_4
inst_2 : SMul H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective.{u_2 + 1, u_4 + 1} (α := X) (β := Y) (⇑j : (a : X) → Y)
hB : IsBlock G B
⊢ ∀ (x x_1 : G),
    Ne.{u_4 + 1} (α := Set Y) ((⇑j : (a : X) → Y) '' (x • B)) ((⇑j : (a : X) → Y) '' (x_1 • B)) →
      Disjoint.{u_4} (α := Set Y) ((⇑j : (a : X) → Y) '' (x • B)) ((⇑j : (a : X) → Y) '' (x_1 • B))

Tactic:
fun g₁ g₂ hg ↦ disjoint_image_of_injective hj <| hB <| ne_of_apply_ne _ hg

Premises used: ne_of_apply_ne, Set.image, DFunLike.coe, 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 : Type u_3
Y : Type u_4
inst_2 : SMul H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective.{u_2 + 1, u_4 + 1} (α := X) (β := Y) (⇑j : (a : X) → Y)
hB : IsBlock G B
⊢ ∀ (x x_1 : G),
    Ne.{u_4 + 1} (α := Set Y) ((⇑j : (a : X) → Y) '' (x • B)) ((⇑j : (a : X) → Y) '' (x_1 • B)) →
      Disjoint.{u_4} (α := Set Y) ((⇑j : (a : X) → Y) '' (x • B)) ((⇑j : (a : X) → Y) '' (x_1 • B))

Tactic:
exact fun g₁ g₂ hg ↦ disjoint_image_of_injective hj <| hB <| ne_of_apply_ne _ hg

Premises used: ne_of_apply_ne, 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
C : SubMulAction G X
hB : IsBlock G B
⊢ IsBlock G (X := ↥C) (Subtype.val (p := fun (x : X) ↦ x ∈ C) ⁻¹' B)

Tactic:
hB.preimage C.inclusion

Premises used: SubMulAction.inclusion, MulAction.IsBlock.preimage
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
C : SubMulAction G X
B : Set ↥C
⊢ IsBlock G (Subtype.val (p := fun (x : X) ↦ x ∈ C) '' B) ↔ IsBlock G B

Tactic:
forall₂_congr fun g₁ g₂ ↦ ?_

Premises used: MulAction.IsBlock, forall₂_congr
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
C : SubMulAction G X
B : Set ↥C
refine :
  ∀ (g₁ g₂ : G),
    g₁ • Subtype.val (p := fun (x : X) ↦ x ∈ C) '' B ≠ g₂ • Subtype.val (p := fun (x : X) ↦ x ∈ C) '' B →
        Disjoint (g₁ • Subtype.val (p := fun (x : X) ↦ x ∈ C) '' B) (g₂ • Subtype.val (p := fun (x : X) ↦ x ∈ C) '' B) ↔
      g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
⊢ IsBlock G (Subtype.val (p := fun (x : X) ↦ x ∈ C) '' B) ↔ IsBlock G B

Tactic:
refine forall₂_congr fun g₁ g₂ ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
rw :
  HSMul.hSMul (β := Set X) g₁ ((⇑C.inclusion : (a : ↥C) → X) '' B) ≠
        HSMul.hSMul (β := Set X) g₂ ((⇑C.inclusion : (a : ↥C) → X) '' B) →
      Disjoint (HSMul.hSMul (β := Set X) g₁ ((⇑C.inclusion : (a : ↥C) → X) '' B))
        (HSMul.hSMul (β := Set X) g₂ ((⇑C.inclusion : (a : ↥C) → X) '' B)) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
rw₁ :
  (⇑C.inclusion : (a : ↥C) → X) '' (g₁ • B) ≠ HSMul.hSMul (β := Set X) g₂ ((⇑C.inclusion : (a : ↥C) → X) '' B) →
      Disjoint ((⇑C.inclusion : (a : ↥C) → X) '' (g₁ • B))
        (HSMul.hSMul (β := Set X) g₂ ((⇑C.inclusion : (a : ↥C) → X) '' B)) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
rw₂ :
  Ne (α := Set X) ((⇑C.inclusion : (a : ↥C) → X) '' (g₁ • B)) ((⇑C.inclusion : (a : ↥C) → X) '' (g₂ • B)) →
      Disjoint (α := Set X) ((⇑C.inclusion : (a : ↥C) → X) '' (g₁ • B)) ((⇑C.inclusion : (a : ↥C) → X) '' (g₂ • B)) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
rw₃ :
  ¬Eq (α := Set X) ((⇑C.inclusion : (a : ↥C) → X) '' (g₁ • B)) ((⇑C.inclusion : (a : ↥C) → X) '' (g₂ • B)) →
      Disjoint (α := Set X) ((⇑C.inclusion : (a : ↥C) → X) '' (g₁ • B)) ((⇑C.inclusion : (a : ↥C) → X) '' (g₂ • B)) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
rw₄ :
  ¬g₁ • B = g₂ • B →
      Disjoint (α := Set X) ((⇑C.inclusion : (a : ↥C) → X) '' (g₁ • B)) ((⇑C.inclusion : (a : ↥C) → X) '' (g₂ • B)) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
rw₅ rw₆ : ¬g₁ • B = g₂ • B → Disjoint (g₁ • B) (g₂ • B) ↔ g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
⊢ g₁ • Subtype.val (p := fun (x : X) ↦ x ∈ C) '' B ≠ g₂ • Subtype.val (p := fun (x : X) ↦ x ∈ C) '' B →
      Disjoint (g₁ • Subtype.val (p := fun (x : X) ↦ x ∈ C) '' B) (g₂ • Subtype.val (p := fun (x : X) ↦ x ∈ C) '' B) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)

Tactic:
rw [← SubMulAction.inclusion.coe_eq, ← image_smul_set, ← image_smul_set, ne_eq,
    Set.image_eq_image C.inclusion_injective, disjoint_image_iff C.inclusion_injective]

Premises used: image_smul_set, SubMulAction.inclusion_injective, Set.image_eq_image, Set.disjoint_image_iff, ne_eq, SubMulAction.inclusion.coe_eq
-- 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
rw :
  ∀
    (g_1 :
      ↥(AddSubgroup.map
          (AddEquiv.toAddMonoidHom
            ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
          H)),
    g_1 +ᵥ g +ᵥ B = g +ᵥ B ∨ Disjoint (g_1 +ᵥ g +ᵥ B) (g +ᵥ B)
⊢ AddAction.IsBlock.{u_3, u_4}
    (↥(AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        H))
    (g +ᵥ B)

Tactic:
rw [AddAction.isBlock_iff_vadd_eq_or_disjoint]

Premises used: AddAction.isBlock_iff_vadd_eq_or_disjoint
-- 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)
obtain :
  ∀ (h : G) (hH : h ∈ H)
    (hh :
      (AddEquiv.toAddMonoidHom
              ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                ((AddAut.conj : (a : G) → Additive (AddAut 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⟩ := AddSubgroup.mem_map.mp (SetLike.coe_mem h')

Premises used: SetLike.coe_mem, Iff.mp, AddSubgroup.mem_map
-- 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)
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_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)
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.vadd_eq_or_disjoint ⟨h, hH⟩).imp

Premises used: Subtype.mk, Or.imp, AddAction.IsBlock.vadd_eq_or_disjoint
-- 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)
this : h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
hB' : 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_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)
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 (AddAction.injective g)

Premises used: AddAction.injective, Set.disjoint_image_of_injective
-- 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)
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 (AddAction.injective g)

Premises used: AddAction.injective, Set.disjoint_image_of_injective
-- 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 +ᵥ 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.vadd_eq_or_disjoint ⟨h, hH⟩).imp
    · intro hB'; congr
    · exact Set.disjoint_image_of_injective (AddAction.injective g)
-- 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)
this : (↑h' : G) +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
⊢ h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B

Tactic:
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)
this : (↑h' : G) +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
⊢ h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B

Tactic:
exact this