awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
a : (↑s : Type u_2)
i : Fin s.ncard := ((Classical.choice Hs).symm : (a : (↑s : Type u_2)) → Fin s.ncard) a
⊢ g • (↑a : α) = (↑a : α)
have ha : (Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i = a
Tactic: have ha : (Classical.choice Hs) i = a := by simp [i]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
a : (↑s : Type u_2)
i : Fin s.ncard := ((Classical.choice Hs).symm : (a : (↑s : Type u_2)) → Fin s.ncard) a
ha : (Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i = a
⊢ g • (↑a : α) = (↑a : α)
have rw : HSMul.hSMul (β := α) g (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α) =
  (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α)
Tactic: rw [← ha]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
a : (↑s : Type u_2)
i : Fin s.ncard := ((Classical.choice Hs).symm : (a : (↑s : Type u_2)) → Fin s.ncard) a
ha : (Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i = a
⊢ HSMul.hSMul (β := α) g (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α) =
    (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α)
have nth_rewrite : HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
  (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α)
Tactic: nth_rewrite 1 [← ofFixingSubgroup.append_left x i]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
a : (↑s : Type u_2)
i : Fin s.ncard := ((Classical.choice Hs).symm : (a : (↑s : Type u_2)) → Fin s.ncard) a
ha : (Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i = a
⊢ HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α)
have rw : HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
  (append (s := s) y : (a : Fin (s.ncard + m)) → α) (castAdd m i)
Tactic: rw [← ofFixingSubgroup.append_left y i, ← hy, ← hg, smul_apply, ← hx]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
a : (↑s : Type u_2)
i : Fin s.ncard := ((Classical.choice Hs).symm : (a : (↑s : Type u_2)) → Fin s.ncard) a
ha : (Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i = a
rw :
  HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (append (s := s) y : (a : Fin (s.ncard + m)) → α) (castAdd m i)
rw₁ :
  HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (y' : (a : Fin (s.ncard + m)) → α) (castAdd m i)
⊢ HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α)
have rw₂ : HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
  (g • x' : (a : Fin (s.ncard + m)) → α) (castAdd m i)
Tactic: rw [← ofFixingSubgroup.append_left y i, ← hy, ← hg, smul_apply, ← hx]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
a : (↑s : Type u_2)
i : Fin s.ncard := ((Classical.choice Hs).symm : (a : (↑s : Type u_2)) → Fin s.ncard) a
ha : (Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i = a
rw :
  HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (append (s := s) y : (a : Fin (s.ncard + m)) → α) (castAdd m i)
rw₁ :
  HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (y' : (a : Fin (s.ncard + m)) → α) (castAdd m i)
rw₂ :
  HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (g • x' : (a : Fin (s.ncard + m)) → α) (castAdd m i)
⊢ HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α)
have rw₃ : HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
  HSMul.hSMul (β := α) g ((x' : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α)
Tactic: rw [← ofFixingSubgroup.append_left y i, ← hy, ← hg, smul_apply, ← hx]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α 0
s : Set α
hs : s.ncard = 0
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - 0)! = (Nat.card α)!
have hs₁ : s = ∅
Tactic: rw [Set.ncard_eq_zero] at hs
Cleared hypotheses: hs
-- 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
⊢ IsPretransitive G α
have rw : IsMultiplyPretransitive G α 1
Tactic: rw [← is_one_pretransitive_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
⊢ IsMultiplyPretransitive G α 1
have hmn : 1 ≤ k + 1
Tactic: apply isMultiplyPretransitive_of_le (n := k + 1)
-- 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
hmn : 1 ≤ k + 1
⊢ IsMultiplyPretransitive G α 1
have hα : k + 1 ≤ Nat.card α
Tactic: apply isMultiplyPretransitive_of_le (n := k + 1)
-- 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
⊢ 1 ≤ k + 1
have hmn : 0 ≤ k
Tactic: rw [Nat.succ_le_succ_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
⊢ k + 1 ≤ Nat.card α
have hα : s.ncard ≤ ncard.{u_2} (α := α) univ
Tactic: rw [← hs, ← Set.ncard_univ]
-- 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
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!
have hGX : IsPretransitive G α
Tactic: have hGX : IsPretransitive G α := by
      rw [← is_one_pretransitive_iff]
      apply isMultiplyPretransitive_of_le (n := k + 1)
      · rw [Nat.succ_le_succ_iff]; apply Nat.zero_le
      · rw [← hs, ← Set.ncard_univ]
        exact ncard_le_ncard s.subset_univ finite_univ
-- 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 α
⊢ s.Nonempty
have rw : 0 < k + 1
Tactic: rw [← Set.ncard_pos, hs]
-- 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 α
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!
have this : s.Nonempty
Tactic: have : s.Nonempty := by
      rw [← Set.ncard_pos, hs]
      exact succ_pos k
-- 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 α
this : s.Nonempty
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!
have succ : ∀ (a : α) (has : a ∈ s), Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!
Tactic: obtain ⟨a, has⟩ := this
Cleared hypotheses: 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
⊢ Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
have 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}
Tactic: rw [Set.image_preimage_eq_inter_range]
-- 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
⊢ 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}
have simp : s ∩ {x : α | Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x} = s \ {a}
Tactic: simp only [Subtype.range_coe_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
⊢ s ∩ {x : α | Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x} = s \ {a}
have rw : {x : α | Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x} ∩ s = {a}ᶜ ∩ s
Tactic: rw [Set.diff_eq_compl_inter, Set.inter_comm]
-- 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
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!
have hat : 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
-- 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}
⊢ s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
have rw : s = insert a (s \ {a})
Tactic: rw [hat, Set.insert_diff_singleton, Set.insert_eq_of_mem has]
-- 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}
rw : s = insert a (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)
have rw₁ : s = insert a s
Tactic: rw [hat, Set.insert_diff_singleton, Set.insert_eq_of_mem has]
-- 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}
rw : s = insert a (s \ {a})
rw₁ : s = insert a s
⊢ s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
have rw₂ : s = s
Tactic: rw [hat, Set.insert_diff_singleton, Set.insert_eq_of_mem has]
-- 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}
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!
have hat' : 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]
-- 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)
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!
have 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))
Tactic: have hfs := SubMulAction.fixingSubgroup_of_insert a t