awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
g : G
a : α
n : ℕ
rw : a = (g⁻¹ ^ n)⁻¹ • a ↔ g ^ n • a = a
rw₁ : (g⁻¹ ^ n)⁻¹ • a = a ↔ g ^ n • a = a
rw₂ : (HPow.hPow (β := ℤ) g⁻¹ (↑n : ℤ))⁻¹ • a = a ↔ g ^ n • a = a
rw₃ : (HPow.hPow (β := ℤ) g (↑n : ℤ))⁻¹⁻¹ • a = a ↔ g ^ n • a = a
rw₄ : HPow.hPow (β := ℤ) g (↑n : ℤ) • a = a ↔ g ^ n • a = a
rw₅ rw₆ : g ^ n • a = a ↔ g ^ n • a = a
⊢ g⁻¹ ^ n • a = a ↔ g ^ n • a = a

Tactic:
rw [smul_eq_iff_eq_inv_smul, eq_comm, ← zpow_natCast, inv_zpow, inv_inv, zpow_natCast]

Premises used: zpow_natCast, inv_zpow, eq_comm, inv_inv, smul_eq_iff_eq_inv_smul
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
rw : m ^ orderOf m • a = a
rw₁ : HSMul.hSMul.{u, v, v} (α := M) 1 a = a
rw₂ rw₃ : a = a
⊢ period m a ∣ orderOf m

Tactic:
rw [← pow_smul_eq_iff_period_dvd, pow_orderOf_eq_one, one_smul]

Premises used: one_smul, pow_orderOf_eq_one, MulAction.pow_smul_eq_iff_period_dvd
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
order_pos : 0 < orderOf m
a : α
⊢ 0 < period m a

Tactic:
Nat.pos_of_dvd_of_pos (period_dvd_orderOf m a) order_pos

Premises used: Nat.pos_of_dvd_of_pos, MulAction.period_dvd_orderOf
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
order_pos : 0 < orderOf m
a : α
⊢ period m a ≤ orderOf m

Tactic:
Nat.le_of_dvd order_pos (period_dvd_orderOf m a)

Premises used: MulAction.period_dvd_orderOf, Nat.le_of_dvd
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
rw : m ^ Monoid.exponent M • a = a
rw₁ : HSMul.hSMul.{u, v, v} (α := M) 1 a = a
rw₂ rw₃ : a = a
⊢ period m a ∣ Monoid.exponent M

Tactic:
rw [← pow_smul_eq_iff_period_dvd, Monoid.pow_exponent_eq_one, one_smul]

Premises used: one_smul, MulAction.pow_smul_eq_iff_period_dvd, Monoid.pow_exponent_eq_one
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
exp_pos : 0 < Monoid.exponent M
m : M
a : α
⊢ 0 < period m a

Tactic:
Nat.pos_of_dvd_of_pos (period_dvd_exponent m a) exp_pos

Premises used: MulAction.period_dvd_exponent, Nat.pos_of_dvd_of_pos
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
exp_pos : 0 < Monoid.exponent M
m : M
a : α
⊢ period m a ≤ Monoid.exponent M

Tactic:
Nat.le_of_dvd exp_pos (period_dvd_exponent m a)

Premises used: MulAction.period_dvd_exponent, Nat.le_of_dvd
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
exp_pos : 0 < Monoid.exponent M
m : M
h : Membership.mem (γ := Set ℕ) (upperBounds (Set.range fun (a : α) ↦ period m a)) (Monoid.exponent M)
⊢ BddAbove (α := ℕ) (Set.range fun (a : α) ↦ period m a)

Tactic:
use Monoid.exponent M

Premises used: Monoid.exponent
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
exp_pos : 0 < Monoid.exponent M
m : M
⊢ Membership.mem (γ := Set ℕ) (upperBounds (Set.range fun (a : α) ↦ period m a)) (Monoid.exponent M)

Tactic:
simpa [upperBounds] using period_le_exponent exp_pos _

Premises used: upperBounds, MulAction.period_le_exponent
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
c : M
s : Set α
⊢ (⇑f : (a : α) → β) '' (c • s) = HSMul.hSMul (β := Set β) (σ c) ((⇑f : (a : α) → β) '' s)

Tactic:
Semiconj.set_image (map_smulₛₗ f c) s

Premises used: MulActionSemiHomClass.map_smulₛₗ, Function.Semiconj.set_image
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
s : Set α
t : Set β
hst : MapsTo (⇑f : (a : α) → β) s t
c : M
⊢ MapsTo (⇑f : (a : α) → β) (c • s) (σ c • t)

Tactic:
Function.Semiconj.mapsTo_image_right (map_smulₛₗ _ _) hst

Premises used: Function.Semiconj.mapsTo_image_right, MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
c : M
t : Set β
⊢ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t) ⊆ (⇑f : (a : α) → β) ⁻¹' (σ c • t)

