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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
x : α
⊢ x ∈ s' ↔
    x ∈
      insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)
have h : x ∈ s' →
  x ∈
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
x : α
h :
  x ∈ s' →
    x ∈
      insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)
⊢ x ∈ s' ↔
    x ∈
      insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)
have h₁ : x ∈
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t) →
  x ∈ 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
x : α
hxs : x ∈ s'
⊢ x ∈
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
have pos : ∀ (hxa : x = a),
  x ∈
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
Tactic: by_cases hxa : x = a
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
x : α
hxs : x ∈ s'
pos :
  ∀ (hxa : x = a),
    x ∈
      insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)
⊢ x ∈
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
have neg : ∀ (hxa : ¬x = a),
  x ∈
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
Tactic: by_cases hxa : x = a
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s') ↥(ofFixingSubgroup M s')
have hst : s' =
  insert a
    (Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
      t)
Tactic: have hst : s' = insert a (Subtype.val '' t) := by
        ext x
        constructor
        · intro hxs
          by_cases hxa : x = a
          · simp [hxa]
          · exact Set.mem_insert_of_mem _
              ⟨⟨x, hxa⟩, by simp only [t, Set.mem_preimage]; exact hxs, rfl⟩
        · rw [Set.mem_insert_iff]
          rintro (⟨rfl⟩ | ⟨y, hy, rfl⟩)
          · simpa [s', ← hg]
          · simpa only using 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s') ↥(ofFixingSubgroup M s')
have mpr : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) t) ↥(ofFixingSubgroup (↥(stabilizer M a)) t)
Tactic: rw [hst, isPreprimitive_fixingSubgroup_insert_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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) t) ↥(ofFixingSubgroup (↥(stabilizer M a)) t)
have mpr : t.encard + 1 = (↑n : ℕ∞)
Tactic: apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup _ n
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
⊢ t.encard + 1 = (↑n : ℕ∞)
have mpr : Eq (α := ℕ∞) ((fun (x : ℕ∞) ↦ x + 1) (t.encard + 1)) ((fun (x : ℕ∞) ↦ x + 1) (↑n : ℕ∞))
Tactic: apply ENat.add_left_injective_of_ne_top ENat.one_ne_top
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
⊢ t.encard + 1 + 1 = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have mpr : t.encard + (↑1 : ℕ∞) + (↑1 : ℕ∞) = s.encard + 1
Tactic: rw [← Nat.cast_one, ← Nat.cast_add, ← hs]
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
⊢ t.encard + (↑1 : ℕ∞) + (↑1 : ℕ∞) = s.encard + 1
have apply : t.encard + (↑1 : ℕ∞) = s.encard
Tactic: apply congr_arg₂ _ _ rfl
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
⊢ t.encard + (↑1 : ℕ∞) = s.encard
have rw : t.encard + (↑1 : ℕ∞) =
  (insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)).encard
Tactic: rw [show s = g⁻¹ • s' from by simp [hs'],
        ← Set.image_smul, (MulAction.injective g⁻¹).encard_image, hst]
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
⊢ t.encard + (↑1 : ℕ∞) =
    (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)).encard
have rw : a ∉
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
    t
Tactic: rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, ENat.coe_one]
-- 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 α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) t)
have htt' : t =
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
    t'
Tactic: have htt' : t = Subtype.val ⁻¹' t' :=
      (Set.preimage_image_eq _ Subtype.coe_injective).symm
-- 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 α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) t)
have rw : IsPreprimitive.{u_1, u_2}
  ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
        t'))
  ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
        t'))
Tactic: rw [htt']
-- 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 α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
⊢ IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t'))
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t'))
have suffices : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (s ∪ t')) ↥(ofFixingSubgroup M (s ∪ t'))
Tactic: suffices IsPreprimitive (fixingSubgroup M (s ∪ t')) (ofFixingSubgroup M (s ∪ t')) by
      apply IsPreprimitive.of_surjective map_ofFixingSubgroupUnion_bijective.surjective
-- 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 α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (s ∪ t')) ↥(ofFixingSubgroup M (s ∪ t'))
have apply : (s ∪ t').encard + 1 = (↑n : ℕ∞)
Tactic: apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup _ n
-- 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 α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
⊢ (s ∪ t').encard + 1 = (↑n : ℕ∞)
have rw : s.encard + t'.encard + 1 = (↑n : ℕ∞)
Tactic: rw [Set.encard_union_eq _]
-- 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 α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
rw : s.encard + t'.encard + 1 = (↑n : ℕ∞)
⊢ (s ∪ t').encard + 1 = (↑n : ℕ∞)
have rw₁ : Disjoint s t'
Tactic: rw [Set.encard_union_eq _]
-- 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 α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
⊢ s.encard + t'.encard + 1 = (↑n : ℕ∞)
have rw : s.Finite
Tactic: rw [Subtype.coe_injective.encard_image, add_assoc, ht,
        ← hs, Nat.cast_add, Set.Finite.cast_ncard_eq]
-- 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 : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
⊢ IsMultiplyPreprimitive M α n
have inl : ∀ (hn : n = 0), IsMultiplyPreprimitive M α n
Tactic: rcases Nat.eq_zero_or_pos n with hn | hn
-- 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 : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
inl : ∀ (hn : n = 0), IsMultiplyPreprimitive M α n
⊢ IsMultiplyPreprimitive M α n
have inr : ∀ (hn : n > 0), IsMultiplyPreprimitive M α n
Tactic: rcases Nat.eq_zero_or_pos n with hn | hn
-- 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 : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n = 0
⊢ IsMultiplyPreprimitive M α n
have inl : IsMultiplyPreprimitive M α 0
Tactic: rw [hn]
-- 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 : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
⊢ IsMultiplyPreprimitive M α n
have inr : 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 : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
⊢ IsMultiplyPretransitive M α n ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑n : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have inr : 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 : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
inr : 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 inr₁ : ∀ {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 : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have inr : ∀ (m : ℕ) (hm : n = Nat.succ 0 + m), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Tactic: obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le hn
-- 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 : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
m : ℕ
hm : n = Nat.succ 0 + m
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have inr : IsMultiplyPretransitive.{u_1, u_2} (↥(fixingSubgroup M s)) (↥(ofFixingSubgroup M s)) 2
Tactic: apply isPreprimitive_of_is_two_pretransitive
-- 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 : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
m : ℕ
hm : n = Nat.succ 0 + m
⊢ s.encard = (↑m : ℕ∞)
have hs₁ : s.encard + 1 = (↑(m + 1) : ℕ∞)
Tactic: simp only [hm, Nat.succ_eq_add_one, zero_add, add_comm 1] at hs
Cleared hypotheses: hs