awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
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))
this : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
⊢ 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

Tactic:
simpa [← Subtype.coe_inj, hf.injective.eq_iff] using this

Premises used: Function.Injective.eq_iff, Subtype.coe_inj, Function.Bijective.injective
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
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))
right : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
⊢ 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

Tactic:
suffices f x = f y by
          simpa [← Subtype.coe_inj, hf.injective.eq_iff] using this
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
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))
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
simpa only [g, ← Subtype.coe_inj] using h

Premises used: Subtype.coe_inj
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
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
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))
⊢ ∃ (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

Tactic:
obtain ⟨y, rfl⟩ := hf.surjective x

Premises used: Function.Bijective.surjective, rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
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 : β)
this : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) 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:
⟨⟨y, this⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
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 : β)
this : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) 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:
exact ⟨⟨y, this⟩, rfl⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
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 : β)
right : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) 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:
suffices y ∈ ofFixingSubgroup M s by
          exact ⟨⟨y, this⟩, rfl⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
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 : β)
⊢ ∀ 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 ⊢

Premises used: Set.mem_image, not_exists, SubMulAction.mem_ofFixingSubgroup_iff, not_and
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
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 : ∀ x ∈ s, ¬Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
⊢ y ∉ s

Tactic:
fun hy ↦ hx y hy rfl

Premises used: Not, rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
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 : ∀ x ∈ s, ¬Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
⊢ y ∉ s

Tactic:
exact fun hy ↦ hx y hy rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.OfQuotient
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
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))
⊢ 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

Tactic:
funext a
-- Module: Mathlib.GroupTheory.GroupAction.OfQuotient
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)
h :
  Eq.{u_2 + 1} (α := A) (↑((toEndHom : (a : G) → Function.End (↑(fixedPoints (↥H) A) : Type u_2)) g a) : A) (↑(1 a) : A)
⊢ 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:
ext
-- Module: Mathlib.GroupTheory.GroupAction.OfQuotient
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} (α := A) (↑((toEndHom : (a : G) → Function.End (↑(fixedPoints (↥H) A) : Type u_2)) g a) : A) (↑(1 a) : A)

Tactic:
a.2 ⟨g, hg⟩

Premises used: Subtype.mk, Subtype.property
-- Module: Mathlib.GroupTheory.GroupAction.OfQuotient
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} (α := A) (↑((toEndHom : (a : G) → Function.End (↑(fixedPoints (↥H) A) : Type u_2)) g a) : A) (↑(1 a) : A)

Tactic:
exact a.2 ⟨g, hg⟩

Premises used: Subtype.mk, Subtype.property
-- Module: Mathlib.GroupTheory.GroupAction.OfQuotient
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
a : (↑(fixedPoints.{u_1, u_2} (↥H) A) : Type u_2)
⊢ HSMul.hSMul (α := G ⧸ H) (↑g : G ⧸ H) a = g • a

Tactic:
rfl

Premises used: Quotient.liftOn', SMul.comp.smul, Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.GroupAction.OfQuotient
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)
rw : ⟦Quotient.out g⟧ • a
| g • a

Tactic:
rw [← g.out_eq]

Premises used: Quotient.out_eq
-- Module: Mathlib.GroupTheory.GroupAction.OfQuotient
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)
conv_rhs : Quotient.out g • a = ⟦Quotient.out g⟧ • a
⊢ Quotient.out g • a = g • a

Tactic:
conv_rhs => rw [← g.out_eq]

Premises used: Quotient.out_eq
-- Module: Mathlib.GroupTheory.GroupAction.OfQuotient
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 = ⟦Quotient.out g⟧ • a

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
n : ℕ
period_pos : 0 < period m a
moved : ∀ (k : ℕ), 0 < k → k < n → m ^ k • a ≠ a
⊢ n ≤ period m a

Tactic:
le_of_not_gt fun period_lt_n =>
    moved _ period_pos period_lt_n <| pow_period_smul m a

Premises used: le_of_not_gt, MulAction.pow_period_smul, MulAction.period
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
n : ℕ
n_pos : 0 < n
fixed : m ^ n • a = a
⊢ period m a ≤ n

Tactic:
(isPeriodicPt_smul_iff.mpr fixed).minimalPeriod_le n_pos

Premises used: Iff.mpr, Function.IsPeriodicPt.minimalPeriod_le, MulAction.period, MulAction.isPeriodicPt_smul_iff
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
n : ℕ
n_pos : 0 < n
fixed : m ^ n • a = a
⊢ 0 < period m a

Tactic:
(isPeriodicPt_smul_iff.mpr fixed).minimalPeriod_pos n_pos

Premises used: Iff.mpr, MulAction.period, MulAction.isPeriodicPt_smul_iff, Function.IsPeriodicPt.minimalPeriod_pos
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
fixed : m • a = a
⊢ HPow.hPow (β := ℕ) m 1 • a = a

Tactic:
simpa
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
n : ℕ
n_pos : 0 < n
n_lt_period : n < period m a
⊢ m ^ n • a ≠ a

Tactic:
fun a_fixed =>
  not_le_of_gt n_lt_period <| period_le_of_fixed n_pos a_fixed

Premises used: MulAction.period_le_of_fixed, not_le_of_gt, Not
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
a : α
⊢ period.{u, v} (M := M) 1 a = 1

Tactic:
period_eq_one_iff.mpr (one_smul M a)

Premises used: Iff.mpr, one_smul, MulAction.period_eq_one_iff
-- Module: Mathlib.GroupTheory.GroupAction.Period
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
g : G
a : α
simp : ∀ (n : ℕ), g⁻¹ ^ n • a = a ↔ g ^ n • a = a
⊢ period g⁻¹ a = period g a

Tactic:
simp only [period_eq_minimalPeriod, Function.minimalPeriod_eq_minimalPeriod_iff,
    isPeriodicPt_smul_iff]

Premises used: Function.minimalPeriod_eq_minimalPeriod_iff, MulAction.isPeriodicPt_smul_iff, MulAction.period_eq_minimalPeriod