Tactic:
((mapsTo_preimage f t).smul_setₛₗ c).subset_preimage

Premises used: Set.MapsTo.subset_preimage, Set.mapsTo_preimage, Set.MapsTo.smul_setₛₗ, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective (β := α) fun (m : α) ↦ c • m
hc' : Injective (β := β) fun (n : β) ↦ σ c • n
⊢ (⇑f : (a : α) → β) ⁻¹' (σ c • t) = HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)

Tactic:
Subset.antisymm ?_ (smul_preimage_set_subsetₛₗ f c t)

Premises used: Set.Subset.antisymm, smul_preimage_set_subsetₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective (β := α) fun (m : α) ↦ c • m
hc' : Injective (β := β) fun (n : β) ↦ σ c • n
refine : (⇑f : (a : α) → β) ⁻¹' (σ c • t) ⊆ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)
⊢ (⇑f : (a : α) → β) ⁻¹' (σ c • t) = HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)

Tactic:
refine Subset.antisymm ?_ (smul_preimage_set_subsetₛₗ f c t)

Premises used: Set.Subset.antisymm, smul_preimage_set_subsetₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective (β := α) fun (m : α) ↦ c • m
hc' : Injective (β := β) fun (n : β) ↦ σ c • n
rw :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' (σ c • t)) (c • x) →
      c • x ∈ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)
⊢ (⇑f : (a : α) → β) ⁻¹' (σ c • t) ⊆ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)

Tactic:
rw [subset_def, hc.forall]

Premises used: Function.Surjective.forall, Set.subset_def
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective (β := α) fun (m : α) ↦ c • m
hc' : Injective (β := β) fun (n : β) ↦ σ c • n
x : α
y : β
hy : y ∈ t
hxy : Eq.{u_5 + 1} (α := β) ((fun (x : β) ↦ σ c • x) y : β) ((f : (a : α) → β) (c • x) : β)
⊢ y = (f : (a : α) → β) x

Tactic:
rw [map_smulₛₗ, hc'.eq_iff] at hxy

Premises used: Function.Injective.eq_iff, MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective (β := α) fun (m : α) ↦ c • m
hc' : Injective (β := β) fun (n : β) ↦ σ c • n
x : α
y : β
hy : y ∈ t
hxy : y = (f : (a : α) → β) x
⊢ Membership.mem (α := β) t ((f : (a : α) → β) x : β)

Tactic:
subst y
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective (β := α) fun (m : α) ↦ c • m
hc' : Injective (β := β) fun (n : β) ↦ σ c • n
x : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
⊢ c • x ∈ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)

Tactic:
smul_mem_smul_set hy

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective (β := α) fun (m : α) ↦ c • m
hc' : Injective (β := β) fun (n : β) ↦ σ c • n
x : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
⊢ c • x ∈ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)

Tactic:
exact smul_mem_smul_set hy

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
inst_4 : FunLike F α β
inst_5 : MulActionSemiHomClass F σ α β
c : M
f : F
hc : IsUnit c
hc' : IsUnit (σ c)
t : Set β
⊢ (⇑f : (a : α) → β) ⁻¹' (σ c • t) = HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)

Tactic:
preimage_smul_setₛₗ' hc.smul_bijective.surjective hc'.smul_bijective.injective

Premises used: Function.Bijective.injective, Function.Bijective.surjective, IsUnit.smul_bijective, preimage_smul_setₛₗ'
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
α : Type u_4
β : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
c : M
F : Type u_6
G : Type u_7
inst_4 : FunLike G M N
inst_5 : MonoidHomClass G M N
σ : G
inst_6 : FunLike F α β
inst_7 : MulActionSemiHomClass.{u_6, u_1, u_2, u_4, u_5} F (M := M) (N := N) (⇑σ : (a : M) → N) α β
f : F
hc : IsUnit c
t : Set β
⊢ (⇑f : (a : α) → β) ⁻¹' HSMul.hSMul.{u_2, u_5, u_5} (α := N) ((σ : (a : M) → N) c : N) t =
    HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)

Tactic:
preimage_smul_setₛₗ_of_isUnit_isUnit _ hc (hc.map _) _

Premises used: preimage_smul_setₛₗ_of_isUnit_isUnit, IsUnit.map
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
N : Type u_2
α : Type u_4
β : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
c : M
F : Type u_6
σ : M →* N
inst_4 : FunLike F α β
inst_5 : MulActionSemiHomClass.{u_6, u_1, u_2, u_4, u_5} F (M := M) (N := N) (⇑σ : (a : M) → N) α β
f : F
hc : IsUnit c
t : Set β
⊢ (⇑f : (a : α) → β) ⁻¹' HSMul.hSMul.{u_2, u_5, u_5} (α := N) ((σ : (a : M) → N) c : N) t =
    HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)

