awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) g

Tactic:
hyp hg
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) g

Tactic:
exact hyp hg
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
mpr : s ⊆ g • s
⊢ g • s = s

Tactic:
apply subset_antisymm (hyp g hg)

Premises used: subset_antisymm
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
h : g⁻¹ • x ∈ s ∧ (fun (x : α) ↦ g • x) (g⁻¹ • x) = x
⊢ x ∈ g • s

Tactic:
use g⁻¹ • x
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
h : g⁻¹ • x ∈ s
h₁ : (fun (x : α) ↦ g • x) (g⁻¹ • x) = x
⊢ g⁻¹ • x ∈ s ∧ (fun (x : α) ↦ g • x) (g⁻¹ • x) = x

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
h : g⁻¹ • x ∈ g⁻¹ • s
⊢ g⁻¹ • x ∈ s

Tactic:
apply hyp g⁻¹ (inv_mem hg)

Premises used: InvMemClass.inv_mem, Inv.inv
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ g⁻¹ • s

Tactic:
simp only [Set.smul_mem_smul_set_iff, hx]

Premises used: Set.smul_mem_smul_set_iff
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun (x : α) ↦ g • x) (g⁻¹ • x) = x

Tactic:
simp only [smul_inv_smul]

Premises used: smul_inv_smul
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
rw : LE.le.{u_1} (α := Subgroup Rˣ) (MulAction.stabilizer Rˣ x) ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup Rˣ) (MulAction.stabilizer Rˣ x) ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
x₁ : ∀ (hg : (↑g : R) • x = x), Membership.mem (γ := Subgroup Rˣ) ⊥ g
⊢ Membership.mem (γ := Subgroup Rˣ) (MulAction.stabilizer Rˣ x) g → Membership.mem (γ := Subgroup Rˣ) ⊥ g

Tactic:
(hg : g.val • x = x)
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : (↑g : R) • x = x
huv : (↑g : R) = (↑1 : R)
⊢ Membership.mem (γ := Subgroup Rˣ) ⊥ g

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : (↑g : R) • x = x
huv : (↑g : R) - (↑1 : R) = 0
huv₁ : ((↑g : R) - (↑1 : R)) • x = 0
huv₂ : ((↑g : R) - 1) • x = 0
huv₃ : (↑g : R) • x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x = 0
huv₄ : x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x = 0
huv₅ : x - x = 0
huv₆ huv₇ : Eq.{u_2 + 1} (α := M) 0 0
⊢ (↑g : R) = (↑1 : R)

Tactic:
rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]

Premises used: sub_self, sub_eq_zero, sub_smul, smul_eq_zero_iff_left, one_smul, Units.val_one
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a b : X
apply : ¬Disjoint (orbit G a) (orbit G b) → orbit G a = orbit G b
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)

Tactic:
apply (em (Disjoint (orbit G a) (orbit G b))).symm.imp _ id

Premises used: Disjoint, em, id, MulAction.orbit, Or.symm, Or.imp
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a b : X
⊢ ¬Disjoint (orbit G a) (orbit G b) → orbit G a = orbit G b

Tactic:
simp +contextual
    only [Set.not_disjoint_iff, ← orbit_eq_iff, forall_exists_index, eq_comm, implies_true]

Premises used: forall_exists_index, eq_comm, Set.not_disjoint_iff, MulAction.orbit_eq_iff, implies_true
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
x y : X
h : Ne.{u_2 + 1} (α := Set X) ((fun (x : X) ↦ orbit G x) x) ((fun (x : X) ↦ orbit G x) y)
contrapose! : ∀ (h : ¬Function.onFun Disjoint id (orbit G x) (orbit G y)), orbit G x = orbit G y
⊢ Function.onFun.{u_2 + 1, u_2 + 1, 1} (α := Set X) Disjoint id ((fun (x : X) ↦ orbit G x) x)
    ((fun (x : X) ↦ orbit G x) y)

Tactic:
contrapose! h
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
x y : X
h : ¬Function.onFun Disjoint id (orbit G x) (orbit G y)
⊢ orbit G x = orbit G y

Tactic:
(orbit.eq_or_disjoint x y).resolve_right h

Premises used: MulAction.orbit.eq_or_disjoint, Or.resolve_right
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
x y : X
h : ¬Function.onFun Disjoint id (orbit G x) (orbit G y)
⊢ orbit G x = orbit G y

Tactic:
exact (orbit.eq_or_disjoint x y).resolve_right h

