awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
N : Type u_3
β : Type u_4
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : M
hk : Membership.mem (γ := Subgroup N) (fixingSubgroup N t) (φ k)
⊢ ∃ (a : ↥(fixingSubgroup M s)),
    ψ a = Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ k) hk
have right : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
Tactic: suffices k ∈ fixingSubgroup M s by
        use ⟨k, this⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
N : Type u_3
β : Type u_4
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : M
hk : Membership.mem (γ := Subgroup N) (fixingSubgroup N t) (φ k)
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
have right : ∀ (hk : ∀ (y : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y → φ k • y = y), ∀ y ∈ s, k • y = y
Tactic: simp only [mem_fixingSubgroup_iff, t] at hk ⊢
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
N : Type u_3
β : Type u_4
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : M
hk : ∀ (y : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y → φ k • y = y
y : α
hy : y ∈ s
⊢ k • y = y
have right : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (k • y) : β) ((f : (a : α) → β) y : β)
Tactic: apply hf.injective
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
N : Type u_3
β : Type u_4
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : M
hk : ∀ (y : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y → φ k • y = y
y : α
hy : y ∈ s
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (k • y) : β) ((f : (a : α) → β) y : β)
have right : Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) y : β)
Tactic: rw [map_smulₛₗ, hk]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
N : Type u_3
β : Type u_4
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
⊢ Function.Bijective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
have right : Function.Injective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
  (⇑g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
N : Type u_3
β : Type u_4
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
right :
  Function.Injective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
⊢ Function.Bijective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
have right₁ : Function.Surjective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
  (⇑g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
N : Type u_3
β : Type u_4
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
y : α
hy : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) y
h :
  Eq.{u_4 + 1} (α := ↥(ofFixingSubgroup N t))
    ((g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx) :
      ↥(ofFixingSubgroup N t))
    ((g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y hy) :
      ↥(ofFixingSubgroup N t))
⊢ Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y hy
have right : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
Tactic: suffices f x = f y by
          simpa [← Subtype.coe_inj, hf.injective.eq_iff] using this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
N : Type u_3
β : Type u_4
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
x : β
hx : Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x
⊢ ∃ (a : ↥(ofFixingSubgroup M s)),
    (g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t)) a =
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) x hx
have right : ∀ (y : α)
  (hx :
    Membership.mem (α := β) (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t)
      ((f : (a : α) → β) y : β)),
  ∃ (a : ↥(ofFixingSubgroup M s)),
    Eq.{u_4 + 1} (α := ↥(ofFixingSubgroup N t))
      ((g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t)) a : ↥(ofFixingSubgroup N t))
      (Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
          ((f : (a : α) → β) y) hx :
        ↥(ofFixingSubgroup N t))
Tactic: obtain ⟨y, rfl⟩ := hf.surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
N : Type u_3
β : Type u_4
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
y : α
hx :
  Membership.mem (α := β) (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t)
    ((f : (a : α) → β) y : β)
⊢ ∃ (a : ↥(ofFixingSubgroup M s)),
    Eq.{u_4 + 1} (α := ↥(ofFixingSubgroup N t))
      ((g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t)) a : ↥(ofFixingSubgroup N t))
      (Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
          ((f : (a : α) → β) y) hx :
        ↥(ofFixingSubgroup N t))
have right : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) y
Tactic: suffices y ∈ ofFixingSubgroup M s by
          exact ⟨⟨y, this⟩, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (hypothesis)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
N : Type u_3
β : Type u_4
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
y : α
hx :
  Membership.mem (α := β) (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t)
    ((f : (a : α) → β) y : β)
