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
rw :
  s ∩
      range (ι := ↥(ofStabilizer G a))
        (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x)) =
    s \ {a}
⊢ Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}

Tactic:
rw [Set.image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range
-- 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
simp : s ∩ {x : α | Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x} = s \ {a}
⊢ s ∩
      range (ι := ↥(ofStabilizer G a))
        (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x)) =
    s \ {a}

Tactic:
simp only [Subtype.range_coe_subtype]

Premises used: Subtype.range_coe_subtype
-- 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
rw : {x : α | Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x} ∩ s = {a}ᶜ ∩ s
⊢ s ∩ {x : α | Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x} = s \ {a}

Tactic:
rw [Set.diff_eq_compl_inter, Set.inter_comm]

Premises used: Set.diff_eq_compl_inter, Set.inter_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
⊢ {x : α | Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x} ∩ s = {a}ᶜ ∩ s

Tactic:
congr
-- 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
⊢ Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}

Tactic:
have hat : Subtype.val '' t = s \ {a} := by
      rw [Set.image_preimage_eq_inter_range]
      simp only [Subtype.range_coe_subtype]
      rw [Set.diff_eq_compl_inter, Set.inter_comm]
      congr
-- 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}
rw : s = insert a (s \ {a})
rw₁ : s = insert a s
rw₂ rw₃ : s = s
⊢ s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)

Tactic:
rw [hat, Set.insert_diff_singleton, Set.insert_eq_of_mem has]

Premises used: Set.insert_eq_of_mem, Set.insert_diff_singleton
-- 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}
⊢ s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)

Tactic:
have hat' : s = insert a (Subtype.val '' t) := by
      rw [hat, Set.insert_diff_singleton, Set.insert_eq_of_mem has]
-- 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)
⊢ Eq (α := Subgroup G) (fixingSubgroup G (α := α) (insert a ((fun (x : ↥(ofStabilizer G a)) ↦ (↑x : α)) '' t)))
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))

Tactic:
have hfs := SubMulAction.fixingSubgroup_of_insert a t
-- 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 (α := α) (insert a ((fun (x : ↥(ofStabilizer G a)) ↦ (↑x : α)) '' t)))
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
⊢ Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))

Tactic:
rw [← hat'] at hfs
-- 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))
⊢ Function.Injective (α := ↥(stabilizer G a)) (β := G)
    (⇑(Subgroup.subtype (stabilizer G a)) : (a : ↥(stabilizer G a)) → G)

Tactic:
simp only [Subgroup.coe_subtype, Subtype.coe_injective]

Premises used: Subgroup.coe_subtype, Subtype.coe_injective
-- 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))
succ :
  Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t ⊔ ⊥) *
        Subgroup.index (MonoidHom.range (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a))) *
      (Nat.card α - (k + 1))! =
    (Nat.card α)!
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!

Tactic:
rw [hfs, Subgroup.index_map,
      (MonoidHom.ker_eq_bot_iff (stabilizer G a).subtype).mpr
        (by simp only [Subgroup.coe_subtype, Subtype.coe_injective])]

Premises used: Iff.mpr, Subgroup.subtype, MonoidHom.ker_eq_bot_iff, MulAction.stabilizer, Subgroup.index_map
-- 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))
succ :
  Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) *
        Subgroup.index (stabilizer G a) *
      (Nat.card α - (k + 1))! =
    (Nat.card α)!
⊢ Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t ⊔ ⊥) *
        Subgroup.index (MonoidHom.range (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a))) *
      (Nat.card α - (k + 1))! =
    (Nat.card α)!

Tactic:
simp only [sup_bot_eq, Subgroup.range_subtype]

Premises used: sup_bot_eq, Subgroup.range_subtype
-- 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))
rw :
  (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
⊢ t.ncard = k

Tactic:
rw [← Nat.succ_inj, Nat.succ_eq_add_one, Nat.succ_eq_add_one, ← hs, hat', eq_comm]

Premises used: Nat.succ_inj, Nat.succ_eq_add_one, eq_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))
this :
  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 =
    (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
          t).ncard +
      1

Tactic:
Set.ncard_insert_of_notMem this ?_

Premises used: Set.ncard_insert_of_notMem
-- 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))
this :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
h :
  t.ncard =
    (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t).ncard
convert! :
  (Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t).Finite
⊢ (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:
convert! Set.ncard_insert_of_notMem this ?_

Premises used: Set.ncard_insert_of_notMem
-- 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))
this :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
h h₁ : t.ncard = t.ncard
⊢ t.ncard =
    (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t).ncard

Tactic:
rw [Set.ncard_image_of_injective _ Subtype.coe_injective]

Premises used: Subtype.coe_injective, Set.ncard_image_of_injective
-- 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))
this :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
⊢ (Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t).Finite

Tactic:
apply Set.toFinite

Premises used: Set.toFinite