internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = 1 + Set.ncard t
htcard : Set.ncard t = k
this :
  (Fintype.card α - 1 - Set.ncard t)! * Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) = (Fintype.card α - 1)!
⊢ Subgroup.index (stabilizer M a) * (Fintype.card α - 1)! = (Fintype.card α)!
Tactic:
rw [stabilizer_index_of_pretransitive M hGX a]
Proof state after:
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = 1 + Set.ncard t
htcard : Set.ncard t = k
this :
  (Fintype.card α - 1 - Set.ncard t)! * Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) = (Fintype.card α - 1)!
⊢ Nat.card α * (Fintype.card α - 1)! = (Fintype.card α)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = 1 + Set.ncard t
htcard : Set.ncard t = k
this :
  (Fintype.card α - 1 - Set.ncard t)! * Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) = (Fintype.card α - 1)!
⊢ Nat.card α * (Fintype.card α - 1)! = (Fintype.card α)!
Tactic:
rw [Nat.card_eq_fintype_card]
Proof state after:
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = 1 + Set.ncard t
htcard : Set.ncard t = k
this :
  (Fintype.card α - 1 - Set.ncard t)! * Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) = (Fintype.card α - 1)!
⊢ Fintype.card α * (Fintype.card α - 1)! = (Fintype.card α)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = 1 + Set.ncard t
htcard : Set.ncard t = k
this :
  (Fintype.card α - 1 - Set.ncard t)! * Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) = (Fintype.card α - 1)!
⊢ Fintype.card α * (Fintype.card α - 1)! = (Fintype.card α)!
Tactic:
apply Nat.mul_factorial_pred
Proof state after:
case hn
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = 1 + Set.ncard t
htcard : Set.ncard t = k
this :
  (Fintype.card α - 1 - Set.ncard t)! * Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) = (Fintype.card α - 1)!
⊢ 0 < Fintype.card α
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case hn
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = 1 + Set.ncard t
htcard : Set.ncard t = k
this :
  (Fintype.card α - 1 - Set.ncard t)! * Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) = (Fintype.card α - 1)!
⊢ 0 < Fintype.card α
Tactic:
rw [Fintype.card_pos_iff]
Proof state after:
case hn
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = 1 + Set.ncard t
htcard : Set.ncard t = k
this :
  (Fintype.card α - 1 - Set.ncard t)! * Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) = (Fintype.card α - 1)!
⊢ Nonempty α
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case hn
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = 1 + Set.ncard t
htcard : Set.ncard t = k
this :
  (Fintype.card α - 1 - Set.ncard t)! * Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) = (Fintype.card α - 1)!
⊢ Nonempty α
Tactic:
use a
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case succ.intro
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = 1 + Set.ncard t
htcard : Set.ncard t = k
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * (Fintype.card α - 1 - Set.ncard t)! = (Fintype.card α - 1)!
Tactic:
rw [add_comm] at hscard
Proof state after:
case succ.intro
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * (Fintype.card α - 1 - Set.ncard t)! = (Fintype.card α - 1)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case succ.intro
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * (Fintype.card α - 1 - Set.ncard t)! = (Fintype.card α - 1)!
Tactic:
have := Nat.sub_eq_of_eq_add hscard
Proof state after:
case succ.intro
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : Set.ncard s - 1 = Set.ncard t
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * (Fintype.card α - 1 - Set.ncard t)! = (Fintype.card α - 1)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case succ.intro
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : Set.ncard s - 1 = Set.ncard t
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * (Fintype.card α - 1 - Set.ncard t)! = (Fintype.card α - 1)!
Tactic:
simp only [hs, Nat.pred_succ] at this
Proof state after:
case succ.intro
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : succ k - 1 = Set.ncard t
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * (Fintype.card α - 1 - Set.ncard t)! = (Fintype.card α - 1)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case succ.intro
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : succ k - 1 = Set.ncard t
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * (Fintype.card α - 1 - Set.ncard t)! = (Fintype.card α - 1)!
Tactic:
convert hrec (stabilizer M a) (SubMulAction.ofStabilizer M a)
  ((stabilizer.isMultiplyPretransitive M α hGX).mp hmk) htcard
Proof state after:
case h.e'_2.h.e'_6.h.e'_1.h.e'_5
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : succ k - 1 = Set.ncard t
⊢ Fintype.card α - 1 = Fintype.card ↥(SubMulAction.ofStabilizer M a)

case h.e'_3.h.e'_1
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : succ k - 1 = Set.ncard t
⊢ Fintype.card α - 1 = Fintype.card ↥(SubMulAction.ofStabilizer M a)
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case h.e'_2.h.e'_6.h.e'_1.h.e'_5
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : succ k - 1 = Set.ncard t
⊢ Fintype.card α - 1 = Fintype.card ↥(SubMulAction.ofStabilizer M a)

case h.e'_3.h.e'_1
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : succ k - 1 = Set.ncard t
⊢ Fintype.card α - 1 = Fintype.card ↥(SubMulAction.ofStabilizer M a)
Tactic:
all_goals {
  apply symm
  convert Fintype.card_compl_set _
  exact setFintype {a}ᶜ }
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case h.e'_3.h.e'_1
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : succ k - 1 = Set.ncard t
⊢ Fintype.card α - 1 = Fintype.card ↥(SubMulAction.ofStabilizer M a)
Tactic:
apply symm
Proof state after:
case h.e'_3.h.e'_1.a
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : succ k - 1 = Set.ncard t
⊢ Fintype.card ↥(SubMulAction.ofStabilizer M a) = Fintype.card α - 1