awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
suffices :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
⊢ (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
          t)).ncard =
    t.ncard + 1

Tactic:
suffices ¬ a ∈ (Subtype.val '' t) by
        convert! Set.ncard_insert_of_notMem this ?_
        · rw [Set.ncard_image_of_injective _ Subtype.coe_injective]
        apply Set.toFinite
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
h :
  a ∈
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
obtain :
  ∀ (b : α) (hb : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) b),
    Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) b hb ∈
        t →
      ∀
        (hb' :
          (↑(Subtype.mk (p := fun (x : α) ↦
                  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) b hb) :
              α) =
            a),
        False
⊢ False

Tactic:
obtain ⟨⟨b, hb⟩, _, hb'⟩ := h
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
b : α
hb : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) b
left :
  Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) b hb ∈
    t
hb' :
  (↑(Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) b hb) :
      α) =
    a
apply : Membership.mem (γ := Set α) {a} b
⊢ False

Tactic:
apply hb
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
b : α
hb : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) b
left :
  Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) b hb ∈
    t
hb' :
  (↑(Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) b hb) :
      α) =
    a
⊢ Membership.mem (γ := Set α) {a} b

Tactic:
simp only [← hb', Set.mem_singleton_iff]

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
⊢ t.ncard = k

Tactic:
have htcard : t.ncard = k := by
      rw [← Nat.succ_inj, Nat.succ_eq_add_one, Nat.succ_eq_add_one, ← hs, hat', eq_comm]
      suffices ¬ a ∈ (Subtype.val '' t) by
        convert! Set.ncard_insert_of_notMem this ?_
        · rw [Set.ncard_image_of_injective _ Subtype.coe_injective]
        apply Set.toFinite
      intro h
      obtain ⟨⟨b, hb⟩, _, hb'⟩ := h
      apply hb
      simp only [← hb', Set.mem_singleton_iff]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
htcard : t.ncard = k
this :
  Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) * (Nat.card α - 1 - k)! =
    (Nat.card α - 1)!
rw : Nat.card α * (Nat.card α - 1)! = (Nat.card α)!
⊢ Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) *
        Subgroup.index (stabilizer G a) *
      (Nat.card α - (k + 1))! =
    (Nat.card α)!

Tactic:
rw [add_comm k, Nat.mul_right_comm, ← Nat.sub_sub, this, mul_comm,
        index_stabilizer_of_transitive G a]

Premises used: Nat.mul_right_comm, MulAction.index_stabilizer_of_transitive, Nat.sub_sub, add_comm, mul_comm
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
htcard : t.ncard = k
this :
  Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) * (Nat.card α - 1 - k)! =
    (Nat.card α - 1)!
⊢ Nat.card α * (Nat.card α - 1)! = (Nat.card α)!

Tactic:
Nat.mul_factorial_pred (card_ne_zero.mpr ⟨⟨a⟩, inferInstance⟩)

Premises used: Iff.mpr, inferInstance, Nonempty.intro, And.intro, Nat.card_ne_zero, Nat.mul_factorial_pred
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
htcard : t.ncard = k
this :
  Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) * (Nat.card α - 1 - k)! =
    (Nat.card α - 1)!
⊢ Nat.card α * (Nat.card α - 1)! = (Nat.card α)!

Tactic:
exact Nat.mul_factorial_pred (card_ne_zero.mpr ⟨⟨a⟩, inferInstance⟩)

Premises used: Iff.mpr, inferInstance, Nonempty.intro, And.intro, Nat.card_ne_zero, Nat.mul_factorial_pred
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
htcard : t.ncard = k
succ :
  Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) * (Nat.card α - 1 - k)! =
    (Nat.card α - 1)!
⊢ Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) *
        Subgroup.index (stabilizer G a) *
      (Nat.card α - (k + 1))! =
    (Nat.card α)!

Tactic:
suffices (fixingSubgroup (stabilizer G a) t).index *
      (Nat.card α - 1 - k).factorial =
        (Nat.card α - 1).factorial by
      rw [add_comm k, Nat.mul_right_comm, ← Nat.sub_sub, this, mul_comm,
        index_stabilizer_of_transitive G a]
      exact Nat.mul_factorial_pred (card_ne_zero.mpr ⟨⟨a⟩, inferInstance⟩)
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
htcard : t.ncard = k
⊢ Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) *
      (Nat.card.{u_2} ↥(ofStabilizer G a) - k)! =
    (Nat.card.{u_2} ↥(ofStabilizer G a))!