⊢ Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) y
have hx₁ : ∀ x ∈ s, ¬Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
Tactic: simp only [mem_ofFixingSubgroup_iff, Set.mem_image, not_exists, not_and, t] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.OfQuotient (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : MulAction G A
H : Subgroup G
inst_2 : H.Normal
g : G
hg : g ∈ H
⊢ Membership.mem (γ := Subgroup G)
    (MonoidHom.ker.{u_1, u_2} (M := Function.End (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2)) toEndHom) g
have h : ∀ (a : (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2)),
  Eq.{u_2 + 1} (α := (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2))
    ((toEndHom : (a : G) → Function.End (↑(fixedPoints (↥H) A) : Type u_2)) g a :
      (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2))
    (1 a : (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2))
Tactic: funext a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.OfQuotient (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : MulAction G A
H : Subgroup G
inst_2 : H.Normal
g : G
hg : g ∈ H
a : (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2)
⊢ Eq.{u_2 + 1} (α := (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2))
    ((toEndHom : (a : G) → Function.End (↑(fixedPoints (↥H) A) : Type u_2)) g a :
      (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2))
    (1 a : (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2))
have h : Eq.{u_2 + 1} (α := A) (↑((toEndHom : (a : G) → Function.End (↑(fixedPoints (↥H) A) : Type u_2)) g a) : A) (↑(1 a) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.OfQuotient (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : MulAction G A
H : Subgroup G
inst_2 : H.Normal
g : G ⧸ H
a : (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2)
| g • a
have rw : ⟦Quotient.out g⟧ • a
Tactic: rw [← g.out_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.OfQuotient (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : MulAction G A
H : Subgroup G
inst_2 : H.Normal
g : G ⧸ H
a : (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2)
⊢ Quotient.out g • a = g • a
have conv_rhs : Quotient.out g • a = ⟦Quotient.out g⟧ • a
Tactic: conv_rhs => rw [← g.out_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
g : G
a : α
⊢ period g⁻¹ a = period g a
have simp : ∀ (n : ℕ), g⁻¹ ^ n • a = a ↔ g ^ n • a = a
Tactic: simp only [period_eq_minimalPeriod, Function.minimalPeriod_eq_minimalPeriod_iff,
    isPeriodicPt_smul_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
g : G
a : α
n : ℕ
⊢ g⁻¹ ^ n • a = a ↔ g ^ n • a = a
have rw : a = (g⁻¹ ^ n)⁻¹ • a ↔ g ^ n • a = a
Tactic: rw [smul_eq_iff_eq_inv_smul, eq_comm, ← zpow_natCast, inv_zpow, inv_inv, zpow_natCast]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
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
⊢ g⁻¹ ^ n • a = a ↔ g ^ n • a = a
have rw₁ : (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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
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
⊢ g⁻¹ ^ n • a = a ↔ g ^ n • a = a
have rw₂ : (HPow.hPow (β := ℤ) 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
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
⊢ g⁻¹ ^ n • a = a ↔ g ^ n • a = a
have rw₃ : (HPow.hPow (β := ℤ) 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
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
⊢ g⁻¹ ^ n • a = a ↔ g ^ n • a = a
have rw₄ : HPow.hPow (β := ℤ) 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
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
⊢ g⁻¹ ^ n • a = a ↔ g ^ n • a = a
have rw₅ : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
⊢ period m a ∣ orderOf m
have rw : m ^ orderOf m • a = a
Tactic: rw [← pow_smul_eq_iff_period_dvd, pow_orderOf_eq_one, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
rw : m ^ orderOf m • a = a
⊢ period m a ∣ orderOf m
have rw₁ : HSMul.hSMul.{u, v, v} (α := M) 1 a = a
Tactic: rw [← pow_smul_eq_iff_period_dvd, pow_orderOf_eq_one, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
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
⊢ period m a ∣ orderOf m
have rw₂ : a = a
Tactic: rw [← pow_smul_eq_iff_period_dvd, pow_orderOf_eq_one, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
⊢ period m a ∣ Monoid.exponent M
have rw : m ^ Monoid.exponent M • a = a
Tactic: rw [← pow_smul_eq_iff_period_dvd, Monoid.pow_exponent_eq_one, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
rw : m ^ Monoid.exponent M • a = a
⊢ period m a ∣ Monoid.exponent M
have rw₁ : HSMul.hSMul.{u, v, v} (α := M) 1 a = a
Tactic: rw [← pow_smul_eq_iff_period_dvd, Monoid.pow_exponent_eq_one, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
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
⊢ period m a ∣ Monoid.exponent M
have rw₂ : a = a
Tactic: rw [← pow_smul_eq_iff_period_dvd, Monoid.pow_exponent_eq_one, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Period (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
exp_pos : 0 < Monoid.exponent M
m : M
⊢ BddAbove (α := ℕ) (Set.range fun (a : α) ↦ period m a)
have h : Membership.mem (γ := Set ℕ) (upperBounds (Set.range fun (a : α) ↦ period m a)) (Monoid.exponent M)
Tactic: use Monoid.exponent M