internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.odd_of_mem_kerφ
Proof state before:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ ConjAct.toConjAct
      {
        toFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
        invFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
        left_inv := ⋯, right_inv := ⋯ } ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) ?a.K✝

case a.K
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ Subgroup ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
Tactic:
rw [OnCycleFactors.hφ_ker_eq_θ_range]
Proof state after:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ {
      toFun :=
        θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
          (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
      invFun :=
        θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
          (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
      left_inv := ⋯, right_inv := ⋯ } ∈
    Set.range ⇑(θ g)
Theorem: OnCycleFactors.odd_of_mem_kerφ
Proof state before:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ {
      toFun :=
        θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
          (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
      invFun :=
        θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
          (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
      left_inv := ⋯, right_inv := ⋯ } ∈
    Set.range ⇑(θ g)
Tactic:
exact Set.mem_range_self _
Proof state after:
no goals
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
Tactic:
rw [← not_lt]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
⊢ ¬Multiset.sum (Equiv.Perm.cycleType g) + 1 < Fintype.card α
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
⊢ ¬Multiset.sum (Equiv.Perm.cycleType g) + 1 < Fintype.card α
Tactic:
intro hm
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 1 < Fintype.card α
⊢ False
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 1 < Fintype.card α
⊢ False
Tactic:
rw [Nat.lt_iff_add_one_le, add_assoc] at hm
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + (1 + 1) ≤ Fintype.card α
⊢ False
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + (1 + 1) ≤ Fintype.card α
⊢ False
Tactic:
change g.cycleType.sum + 2 ≤ _ at hm
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
⊢ False
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
⊢ False
Tactic:
suffices 1 < Fintype.card (MulAction.fixedBy α g) by
  obtain ⟨a, b, hab⟩ := Fintype.exists_pair_of_one_lt_card this
  suffices Equiv.Perm.sign (θ g ⟨Equiv.swap a b, 1⟩) ≠ 1 by
    apply this
    apply h
    change ConjAct.toConjAct _ ∈ _
    apply Subgroup.map_subtype_le
    rw [OnCycleFactors.hφ_ker_eq_θ_range]
    exact Set.mem_range_self _
  rw [θ_apply_fst]
  simp only [Equiv.Perm.ofSubtype_swap_eq, Equiv.Perm.sign_swap', ne_eq, ite_eq_left_iff,
    neg_units_ne_self, imp_false, not_not]
  rw [Subtype.coe_inj]
  exact hab
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
⊢ 1 < Fintype.card ↑(MulAction.fixedBy α g)
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this : 1 < Fintype.card ↑(MulAction.fixedBy α g)
⊢ False
Tactic:
obtain ⟨a, b, hab⟩ := Fintype.exists_pair_of_one_lt_card this
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
⊢ False
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
⊢ False
Tactic:
suffices Equiv.Perm.sign (θ g ⟨Equiv.swap a b, 1⟩) ≠ 1 by
  apply this
  apply h
  change ConjAct.toConjAct _ ∈ _
  apply Subgroup.map_subtype_le
  rw [OnCycleFactors.hφ_ker_eq_θ_range]
  exact Set.mem_range_self _
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
⊢ Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
⊢ Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
Tactic:
rw [θ_apply_fst]
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
⊢ Equiv.Perm.sign (Equiv.Perm.ofSubtype (Equiv.swap a b)) ≠ 1
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
⊢ Equiv.Perm.sign (Equiv.Perm.ofSubtype (Equiv.swap a b)) ≠ 1
Tactic:
simp only [Equiv.Perm.ofSubtype_swap_eq, Equiv.Perm.sign_swap', ne_eq, ite_eq_left_iff,
  neg_units_ne_self, imp_false, not_not]
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
⊢ ¬↑a = ↑b
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
⊢ ¬↑a = ↑b
Tactic:
rw [Subtype.coe_inj]
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
⊢ ¬a = b
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
⊢ ¬a = b
Tactic:
exact hab
Proof state after:
no goals
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ False
Tactic:
apply this
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) = 1
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) = 1
Tactic:
apply h
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ (θ g) (Equiv.swap a b, 1) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ (θ g) (Equiv.swap a b, 1) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Tactic:
change ConjAct.toConjAct _ ∈ _
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ ConjAct.toConjAct
      { toFun := θAux g (Equiv.swap a b, 1).1 (Equiv.swap a b, 1).2,
        invFun := θAux g (Equiv.swap a b, 1).1⁻¹ (Equiv.swap a b, 1).2⁻¹, left_inv := ⋯, right_inv := ⋯ } ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ ConjAct.toConjAct
      { toFun := θAux g (Equiv.swap a b, 1).1 (Equiv.swap a b, 1).2,
        invFun := θAux g (Equiv.swap a b, 1).1⁻¹ (Equiv.swap a b, 1).2⁻¹, left_inv := ⋯, right_inv := ⋯ } ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Tactic:
apply Subgroup.map_subtype_le
Proof state after:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ ConjAct.toConjAct
      { toFun := θAux g (Equiv.swap a b, 1).1 (Equiv.swap a b, 1).2,
        invFun := θAux g (Equiv.swap a b, 1).1⁻¹ (Equiv.swap a b, 1).2⁻¹, left_inv := ⋯, right_inv := ⋯ } ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) ?a.K✝

case a.K
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ Subgroup ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ ConjAct.toConjAct
      { toFun := θAux g (Equiv.swap a b, 1).1 (Equiv.swap a b, 1).2,
        invFun := θAux g (Equiv.swap a b, 1).1⁻¹ (Equiv.swap a b, 1).2⁻¹, left_inv := ⋯, right_inv := ⋯ } ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) ?a.K✝

