internlm/Lean-Github huggingface dataset:
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 : s = ∅
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α)! = (Fintype.card α)!
Tactic:
simp only [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 ∅) * (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 : s = ∅
⊢ Subgroup.index (fixingSubgroup M ∅) * (Fintype.card α)! = (Fintype.card α)!
Tactic:
suffices fixingSubgroup M ∅ = ⊤ by
  rw [this, Subgroup.index_top, one_mul]
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 = ∅
⊢ fixingSubgroup M ∅ = ⊤
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 : s = ∅
⊢ fixingSubgroup M ∅ = ⊤
Tactic:
exact GaloisConnection.l_bot (fixingSubgroup_fixedPoints_gc M α)
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk✝ : IsMultiplyPretransitive M α zero
s : Set α
hs : s = ∅
this : fixingSubgroup M ∅ = ⊤
⊢ Subgroup.index (fixingSubgroup M ∅) * (Fintype.card α)! = (Fintype.card α)!
Tactic:
rw [this, Subgroup.index_top, one_mul]
Proof state after:
no goals
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
⊢ IsPretransitive M α
Tactic:
rw [isPretransitive_iff_is_one_pretransitive]
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
⊢ IsMultiplyPretransitive M α 1
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
⊢ IsMultiplyPretransitive M α 1
Tactic:
apply isMultiplyPretransitive_of_higher M α hmk
Proof state after:
case hmn
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
⊢ 1 ≤ succ k

case hα
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
⊢ ↑(succ k) ≤ PartENat.card α
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case hmn
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
⊢ 1 ≤ succ k
Tactic:
rw [Nat.succ_le_succ_iff]
Proof state after:
case hmn
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
⊢ 0 ≤ k
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case hmn
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
⊢ 0 ≤ k
Tactic:
apply Nat.zero_le
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case hα
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
⊢ ↑(succ k) ≤ PartENat.card α
Tactic:
rw [← hs]
Proof state after:
case hα
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
⊢ ↑(Set.ncard s) ≤ PartENat.card α
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case hα
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
⊢ ↑(Set.ncard s) ≤ PartENat.card α
Tactic:
simp only [PartENat.card_eq_coe_fintype_card, Fintype.card_coe, PartENat.coe_le_coe]
Proof state after:
case hα
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
⊢ Set.ncard s ≤ Fintype.card α
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case hα
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
⊢ Set.ncard s ≤ Fintype.card α
Tactic:
apply Set.ncard_le_fintype_card
Proof state after:
no goals
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 α
⊢ Set.Nonempty s
Tactic:
rw [← Set.ncard_pos, hs]
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 α
⊢ 0 < succ k
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 α
⊢ 0 < succ k
Tactic:
exact succ_pos k
Proof state after:
no goals
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
⊢ Subtype.val '' t = s \ {a}
Tactic:
rw [Set.image_preimage_eq_inter_range]
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
⊢ s ∩ Set.range Subtype.val = s \ {a}
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
⊢ s ∩ Set.range Subtype.val = s \ {a}
Tactic:
simp only [Subtype.range_coe_subtype]
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
⊢ s ∩ {x | x ∈ SubMulAction.ofStabilizer M a} = s \ {a}
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
⊢ s ∩ {x | x ∈ SubMulAction.ofStabilizer M a} = s \ {a}
Tactic:
rw [Set.diff_eq_compl_inter, Set.inter_comm]
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
⊢ {x | x ∈ SubMulAction.ofStabilizer M a} ∩ s = {a}ᶜ ∩ s
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
⊢ {x | x ∈ SubMulAction.ofStabilizer M a} ∩ s = {a}ᶜ ∩ s
Tactic:
congr
Proof state after:
no goals
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}
⊢ s = insert a (Subtype.val '' t)
Tactic:
rw [hat, Set.insert_diff_singleton, Set.insert_eq_of_mem has]
Proof state after:
no goals
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)
⊢ fixingSubgroup M s = ?m.186999
Tactic:
rw [hat']
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)
⊢ fixingSubgroup M (insert a (Subtype.val '' t)) = ?m.186999

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 M
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)
⊢ fixingSubgroup M (insert a (Subtype.val '' t)) = ?m.186999

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 M
Tactic:
exact fixingSubgroup_of_insert M a t
Proof state after:
no goals
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)
⊢ Function.Injective ⇑(Subgroup.subtype (stabilizer M a))
Tactic:
simp only [Subgroup.coeSubtype, Subtype.coe_injective]
Proof state after:
no goals
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)
⊢ Set.ncard s = 1 + Set.ncard t
Tactic:
rw [hat']
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)
⊢ Set.ncard (insert a (Subtype.val '' t)) = 1 + Set.ncard t