Premises used: MulAction.orbit.eq_or_disjoint, Or.resolve_right
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
h₂ : ∀ (a : X), ∃ (x : Set X), Membership.mem (γ := Set (Set X)) (range fun (x : X) ↦ orbit G x) x ∧ a ∈ x
h₃ : ∅ ∉ range fun (x : X) ↦ orbit G x
⊢ Setoid.IsPartition.{u_2} (α := X) (range fun (a : X) ↦ orbit G a)

Tactic:
apply orbit.pairwiseDisjoint.isPartition_of_exists_of_ne_empty

Premises used: Set.PairwiseDisjoint.isPartition_of_exists_of_ne_empty, MulAction.orbit.pairwiseDisjoint
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
x : X
⊢ ∃ (x_1 : Set X), Membership.mem (γ := Set (Set X)) (range fun (x : X) ↦ orbit G x) x_1 ∧ x ∈ x_1

Tactic:
⟨_, ⟨x, rfl⟩, mem_orbit_self x⟩

Premises used: And.intro, Exists.intro, rfl, MulAction.mem_orbit_self
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
x : X
⊢ ∃ (x_1 : Set X), Membership.mem (γ := Set (Set X)) (range fun (x : X) ↦ orbit G x) x_1 ∧ x ∈ x_1

Tactic:
exact ⟨_, ⟨x, rfl⟩, mem_orbit_self x⟩
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
ha : orbit G a = ∅
⊢ False

Tactic:
(MulAction.nonempty_orbit a).ne_empty ha

Premises used: MulAction.nonempty_orbit, 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
a : X
ha : orbit G a = ∅
⊢ False

Tactic:
exact (MulAction.nonempty_orbit a).ne_empty ha

Premises used: MulAction.nonempty_orbit, Set.Nonempty.ne_empty
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set α
hB : IsTrivialBlock B
inl : ∀ (hB : B.Subsingleton), IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)
inr : ∀ (hB : B = univ), IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)
⊢ IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)

Tactic:
obtain hB | hB := hB
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set α
hB : B.Subsingleton
inl : Set.Subsingleton.{u_6} (α := β) ((⇑f : (a : α) → β) '' B)
⊢ IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)

Tactic:
apply Or.intro_left

Premises used: Or.intro_left
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set α
hB : B.Subsingleton
⊢ Set.Subsingleton.{u_6} (α := β) ((⇑f : (a : α) → β) '' B)

Tactic:
apply Set.Subsingleton.image hB

Premises used: Set.Subsingleton.image
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set α
hB : B = univ
inr : Eq.{u_6 + 1} (α := Set β) ((⇑f : (a : α) → β) '' B) univ
⊢ IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)

Tactic:
apply Or.intro_right

Premises used: Or.intro_right
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set α
hB : B = univ
inr : Eq.{u_6 + 1} (α := Set β) (Set.image.{u_4, u_6} (α := α) (⇑f : (a : α) → β) univ) univ
⊢ Eq.{u_6 + 1} (α := Set β) ((⇑f : (a : α) → β) '' B) univ

Tactic:
rw [hB]
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set α
hB : B = univ
⊢ Eq.{u_6 + 1} (α := Set β) (Set.image.{u_4, u_6} (α := α) (⇑f : (a : α) → β) univ) univ

Tactic:
simp only [Set.image_univ, Set.range_eq_univ, hf]

Premises used: Set.range_eq_univ, Set.image_univ
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : IsTrivialBlock B
inl : ∀ (hB : B.Subsingleton), IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)
inr : ∀ (hB : B = univ), IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)
⊢ IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)

Tactic:
obtain hB | hB := hB
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : B.Subsingleton
inl : Set.Subsingleton.{u_4} (α := α) ((⇑f : (a : α) → β) ⁻¹' B)
⊢ IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)

Tactic:
apply Or.intro_left

