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
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
⊢ s.encard + 1 = (↑n : ℕ∞)
have rw₁ : s.encard + 1 = Set.encard.{u_4} (α := β) ((⇑f : (a : α) → β) '' s) + 1
Tactic: rw [← ht, ← hs', hf.injective.encard_image]
-- 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
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
⊢ s.encard + 1 = (↑n : ℕ∞)
have rw₂ : s.encard + 1 = s.encard + 1
Tactic: rw [← ht, ← hs', hf.injective.encard_image]
-- 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
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_3, u_4} ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)
have this : 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])
-- 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 : ℕ
⊢ IsMultiplyPreprimitive M α n ↔ IsMultiplyPreprimitive N β n
have refine : IsMultiplyPreprimitive N β n → IsMultiplyPreprimitive M α n
Tactic: refine ⟨IsMultiplyPreprimitive.of_bijective_map hf, ?_⟩
-- 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
⊢ IsMultiplyPreprimitive M α n
have rw : IsMultiplyPretransitive M α n ∧
  ∀ {s : Set α} (hs : s.encard + 1 = (↑n : ℕ∞)), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Tactic: rw [isMultiplyPreprimitive_iff]
-- 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
⊢ IsMultiplyPretransitive M α n ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑n : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have left : IsMultiplyPretransitive M α n
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
left : IsMultiplyPretransitive M α n
⊢ IsMultiplyPretransitive M α n ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑n : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have right : ∀ {s : Set α} (hs : s.encard + 1 = (↑n : ℕ∞)), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
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
x : ↥(fixingSubgroup M s)
g : M
hg : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) g
⊢ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) (φ g)
have simp : ∀ (hg : ∀ y ∈ s, g • y = y), ∀ y ∈ t, φ g • y = y
Tactic: simp only [mem_fixingSubgroup_iff] at hg ⊢
Cleared hypotheses: hg
-- 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
x : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
y : β
hy : y ∈ t
this : ∃ x ∈ s, y = (f : (a : α) → β) x
⊢ φ g • y = y
have obtain : ∀ (x : α) (hx : x ∈ s) (hy : Membership.mem (α := β) t ((f : (a : α) → β) x : β)),
  HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) x
Tactic: obtain ⟨x, hx, rfl⟩ := this
Cleared hypotheses: y, hy, 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
x_1 : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
x : α
hx : x ∈ s
hy : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
⊢ HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) x
have rwa : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (g • x) : β) ((f : (a : α) → β) x : β)
Tactic: rwa [← map_smulₛₗ, hg]
-- 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
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 : β)
⊢ HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) x
have rwa₁ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
Tactic: rwa [← map_smulₛₗ, hg]
-- 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
x : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
y : β
hy : y ∈ t
⊢ φ g • y = y
have suffices : ∃ x ∈ s, y = (f : (a : α) → β) x
Tactic: suffices ∃ x ∈ s, y = f x by
        obtain ⟨x, hx, rfl⟩ := this
        rwa [← map_smulₛₗ, hg]
-- 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
x : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
y : β
hy : y ∈ t
⊢ ∃ x ∈ s, y = (f : (a : α) → β) x
have obtain : ∀ (x : α) (hy : Membership.mem (α := β) t ((f : (a : α) → β) x : β)),
  ∃ x_1 ∈ s, Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x_1 : β)
Tactic: obtain ⟨x, rfl⟩ := hf.surjective y
Cleared hypotheses: y, hy
-- 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) ⋯
x : ↥(ofFixingSubgroup M s)
⊢ Membership.mem (α := β) (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t)
    ((f : (a : α) → β) (↑x : α) : β)
have simp : (↑x : α) ∉ s
Tactic: simp only [mem_ofFixingSubgroup_iff, Set.mem_image, hf.injective.eq_iff, exists_eq_right, t]
-- 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' := ⋯ }
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have right : IsPreprimitive.{u_3, u_4} ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)
Tactic: rw [isPreprimitive_congr (f := g)]
-- 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 : IsPreprimitive.{u_3, u_4} ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have right₁ : Function.Surjective ψ
Tactic: rw [isPreprimitive_congr (f := g)]
-- 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 : IsPreprimitive.{u_3, u_4} ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)
right₁ : Function.Surjective ψ
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have right₂ : Function.Bijective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
  (⇑g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
Tactic: rw [isPreprimitive_congr (f := g)]
-- 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' := ⋯ }
⊢ IsPreprimitive.{u_3, u_4} ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)
have right : t.encard + 1 = (↑n : ℕ∞)
Tactic: apply H.isPreprimitive_ofFixingSubgroup
-- 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 : N
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 : ∀ (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
Tactic: obtain ⟨k, rfl⟩ := hφ k
Cleared hypotheses: k, 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 : Membership.mem (γ := Subgroup N) (fixingSubgroup N t) (φ k)
this : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
⊢ ∃ (a : ↥(fixingSubgroup M s)),
    ψ a = Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ k) hk
have w : ↥(fixingSubgroup M s)
Tactic: 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)
this : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
w : ↥(fixingSubgroup M s)
⊢ ∃ (a : ↥(fixingSubgroup M s)),
    ψ a = Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ k) hk
have h : ψ (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k this) =
  Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ k) hk
Tactic: use ⟨k, this⟩