Tactic:
hrec (ofStabilizer.isMultiplyPretransitive.mp Hk) htcard

Premises used: SubMulAction.ofStabilizer.isMultiplyPretransitive, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
htcard : t.ncard = k
h h₁ : Nat.card α - 1 = Nat.card.{u_2} ↥(ofStabilizer G a)
⊢ Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) * (Nat.card α - 1 - k)! =
    (Nat.card α - 1)!

Tactic:
convert! hrec (ofStabilizer.isMultiplyPretransitive.mp Hk) htcard

Premises used: SubMulAction.ofStabilizer.isMultiplyPretransitive, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
htcard : t.ncard = k
h h₁ : Nat.card α - 1 = Nat.card α - 1
⊢ Nat.card α - 1 = Nat.card.{u_2} ↥(ofStabilizer G a)

Tactic:
rw [nat_card_ofStabilizer_eq G a]

Premises used: SubMulAction.nat_card_ofStabilizer_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
htcard : t.ncard = k
h h₁ : Nat.card α - 1 = Nat.card α - 1
⊢ Nat.card α - 1 = Nat.card.{u_2} ↥(ofStabilizer G a)

Tactic:
{ rw [nat_card_ofStabilizer_eq G a] }

Premises used: SubMulAction.nat_card_ofStabilizer_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
s : Set α
hMk : IsMultiplyPretransitive G α s.ncard
apply :
  Subgroup.index (fixingSubgroup G s) * (Nat.card α - s.ncard)! =
    (Nat.card α).choose s.ncard * s.ncard ! * (Nat.card α - s.ncard)!
apply₁ : ℕ
⊢ Subgroup.index (fixingSubgroup G s) = (Nat.card α).choose s.ncard * s.ncard !

Tactic:
apply Nat.eq_of_mul_eq_mul_right (Nat.factorial_pos _)

Premises used: Nat.eq_of_mul_eq_mul_right, Nat.factorial_pos
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
s : Set α
hMk : IsMultiplyPretransitive G α s.ncard
rw : s.ncard ≤ ncard.{u_2} (α := α) univ
⊢ s.ncard ≤ Nat.card α

Tactic:
rw [← ncard_univ]

Premises used: Set.ncard_univ
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
s : Set α
hMk : IsMultiplyPretransitive G α s.ncard
⊢ s.ncard ≤ ncard.{u_2} (α := α) univ

Tactic:
ncard_le_ncard (subset_univ s)

Premises used: Set.subset_univ, Set.ncard_le_ncard
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
s : Set α
hMk : IsMultiplyPretransitive G α s.ncard
⊢ s.ncard ≤ ncard.{u_2} (α := α) univ

Tactic:
exact ncard_le_ncard (subset_univ s)

Premises used: Set.subset_univ, Set.ncard_le_ncard
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
ι : Type u_2
inst : Finite ι
β : Type u_3
x y : ι ↪ β
obtain :
  ∀ (σ : Perm β)
    (hσ : ∀ (a : ι), Eq (α := β) ((σ : (a : β) → β) ((x : (a : ι) → β) a : β) : β) ((y : (a : ι) → β) a : β)),
    ∃ (σ : Perm β), σ • x = y
⊢ ∃ (σ : Perm β), σ • x = y

Tactic:
obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair x y x.injective y.injective

Premises used: Equiv.Perm.exists_extending_pair, Function.Embedding.injective, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
ι : Type u_2
inst : Finite ι
β : Type u_3
x y : ι ↪ β
σ : Perm β
hσ : ∀ (a : ι), Eq (α := β) ((σ : (a : β) → β) ((x : (a : ι) → β) a : β) : β) ((y : (a : ι) → β) a : β)
i : ι
⊢ Eq.{u_3 + 1} (α := β) ((σ • x : (a : ι) → β) i : β) ((y : (a : ι) → β) i : β)

Tactic:
simp [Function.Embedding.smul_apply, hσ]

Premises used: Function.Embedding.smul_apply
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
ι : Type u_2
inst : Finite ι
β : Type u_3
x y : ι ↪ β
σ : Perm β
hσ : ∀ (a : ι), Eq (α := β) ((σ : (a : β) → β) ((x : (a : ι) → β) a : β) : β) ((y : (a : ι) → β) a : β)
⊢ ∃ (σ : Perm β), σ • x = y

Tactic:
exact ⟨σ, Function.Embedding.ext fun i => by simp [Function.Embedding.smul_apply, hσ]⟩