internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case succ
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 α
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Tactic:
have : s.Nonempty := by
  rw [← Set.ncard_pos, hs]
  exact succ_pos k
Proof state after:
case succ
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 α
this : Set.Nonempty s
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case succ
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 α
this : Set.Nonempty s
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Tactic:
obtain ⟨a, has⟩ := 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
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
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
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Tactic:
let t : Set (SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
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
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
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
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
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
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}
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
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}
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Tactic:
have hat' : s = insert a (Subtype.val '' t) := by
  rw [hat, Set.insert_diff_singleton, Set.insert_eq_of_mem has]
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)
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
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)
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Tactic:
have hfs : fixingSubgroup M s = ?_ := by
  rw [hat']
  exact fixingSubgroup_of_insert M a t
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)
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
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)
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Tactic:
rw [hfs]
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)
⊢ Subgroup.index (Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)) *
      (Fintype.card α - Set.ncard s)! =
    (Fintype.card α)!
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)
⊢ Subgroup.index (Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)) *
      (Fintype.card α - Set.ncard s)! =
    (Fintype.card α)!
Tactic:
rw [Subgroup.index_map]
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)
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t ⊔ MonoidHom.ker (Subgroup.subtype (stabilizer M a))) *
        Subgroup.index (MonoidHom.range (Subgroup.subtype (stabilizer M a))) *
      (Fintype.card α - Set.ncard s)! =
    (Fintype.card α)!
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)
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t ⊔ MonoidHom.ker (Subgroup.subtype (stabilizer M a))) *
        Subgroup.index (MonoidHom.range (Subgroup.subtype (stabilizer M a))) *
      (Fintype.card α - Set.ncard s)! =
    (Fintype.card α)!
Tactic:
rw [(MonoidHom.ker_eq_bot_iff (stabilizer M a).subtype).mpr
    (by simp only [Subgroup.coeSubtype, Subtype.coe_injective])]
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)
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t ⊔ ⊥) *
        Subgroup.index (MonoidHom.range (Subgroup.subtype (stabilizer M a))) *
      (Fintype.card α - Set.ncard s)! =
    (Fintype.card α)!
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)
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t ⊔ ⊥) *
        Subgroup.index (MonoidHom.range (Subgroup.subtype (stabilizer M a))) *
      (Fintype.card α - Set.ncard s)! =
    (Fintype.card α)!
Tactic:
simp only [sup_bot_eq, Subgroup.subtype_range]
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)
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * Subgroup.index (stabilizer M a) *
      (Fintype.card α - Set.ncard s)! =
    (Fintype.card α)!
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)
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * Subgroup.index (stabilizer M a) *
      (Fintype.card α - Set.ncard s)! =
    (Fintype.card α)!
Tactic:
have hscard : s.ncard = 1 + t.ncard := by
  rw [hat']
  suffices ¬ a ∈ (Subtype.val '' t) by
    rw [add_comm]
    convert Set.ncard_insert_of_not_mem this ?_
    rw [Set.ncard_image_of_injective _ Subtype.coe_injective]
    apply Set.toFinite
  intro h
  obtain ⟨⟨b, hb⟩, _, hb'⟩ := h
  apply hb
  simp only [Set.mem_singleton_iff]
  rw [← hb']
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 = 1 + Set.ncard t
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * Subgroup.index (stabilizer M a) *
      (Fintype.card α - Set.ncard s)! =
    (Fintype.card α)!
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
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * Subgroup.index (stabilizer M a) *
      (Fintype.card α - Set.ncard s)! =
    (Fintype.card α)!
Tactic:
have htcard : t.ncard = k := by
  rw [← Nat.succ_inj', ← hs, hscard, add_comm]
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 = 1 + Set.ncard t
htcard : Set.ncard t = k
⊢ Subgroup.index (fixingSubgroup (↥(stabilizer M a)) t) * Subgroup.index (stabilizer M a) *
      (Fintype.card α - Set.ncard s)! =
    (Fintype.card α)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case zero

⊢ ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α zero →
      ∀ {s : Set α},
        Set.ncard s = zero → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Tactic:
intro M α _ _ _ _ s hs
Proof state after:
case zero
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk✝ : IsMultiplyPretransitive M α zero
s : Set α
hs : Set.ncard s = zero
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case zero
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk✝ : IsMultiplyPretransitive M α zero
s : Set α
hs : Set.ncard s = zero
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Tactic:
simp only [hs, zero_eq, ge_iff_le, nonpos_iff_eq_zero, tsub_zero, ne_eq]
Proof state after:
case zero
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk✝ : IsMultiplyPretransitive M α zero
s : Set α
hs : Set.ncard s = zero
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α)! = (Fintype.card α)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case zero
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk✝ : IsMultiplyPretransitive M α zero
s : Set α
hs : Set.ncard s = zero
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α)! = (Fintype.card α)!
Tactic:
rw [Set.ncard_eq_zero] at hs
Proof state after:
case zero
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk✝ : IsMultiplyPretransitive M α zero
s : Set α
hs : s = ∅
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α)! = (Fintype.card α)!