awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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₂
⊢ g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂
have rw : g₂ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂
Tactic: rw [h₁ ⟨a, ha₁.1, ha₂.1⟩, h₂ ⟨a, ha₁.2, ha₂.2⟩]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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₂
⊢ g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂
have rw₁ : g₂ • B₁ ∩ g₂ • B₂ = g₂ • B₁ ∩ g₂ • B₂
Tactic: rw [h₁ ⟨a, ha₁.1, ha₂.1⟩, h₂ ⟨a, ha₁.2, ha₂.2⟩]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ IsBlock.{u_1, u_2} G (X := X) (⋂ (i : ι), B i)
have 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)
Tactic: simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_iInter] at hB ⊢
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hB : IsTrivialBlock B
⊢ IsBlock G B
have inl : ∀ (hB : B.Subsingleton), IsBlock G B
Tactic: obtain hB | rfl := hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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
⊢ IsBlock G B
have inr : IsBlock.{u_1, u_2} G (X := X) univ
Tactic: obtain hB | rfl := hB
Cleared hypotheses: B, hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ Disjoint (HSMul.hSMul (β := Set Y) g₁ ((⇑j : (a : Y) → X) ⁻¹' B))
    (HSMul.hSMul (β := Set Y) g₂ ((⇑j : (a : Y) → X) ⁻¹' B))
have 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))
Tactic: rw [← Group.preimage_smul_setₛₗ, ← Group.preimage_smul_setₛₗ] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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
⊢ IsBlock.{u_3, u_4} H (X := Y) ((⇑j : (a : X) → Y) '' B)
have 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))
Tactic: simp only [IsBlock, hφ.forall, ← image_smul_setₛₗ]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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
have 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)
Tactic: refine forall₂_congr fun g₁ g₂ ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ 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)
have rw₅ : ¬g₁ • B = g₂ • B → Disjoint (g₁ • B) (g₂ • 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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
⊢ 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)
have 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)
Tactic: rw [AddAction.isBlock_iff_vadd_eq_or_disjoint]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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 +ᵥ B = g +ᵥ B ∨ Disjoint (h' +ᵥ g +ᵥ B) (g +ᵥ B)
have 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)
Tactic: obtain ⟨h, hH, hh⟩ := AddSubgroup.mem_map.mp (SetLike.coe_mem h')
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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
⊢ h' +ᵥ g +ᵥ B = g +ᵥ B ∨ Disjoint (h' +ᵥ g +ᵥ B) (g +ᵥ B)
have simp : g +ᵥ h +ᵥ B = g +ᵥ B ∨ Disjoint (g +ᵥ h +ᵥ B) (g +ᵥ B)
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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
⊢ g +ᵥ h +ᵥ B = g +ᵥ B ∨ Disjoint (g +ᵥ h +ᵥ B) (g +ᵥ B)
have f : Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hH +ᵥ B = B → g +ᵥ h +ᵥ B = g +ᵥ B
Tactic: apply (hB.vadd_eq_or_disjoint ⟨h, hH⟩).imp
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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 +ᵥ h +ᵥ B = g +ᵥ B ∨ Disjoint (g +ᵥ h +ᵥ B) (g +ᵥ B)
have g₁ : Disjoint (Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hH +ᵥ B) B → Disjoint (g +ᵥ h +ᵥ B) (g +ᵥ B)
Tactic: apply (hB.vadd_eq_or_disjoint ⟨h, hH⟩).imp
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ h' +ᵥ g +ᵥ B = g +ᵥ B ∨ Disjoint (h' +ᵥ g +ᵥ B) (g +ᵥ B)
have suffices : h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ 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)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
have suffices : (↑h' : G) +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
Tactic: suffices (h' : G) +ᵥ (g +ᵥ B) = g +ᵥ (h +ᵥ B) by
    exact this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ (↑h' : G) +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
have rw : (g + h + -g + g) +ᵥ B = (g + h) +ᵥ B
Tactic: rw [← hh, vadd_vadd, vadd_vadd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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
⊢ IsBlock.{u_1, u_2} (↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)) (g • B)
have 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)
Tactic: rw [isBlock_iff_smul_eq_or_disjoint]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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 • B = g • B ∨ Disjoint (h' • g • B) (g • B)
have 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)
Tactic: obtain ⟨h, hH, hh⟩ := Subgroup.mem_map.mp (SetLike.coe_mem h')
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
have simp : g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
have f : Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hH • B = B → g • h • B = g • B
Tactic: apply (hB.smul_eq_or_disjoint ⟨h, hH⟩).imp
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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 • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
have g₁ : Disjoint (Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hH • B) B → Disjoint (g • h • B) (g • B)
Tactic: apply (hB.smul_eq_or_disjoint ⟨h, hH⟩).imp
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
have suffices : h' • g • B = g • h • 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)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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 = g • h • B
have rw : h' • g • B = (↑h' : G) • g • B
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
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)
⊢ h' • g • B = g • h • B
have suffices : (↑h' : G) • g • B = g • h • B
Tactic: suffices (h' : G) • g • B = g • h • B by
    rw [← this]; rfl