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
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x with
      | ⟨x, hx⟩ =>
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
          ⋯,
    map_smul' := ⋯ }
y : β
hy : Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) y
x : α
hx : (f : (a : α) → β) x = y
h₁ :
  (f' : (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 ⋯) =
    Subtype.mk (p := fun (x : β) ↦
      Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) y hy
w : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
⊢ ∃ (a : ↥(ofFixingSubgroup M s)),
    (f' : (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) y hy

Tactic:
use ⟨x, ?_⟩
-- 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
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x with
      | ⟨x, hx⟩ =>
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
          ⋯,
    map_smul' := ⋯ }
y : β
hy : Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) y
x : α
hx : (f : (a : α) → β) x = y
⊢ (f' : (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 ⋯) =
    Subtype.mk (p := fun (x : β) ↦
      Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) y hy

Tactic:
simpa only [f', ← Subtype.coe_inj] using hx

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
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h_1 : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x with
      | ⟨x, hx⟩ =>
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
          ⋯,
    map_smul' := ⋯ }
y : β
hy : Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) y
x : α
hx : (f : (a : α) → β) x = y
h : x ∈ s
w : y ∈ t
⊢ False

Tactic:
apply hy
-- 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
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h_1 : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x with
      | ⟨x, hx⟩ =>
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
          ⋯,
    map_smul' := ⋯ }
y : β
hy : Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) y
x : α
hx : (f : (a : α) → β) x = y
h : x ∈ s
w : Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y
⊢ y ∈ t

Tactic:
rw [← hs']
-- 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
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h_1 : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x with
      | ⟨x, hx⟩ =>
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
          ⋯,
    map_smul' := ⋯ }
y : β
hy : Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) y
x : α
hx : (f : (a : α) → β) x = y
h : x ∈ s
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y

Tactic:
⟨x, h, hx⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- 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
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h_1 : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x with
      | ⟨x, hx⟩ =>
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
          ⋯,
    map_smul' := ⋯ }
y : β
hy : Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) y
x : α
hx : (f : (a : α) → β) x = y
h : x ∈ s
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y

Tactic:
exact ⟨x, h, hx⟩
-- 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
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x with
      | ⟨x, hx⟩ =>
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
          ⋯,
    map_smul' := ⋯ }
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑f' : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))

Tactic:
have hf' : Function.Surjective f' := by
      rintro ⟨y, hy⟩
      obtain ⟨x, hx⟩ := hf.right y
      use ⟨x, ?_⟩
      · simpa only [f', ← Subtype.coe_inj] using hx
      · intro h
        apply hy
        rw [← hs']
        exact ⟨x, h, hx⟩
-- 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
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x with
      | ⟨x, hx⟩ =>
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
          ⋯,
    map_smul' := ⋯ }
hf' :
  Function.Surjective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑f' : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
rw : s.encard + 1 = t.encard + 1
rw₁ : s.encard + 1 = Set.encard.{u_4} (α := β) ((⇑f : (a : α) → β) '' s) + 1
rw₂ rw₃ : s.encard + 1 = s.encard + 1
⊢ s.encard + 1 = (↑n : ℕ∞)

Tactic:
rw [← ht, ← hs', hf.injective.encard_image]

Premises used: Function.Bijective.injective, Function.Injective.encard_image
-- 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
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x with
      | ⟨x, hx⟩ =>
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
          ⋯,
    map_smul' := ⋯ }
hf' :
  Function.Surjective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑f' : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
have : IsPreprimitive (fixingSubgroup M s) (ofFixingSubgroup M s) :=
      IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup _ n
        (by rw [← ht, ← hs', hf.injective.encard_image])
-- 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
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x with
      | ⟨x, hx⟩ =>
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
          ⋯,
    map_smul' := ⋯ }
hf' :
  Function.Surjective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑f' : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
this : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsPreprimitive.{u_3, u_4} ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)

Tactic:
IsPreprimitive.of_surjective (f := f') (φ := φ') hf'

Premises used: MulAction.IsPreprimitive.of_surjective, Set.Mem
-- 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
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x with
      | ⟨x, hx⟩ =>
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
          ⋯,
    map_smul' := ⋯ }
hf' :
  Function.Surjective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑f' : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
this : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsPreprimitive.{u_3, u_4} ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)

Tactic:
exact IsPreprimitive.of_surjective (f := f') (φ := φ') hf'

Premises used: MulAction.IsPreprimitive.of_surjective
-- 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 : ℕ
⊢ IsMultiplyPreprimitive M α n ↔ IsMultiplyPreprimitive N β n

Tactic:
⟨IsMultiplyPreprimitive.of_bijective_map hf, ?_⟩

Premises used: MulAction.IsMultiplyPreprimitive.of_bijective_map, Iff.intro
-- 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 : ℕ
refine : IsMultiplyPreprimitive N β n → IsMultiplyPreprimitive M α n
⊢ IsMultiplyPreprimitive M α n ↔ IsMultiplyPreprimitive N β n

Tactic:
refine ⟨IsMultiplyPreprimitive.of_bijective_map hf, ?_⟩
-- 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
rw :
  IsMultiplyPretransitive M α n ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑n : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsMultiplyPreprimitive M α n

Tactic:
rw [isMultiplyPreprimitive_iff]

Premises used: MulAction.isMultiplyPreprimitive_iff
-- 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
left : IsMultiplyPretransitive M α n
right :
  ∀ {s : Set α} (hs : s.encard + 1 = (↑n : ℕ∞)), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsMultiplyPretransitive M α n ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑n : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
constructor
-- 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
⊢ IsMultiplyPretransitive M α n

Tactic:
(IsPretransitive.of_embedding_congr hφ hf).mpr H.isMultiplyPretransitive

Premises used: Iff.mpr, MulAction.IsMultiplyPreprimitive.isMultiplyPretransitive, MulAction.IsPretransitive.of_embedding_congr
-- 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
⊢ IsMultiplyPretransitive M α n

Tactic:
exact (IsPretransitive.of_embedding_congr hφ hf).mpr H.isMultiplyPretransitive

Premises used: Iff.mpr, MulAction.IsMultiplyPreprimitive.isMultiplyPretransitive, MulAction.IsPretransitive.of_embedding_congr
-- 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
x : ↥(fixingSubgroup M s)
g : M
hg : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) g
simp : ∀ (hg : ∀ y ∈ s, g • y = y), ∀ y ∈ t, φ g • y = y
⊢ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) (φ g)

Tactic:
simp only [mem_fixingSubgroup_iff] at hg ⊢

Premises used: mem_fixingSubgroup_iff
-- 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
x : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
y : β
hy : y ∈ t
this : ∃ x ∈ s, y = (f : (a : α) → β) x
obtain :
  ∀ (x : α) (hx : x ∈ s) (hy : Membership.mem (α := β) t ((f : (a : α) → β) x : β)),
    HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) x
⊢ φ g • y = y

Tactic:
obtain ⟨x, hx, rfl⟩ := this

Premises used: 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
x_1 : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
x : α
hx : x ∈ s
hy : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
rwa : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (g • x) : β) ((f : (a : α) → β) x : β)
rwa₁ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
a : x ∈ s
rwa₂ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
a₁ a₂ a₃ : x ∈ s
⊢ HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) x

Tactic:
rwa [← map_smulₛₗ, hg]

Premises used: MulActionSemiHomClass.map_smulₛₗ