Tactic:
hc.preimage_smul_setₛₗ σ f t

Premises used: IsUnit.preimage_smul_setₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
σ : G → H
inst_2 : MulAction G α
inst_3 : MulAction H β
F : Type u_5
inst_4 : FunLike F α β
inst_5 : MulActionSemiHomClass F σ α β
f : F
c : G
t : Set β
⊢ (⇑f : (a : α) → β) ⁻¹' (σ c • t) = HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)

Tactic:
preimage_smul_setₛₗ_of_isUnit_isUnit _ (Group.isUnit _) (Group.isUnit _) _

Premises used: Group.isUnit, preimage_smul_setₛₗ_of_isUnit_isUnit
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : FunLike F α β
inst_3 : MulActionHomClass F M α β
f : F
c : M
s : Set α
⊢ (⇑f : (a : α) → β) '' (c • s) = HSMul.hSMul (β := Set β) c ((⇑f : (a : α) → β) '' s)

Tactic:
image_smul_setₛₗ f c s

Premises used: image_smul_setₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : FunLike F α β
inst_3 : MulActionHomClass F M α β
f : F
c : M
t : Set β
⊢ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t) ⊆ (⇑f : (a : α) → β) ⁻¹' (c • t)

Tactic:
smul_preimage_set_subsetₛₗ f c t

Premises used: smul_preimage_set_subsetₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : FunLike F α β
inst_3 : MulActionHomClass F M α β
f : F
s : Set α
t : Set β
hst : MapsTo (⇑f : (a : α) → β) s t
c : M
⊢ MapsTo (⇑f : (a : α) → β) (c • s) (c • t)

Tactic:
hst.smul_setₛₗ c

Premises used: Set.MapsTo.smul_setₛₗ
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
inst_3 : FunLike F α β
inst_4 : MulActionHomClass F M α β
f : F
c : M
hc : IsUnit c
t : Set β
⊢ (⇑f : (a : α) → β) ⁻¹' (c • t) = HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)

Tactic:
preimage_smul_setₛₗ_of_isUnit_isUnit f hc hc t

Premises used: preimage_smul_setₛₗ_of_isUnit_isUnit
-- Module: Mathlib.GroupTheory.GroupAction.Pointwise
Goal:
G : Type u_1
inst : Group G
α : Type u_2
β : Type u_3
inst_1 : MulAction G α
inst_2 : MulAction G β
F : Type u_4
inst_3 : FunLike F α β
inst_4 : MulActionHomClass F G α β
f : F
c : G
t : Set β
⊢ (⇑f : (a : α) → β) ⁻¹' (c • t) = HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)

Tactic:
(Group.isUnit c).preimage_smul_set f t

Premises used: Group.isUnit, IsUnit.preimage_smul_set
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
inst_1 : IsPreprimitive G X
B : Set X
hB : IsBlock G B
⊢ B.Subsingleton ∨ B = Set.univ

Tactic:
isTrivialBlock_of_isBlock hB

Premises used: MulAction.IsPreprimitive.isTrivialBlock_of_isBlock, MulAction.IsTrivialBlock
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
inst_1 : Nonempty G
inst_2 : Subsingleton X
x y : X
h : Classical.arbitrary G • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
use Classical.arbitrary G

Premises used: Classical.arbitrary
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
inst_1 : Nonempty G
inst_2 : Subsingleton X
x y : X
h : True
⊢ Classical.arbitrary G • x = y

