awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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))
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!
have hfs₁ : 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
Cleared hypotheses: hfs
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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))
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!
have 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 α)!
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])]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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))
⊢ 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 α)!
have 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 α)!
Tactic: simp only [sup_bot_eq, Subgroup.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
have 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
Tactic: rw [← Nat.succ_inj, Nat.succ_eq_add_one, Nat.succ_eq_add_one, ← hs, hat', eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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 =
    t.ncard + 1
have h : t.ncard =
  (Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t).ncard
Tactic: convert! Set.ncard_insert_of_notMem this ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ (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
have convert! : (Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
    t).Finite
Tactic: convert! Set.ncard_insert_of_notMem this ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ t.ncard =
    (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t).ncard
have h : t.ncard = t.ncard
Tactic: rw [Set.ncard_image_of_injective _ Subtype.coe_injective]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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))
⊢ (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
have suffices : a ∉
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
    t
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
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ False
have 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
Tactic: obtain ⟨⟨b, hb⟩, _, hb'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ False
have apply : Membership.mem (γ := Set α) {a} b
Tactic: apply hb
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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))
⊢ Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) *
        Subgroup.index (stabilizer G a) *
      (Nat.card α - (k + 1))! =
    (Nat.card α)!
have htcard : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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)!
⊢ Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) *
        Subgroup.index (stabilizer G a) *
      (Nat.card α - (k + 1))! =
    (Nat.card α)!
have rw : Nat.card α * (Nat.card α - 1)! = (Nat.card α)!
Tactic: rw [add_comm k, Nat.mul_right_comm, ← Nat.sub_sub, this, mul_comm,
        index_stabilizer_of_transitive G a]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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) *
        Subgroup.index (stabilizer G a) *
      (Nat.card α - (k + 1))! =
    (Nat.card α)!
have succ : Subgroup.index.{u_1} (G := ↥(stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t) * (Nat.card α - 1 - k)! =
  (Nat.card α - 1)!
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⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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 α - 1 - k)! =
    (Nat.card α - 1)!
have h : Nat.card α - 1 = Nat.card.{u_2} ↥(ofStabilizer G a)
Tactic: convert! hrec (ofStabilizer.isMultiplyPretransitive.mp Hk) htcard