Premises used: Or.intro_left
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : B.Subsingleton
⊢ Set.Subsingleton.{u_4} (α := α) ((⇑f : (a : α) → β) ⁻¹' B)

Tactic:
Set.Subsingleton.preimage hB hf

Premises used: Set.Subsingleton.preimage
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : B.Subsingleton
⊢ Set.Subsingleton.{u_4} (α := α) ((⇑f : (a : α) → β) ⁻¹' B)

Tactic:
exact Set.Subsingleton.preimage hB hf

Premises used: Set.Subsingleton.preimage
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : B = univ
inr : Eq.{u_4 + 1} (α := Set α) ((⇑f : (a : α) → β) ⁻¹' B) univ
⊢ IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)

Tactic:
apply Or.intro_right

Premises used: Or.intro_right
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : B = univ
inr : Eq.{u_4 + 1} (α := Set α) (Set.preimage.{u_4, u_6} (β := β) (⇑f : (a : α) → β) univ) univ
⊢ Eq.{u_4 + 1} (α := Set α) ((⇑f : (a : α) → β) ⁻¹' B) univ

Tactic:
simp only [hB]
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : B = univ
⊢ Eq.{u_4 + 1} (α := Set α) (Set.preimage.{u_4, u_6} (β := β) (⇑f : (a : α) → β) univ) univ

Tactic:
apply Set.preimage_univ

Premises used: Set.preimage_univ
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
h : B.Subsingleton
inl : (g • B).Subsingleton
⊢ IsTrivialBlock (g • B)

Tactic:
left
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
h : B.Subsingleton
⊢ (g • B).Subsingleton

Tactic:
(Function.Injective.subsingleton_image_iff (MulAction.injective g)).mpr h

Premises used: Iff.mpr, Function.Injective.subsingleton_image_iff, MulAction.injective
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
h : B.Subsingleton
⊢ (g • B).Subsingleton

Tactic:
exact (Function.Injective.subsingleton_image_iff (MulAction.injective g)).mpr h

Premises used: Iff.mpr, Function.Injective.subsingleton_image_iff, MulAction.injective
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
h : B = univ
inr : g • B = univ
⊢ IsTrivialBlock (g • B)

Tactic:
right
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
h : B = univ
inr : HSMul.hSMul (β := Set α) g univ = univ
inr₁ : Eq.{u_4 + 1} (α := Set α) ((fun (x : α) ↦ g • x) '' univ) univ
inr₂ inr₃ : Eq.{u_4 + 1} (α := Set α) univ univ
⊢ g • B = univ

Tactic:
rw [h, ← Set.image_smul, Set.image_univ_of_surjective (MulAction.surjective g)]

Premises used: Set.image_smul, Set.image_univ_of_surjective, MulAction.surjective
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
hB : IsTrivialBlock B
g : M
inl : ∀ (h : B.Subsingleton), IsTrivialBlock (g • B)
inr : ∀ (h : B = univ), IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g • B)

Tactic:
cases hB with
  | inl h =>
    left
    exact (Function.Injective.subsingleton_image_iff (MulAction.injective g)).mpr h
  | inr h =>
    right
    rw [h, ← Set.image_smul, Set.image_univ_of_surjective (MulAction.surjective g)]

Premises used: Set.image_smul, Set.image_univ_of_surjective, MulAction.surjective
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
mp : IsTrivialBlock (g • B) → IsTrivialBlock B
mpr : IsTrivialBlock B → IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g • B) ↔ IsTrivialBlock B

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
H : IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g⁻¹ • g • B)

Tactic:
IsTrivialBlock.smul H g⁻¹

Premises used: MulAction.IsTrivialBlock.smul, Inv.inv
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
H : IsTrivialBlock (g • B)
h : B = g⁻¹ • g • B
⊢ IsTrivialBlock B

Tactic:
convert! IsTrivialBlock.smul H g⁻¹

Premises used: MulAction.IsTrivialBlock.smul, Inv.inv
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
H : IsTrivialBlock (g • B)
⊢ B = g⁻¹ • g • B

Tactic:
simp only [inv_smul_smul]

Premises used: inv_smul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
H : IsTrivialBlock B
⊢ IsTrivialBlock (g • B)

Tactic:
IsTrivialBlock.smul H g

Premises used: MulAction.IsTrivialBlock.smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
H : IsTrivialBlock B
⊢ IsTrivialBlock (g • B)

Tactic:
exact IsTrivialBlock.smul H g

Premises used: MulAction.IsTrivialBlock.smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
simp_rw :
  (∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)) ↔
    ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B
simp_rw₁ :
  (∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)) ↔
    ∀ ⦃g₁ g₂ : G⦄, ¬Disjoint (g₁ • B) (g₂ • B) → g₁ • B = g₂ • B
⊢ IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B

Tactic:
simp_rw [IsBlock, ← not_disjoint_iff_nonempty_inter, not_imp_comm]

Premises used: MulAction.IsBlock, not_imp_comm, Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
⊢ IsBlock G B ↔ PairwiseDisjoint.{u_2, u_2} (α := Set X) (range fun (g : G) ↦ g • B) id