Tactic:
rw [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
inst_1 : Nonempty G
inst_2 : Subsingleton X
x y : X
⊢ True

Tactic:
trivial
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
inst_1 : Nonempty G
inst_2 : Subsingleton X
B_1 : Set X
B : IsBlock G B_1
h : B_1.Subsingleton
⊢ IsTrivialBlock B_1

Tactic:
left
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
inst_1 : Nonempty G
inst_2 : Subsingleton X
B_1 : Set X
B : IsBlock G B_1
⊢ B_1.Subsingleton

Tactic:
Set.subsingleton_of_subsingleton

Premises used: Set.subsingleton_of_subsingleton
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
inst_1 : Nonempty G
inst_2 : Subsingleton X
B_1 : Set X
B : IsBlock G B_1
⊢ B_1.Subsingleton

Tactic:
exact Set.subsingleton_of_subsingleton

Premises used: Set.subsingleton_of_subsingleton
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
X : Type u_2
inst : Finite X
hX : Nat.card X ≤ 2
B : Set X
rw : B.ncard ≤ 1 ∨ B.ncard = Nat.card X
⊢ IsTrivialBlock B

Tactic:
rw [IsTrivialBlock, ← B.ncard_le_one_iff_subsingleton, B.eq_univ_iff_ncard]

Premises used: Set.ncard_le_one_iff_subsingleton, Set.eq_univ_iff_ncard, MulAction.IsTrivialBlock
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
X : Type u_2
inst : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ B.ncard ≤ Nat.card X

Tactic:
have := B.ncard_le_card
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
X : Type u_2
inst : Finite X
hX : Nat.card X ≤ 2
B : Set X
this : B.ncard ≤ Nat.card X
⊢ B.ncard ≤ 1 ∨ B.ncard = Nat.card X

Tactic:
grind
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
inl : ∀ (hB : IsBlock.{u_1, u_2} G (X := X) ∅), IsTrivialBlock.{u_2} (X := X) ∅
inr : ∀ (b : X) (hb : b ∈ B), IsTrivialBlock B
⊢ IsTrivialBlock B

Tactic:
obtain rfl | ⟨b, hb⟩ := B.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
hB : IsBlock.{u_1, u_2} G (X := X) ∅
⊢ IsTrivialBlock.{u_2} (X := X) ∅

Tactic:
simp [IsTrivialBlock]

Premises used: MulAction.IsTrivialBlock
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
inr : ∀ (g : G) (hg : g • b = a), IsTrivialBlock B
⊢ IsTrivialBlock B

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

Premises used: MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
inr : IsTrivialBlock (g • B)
⊢ IsTrivialBlock B

Tactic:
rw [← IsTrivialBlock.smul_iff g]

Premises used: MulAction.IsTrivialBlock.smul_iff
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
apply : a ∈ g • B
⊢ IsTrivialBlock (g • B)

Tactic:
apply H _ (hB.translate g)

Premises used: MulAction.IsBlock.translate
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
rw : g • b ∈ g • B
⊢ a ∈ g • B

Tactic:
rw [← hg]
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
w : X
h : b ∈ B ∧ (fun (x : X) ↦ g • x) b = g • b
⊢ g • b ∈ g • B

Tactic:
use b
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
rw : ∀ (x : X), ∃ (g : G), g • a = x
⊢ IsPretransitive G X

Tactic:
rw [isPretransitive_iff_base a]

Premises used: MulAction.isPretransitive_iff_base
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
inl : ∀ (H : (orbit G a).Subsingleton) (x : X), ∃ (g : G), g • a = x
inr : ∀ (H : orbit G a = Set.univ) (x : X), ∃ (g : G), g • a = x
⊢ ∀ (x : X), ∃ (g : G), g • a = x

Tactic:
rcases H (mem_orbit_self a) (IsBlock.orbit a) with H | H

Premises used: MulAction.IsBlock.orbit, MulAction.mem_orbit_self
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : (orbit G a).Subsingleton
inl : False
⊢ ∀ (x : X), ∃ (g : G), g • a = x

Tactic:
exfalso
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : (orbit G a).Subsingleton
inl : a ∈ fixedPoints G X
⊢ False

Tactic:
apply ha
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : (orbit G a).Subsingleton
⊢ orbit G a = {a}

Tactic:
rw [Set.subsingleton_iff_singleton (mem_orbit_self a)] at H

Premises used: Set.subsingleton_iff_singleton, MulAction.mem_orbit_self
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
inl : g • a ∈ orbit G a
⊢ Membership.mem (γ := Set X) {a} (g • a)

Tactic:
rw [← H]
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a ∈ orbit G a

Tactic:
mem_orbit a g

Premises used: MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a ∈ orbit G a

Tactic:
exact mem_orbit a g

Premises used: MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = Set.univ
x : X
inr : Membership.mem (γ := Set X) Set.univ x
⊢ ∃ (g : G), g • a = x

Tactic:
rw [← MulAction.mem_orbit_iff, H]

Premises used: MulAction.mem_orbit_iff
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = Set.univ
x : X
⊢ Membership.mem (γ := Set X) Set.univ x

Tactic:
Set.mem_univ x

Premises used: Set.mem_univ
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = Set.univ
x : X
⊢ Membership.mem (γ := Set X) Set.univ x

Tactic:
exact Set.mem_univ x

Premises used: Set.mem_univ
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
inl : ∀ (hB : IsBlock.{u_1, u_2} G (X := X) ∅), IsTrivialBlock.{u_2} (X := X) ∅
inr : ∀ (b : X) (hb : b ∈ B), IsTrivialBlock B
⊢ IsTrivialBlock B

Tactic:
obtain rfl | ⟨b, hb⟩ := B.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
hB : IsBlock.{u_1, u_2} G (X := X) ∅
⊢ IsTrivialBlock.{u_2} (X := X) ∅

Tactic:
simp [IsTrivialBlock]

Premises used: MulAction.IsTrivialBlock
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
inr : ∀ (g : G) (hg : g • b = a), IsTrivialBlock B
⊢ IsTrivialBlock B

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

Premises used: MulAction.exists_smul_eq