Theorem: OnCycleFactors.card_le_of_mem_kerφ (Jordan/ConjClassCount.lean)

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]
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 α

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
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

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
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

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
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

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
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)

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
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

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 _
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

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]
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

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]
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

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]
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

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
State after:
no goals

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
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

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
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

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 _ ∈ _
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

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
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)

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]
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)

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 _
State after:
no goals

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]
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)

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
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)

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]
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 α

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
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 α

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]
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 α

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 _
State after:
no goals