case a.K
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ Subgroup ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
Tactic:
rw [OnCycleFactors.hφ_ker_eq_θ_range]
Proof state after:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ { toFun := θAux g (Equiv.swap a b, 1).1 (Equiv.swap a b, 1).2,
      invFun := θAux g (Equiv.swap a b, 1).1⁻¹ (Equiv.swap a b, 1).2⁻¹, left_inv := ⋯, right_inv := ⋯ } ∈
    Set.range ⇑(θ g)
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(MulAction.fixedBy α g)
a b : ↑(MulAction.fixedBy α g)
hab : a ≠ b
this : Equiv.Perm.sign ((θ g) (Equiv.swap a b, 1)) ≠ 1
⊢ { toFun := θAux g (Equiv.swap a b, 1).1 (Equiv.swap a b, 1).2,
      invFun := θAux g (Equiv.swap a b, 1).1⁻¹ (Equiv.swap a b, 1).2⁻¹, left_inv := ⋯, right_inv := ⋯ } ∈
    Set.range ⇑(θ g)
Tactic:
exact Set.mem_range_self _
Proof state after:
no goals
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
⊢ 1 < Fintype.card ↑(MulAction.fixedBy α g)
Tactic:
rw [OnCycleFactors.Equiv.Perm.card_fixedBy g]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
⊢ 1 < Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : Multiset.sum (Equiv.Perm.cycleType g) + 2 ≤ Fintype.card α
⊢ 1 < Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)
Tactic:
rw [add_comm] at hm
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : 2 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
⊢ 1 < Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : 2 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
⊢ 1 < Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)
Tactic:
rw [Nat.lt_iff_add_one_le, Nat.le_sub_iff_add_le]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : 2 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
⊢ 1 + 1 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : 2 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
⊢ Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : 2 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
⊢ 1 + 1 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : 2 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
⊢ Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
Tactic:
exact hm
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : 2 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
⊢ Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : 2 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
⊢ Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
Tactic:
rw [Equiv.Perm.sum_cycleType]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : 2 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
⊢ (Equiv.Perm.support g).card ≤ Fintype.card α
Theorem: OnCycleFactors.card_le_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm : 2 + Multiset.sum (Equiv.Perm.cycleType g) ≤ Fintype.card α
⊢ (Equiv.Perm.support g).card ≤ Fintype.card α
Tactic:
exact Finset.card_le_univ _
Proof state after:
no goals
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
⊢ ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
rw [← Multiset.nodup_iff_count_le_one, Equiv.Perm.cycleType_def]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
⊢ Multiset.Nodup (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
⊢ Multiset.Nodup (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
rw [Multiset.nodup_map_iff_inj_on g.cycleFactorsFinset.nodup]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
⊢ ∀ x ∈ (Equiv.Perm.cycleFactorsFinset g).val,
    ∀ y ∈ (Equiv.Perm.cycleFactorsFinset g).val,
      (Finset.card ∘ Equiv.Perm.support) x = (Finset.card ∘ Equiv.Perm.support) y → x = y