Tactic:
pairwiseDisjoint_range_iff.symm

Premises used: Set.pairwiseDisjoint_range_iff, MulAction.IsBlock, Iff.symm
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
⊢ IsBlock G B ↔ ∀ (g₁ g₂ : G), g₁ • B = g₂ • B ∨ Disjoint (g₁ • B) (g₂ • B)

Tactic:
forall₂_congr fun _ _ ↦ or_iff_not_imp_left.symm

Premises used: MulAction.IsBlock, forall₂_congr, Classical.or_iff_not_imp_left, Iff.symm
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
by_contra! : ∀ (hg' : g₁ • B ≠ g₂ • B), False
⊢ g₁ • B = g₂ • B

Tactic:
by_contra! hg'
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
⊢ B = ∅

Tactic:
simpa using (hB hg').eq_bot_of_le hg

Premises used: Disjoint.eq_bot_of_le
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
⊢ IsBlock.{u_1, u_2} G (X := X) ∅

Tactic:
obtain rfl : B = ∅ := by simpa using (hB hg').eq_bot_of_le hg

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
hB₁ : IsBlock.{u_1, u_2} G (X := X) ∅
⊢ HSMul.hSMul (β := Set X) g₁ ∅ ⊆ HSMul.hSMul (β := Set X) g₂ ∅

Tactic:
obtain rfl : B = ∅ := by simpa using (hB hg').eq_bot_of_le hg

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
hB₁ : IsBlock.{u_1, u_2} G (X := X) ∅
hg₁ : HSMul.hSMul (β := Set X) g₁ ∅ ⊆ HSMul.hSMul (β := Set X) g₂ ∅
⊢ HSMul.hSMul (β := Set X) g₁ ∅ ≠ HSMul.hSMul (β := Set X) g₂ ∅

Tactic:
obtain rfl : B = ∅ := by simpa using (hB hg').eq_bot_of_le hg

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
g₁ g₂ : G
hB : IsBlock.{u_1, u_2} G (X := X) ∅
hg : HSMul.hSMul (β := Set X) g₁ ∅ ⊆ HSMul.hSMul (β := Set X) g₂ ∅
hg' : HSMul.hSMul (β := Set X) g₁ ∅ ≠ HSMul.hSMul (β := Set X) g₂ ∅
⊢ False

Tactic:
simp at hg'
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
⊢ ¬g₁ • B ⊂ g₂ • B

Tactic:
fun hab ↦ hab.ne <| hB.smul_eq_smul_of_subset hab.subset

Premises used: HasSSubset.SSubset.subset, MulAction.IsBlock.smul_eq_smul_of_subset, HasSSubset.SSubset.ne, Not
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
rw : ∀ (i : G) (j : i ∈ s), Disjoint (g • B) (i • B)
⊢ Disjoint (g • B) (s • B)

Tactic:
rw [← iUnion_smul_set, disjoint_iUnion₂_right]

Premises used: Set.disjoint_iUnion₂_right, Set.iUnion_smul_set
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ ∀ (i : G) (j : i ∈ s), Disjoint (g • B) (i • B)

Tactic:
fun b hb ↦ hB fun h ↦ hgs <| h.trans_subset <| smul_set_subset_smul hb

Premises used: Set.smul_set_subset_smul, Eq.trans_subset
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ ∀ (i : G) (j : i ∈ s), Disjoint (g • B) (i • B)

Tactic:
exact fun b hb ↦ hB fun h ↦ hgs <| h.trans_subset <| smul_set_subset_smul hb

Premises used: Set.smul_set_subset_smul, Eq.trans_subset
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ Disjoint (s • B) (g • B)

Tactic:
(hB.disjoint_smul_set_smul hgs).symm

Premises used: MulAction.IsBlock.disjoint_smul_set_smul, Disjoint.symm
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
hfB : IsFixedBlock G B
⊢ IsBlock G B

Tactic:
simp [IsBlock, hfB _]

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

Tactic:
simp [IsBlock]

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

Tactic:
simp [IsBlock]

Premises used: MulAction.IsBlock
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
hB : B.Subsingleton
⊢ IsBlock G B

Tactic:
hB.induction_on .empty fun _ ↦ .singleton

Premises used: Set.Subsingleton.induction_on, MulAction.IsBlock.empty, MulAction.IsBlock.singleton
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
hB : IsFixedBlock G B
⊢ IsInvariantBlock G B

Tactic:
fun _ ↦ (hB _).le

Premises used: Eq.le, MulAction.IsInvariantBlock