Theorem: OnCycleFactors.hφ_range_card (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ Nat.card ↥(MonoidHom.range (φ g)) =
    Multiset.prod
      (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
        (Multiset.dedup (Equiv.Perm.cycleType g)))
Tactic:
rw [hφ_range_card', Equiv.Perm.of_partition_card]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ (Finset.prod Finset.univ fun i => Nat.factorial (Fintype.card ↑{a | fsc a = i})) =
    Multiset.prod
      (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
        (Multiset.dedup (Equiv.Perm.cycleType g)))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
Tactic:
rintro ⟨i, hi⟩
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count (↑{ val := i, isLt := hi }) (Equiv.Perm.cycleType g)

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count (↑{ val := i, isLt := hi }) (Equiv.Perm.cycleType g)
Tactic:
rw [Equiv.Perm.cycleType_def]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count (↑{ val := i, isLt := hi })
      (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count (↑{ val := i, isLt := hi })
      (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
simp only [Fin.val_mk]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count i (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Multiset.count i (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
rw [← Set.ncard_filter_eq_count (Finset.card ∘ Equiv.Perm.support) g.cycleFactorsFinset i]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i}

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card ↑{a | fsc a = { val := i, isLt := hi }} =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i}
Tactic:
simp only [Set.coe_setOf, Set.mem_setOf_eq, Function.comp_apply]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}
Tactic:
let u : {x : g.cycleFactorsFinset | fsc x = ⟨i, hi⟩} →
    {x ∈ g.cycleFactorsFinset | (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun ⟨⟨x, hx⟩, hx'⟩ => ⟨x, by
    simp only [fsc, Fin.mk.injEq, Set.mem_setOf_eq] at hx'
    simp only [Function.comp_apply, Set.mem_setOf_eq]
    exact ⟨hx, hx'⟩⟩
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
this : Function.Bijective u
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Set.ncard {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}
Tactic:
rw [← Set.Nat.card_coe_set_eq, Nat.card_eq_fintype_card]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
this : Function.Bijective u
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Fintype.card ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
this : Function.Bijective u
⊢ Fintype.card { x // fsc x = { val := i, isLt := hi } } =
    Fintype.card ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i}
Tactic:
apply Fintype.card_of_bijective this
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
⊢ ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
Tactic:
intro i hi
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i < Fintype.card α + 1

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i < Fintype.card α + 1
Tactic:
rw [Nat.lt_succ_iff]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i ≤ Fintype.card α

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i ≤ Fintype.card α
Tactic:
apply le_trans _ (Finset.card_le_univ g.support)
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i ≤ (Equiv.Perm.support g).card

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i ≤ (Equiv.Perm.support g).card
Tactic:
apply Equiv.Perm.le_card_support_of_mem_cycleType
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i ∈ Equiv.Perm.cycleType g

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ i ∈ Equiv.Perm.cycleType g
Tactic:
exact hi
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ (Finset.prod Finset.univ fun i => Nat.factorial (Fintype.card ↑{a | fsc a = i})) =
    Multiset.prod
      (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
        (Multiset.dedup (Equiv.Perm.cycleType g)))
Tactic:
simp_rw [hlc]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ (Finset.prod Finset.univ fun x => Nat.factorial (Multiset.count (↑x) (Equiv.Perm.cycleType g))) =
    Multiset.prod
      (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
        (Multiset.dedup (Equiv.Perm.cycleType g)))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ (Finset.prod Finset.univ fun x => Nat.factorial (Multiset.count (↑x) (Equiv.Perm.cycleType g))) =
    Multiset.prod
      (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
        (Multiset.dedup (Equiv.Perm.cycleType g)))
Tactic:
rw [← Finset.prod_range fun i => (g.cycleType.count i).factorial]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ (Finset.prod (Finset.range (Fintype.card α + 1)) fun i => Nat.factorial (Multiset.count i (Equiv.Perm.cycleType g))) =
    Multiset.prod
      (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
        (Multiset.dedup (Equiv.Perm.cycleType g)))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ (Finset.prod (Finset.range (Fintype.card α + 1)) fun i => Nat.factorial (Multiset.count i (Equiv.Perm.cycleType g))) =
    Multiset.prod
      (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
        (Multiset.dedup (Equiv.Perm.cycleType g)))
Tactic:
rw [← Multiset.prod_toFinset]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ (Finset.prod (Finset.range (Fintype.card α + 1)) fun i => Nat.factorial (Multiset.count i (Equiv.Perm.cycleType g))) =
    Finset.prod (Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))) fun n =>
      Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g))

case hm
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ Multiset.Nodup (Multiset.dedup (Equiv.Perm.cycleType g))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ (Finset.prod (Finset.range (Fintype.card α + 1)) fun i => Nat.factorial (Multiset.count i (Equiv.Perm.cycleType g))) =
    Finset.prod (Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))) fun n =>
      Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g))

case hm
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ Multiset.Nodup (Multiset.dedup (Equiv.Perm.cycleType g))
Tactic:
apply symm
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ (Finset.prod (Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))) fun n =>
      Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g))) =
    Finset.prod (Finset.range (Fintype.card α + 1)) fun i => Nat.factorial (Multiset.count i (Equiv.Perm.cycleType g))

case hm
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ Multiset.Nodup (Multiset.dedup (Equiv.Perm.cycleType g))

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ (Finset.prod (Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))) fun n =>
      Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g))) =
    Finset.prod (Finset.range (Fintype.card α + 1)) fun i => Nat.factorial (Multiset.count i (Equiv.Perm.cycleType g))

case hm
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ Multiset.Nodup (Multiset.dedup (Equiv.Perm.cycleType g))
Tactic:
apply Finset.prod_subset_one_on_sdiff
State after:
case a.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g)) ⊆ Finset.range (Fintype.card α + 1)

case a.hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ ∀ x ∈ Finset.range (Fintype.card α + 1) \ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g)),
    Nat.factorial (Multiset.count x (Equiv.Perm.cycleType g)) = 1

case a.hfg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ ∀ x ∈ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g)),
    Nat.factorial (Multiset.count x (Equiv.Perm.cycleType g)) =
      Nat.factorial (Multiset.count x (Equiv.Perm.cycleType g))

case hm
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ Multiset.Nodup (Multiset.dedup (Equiv.Perm.cycleType g))

State before:
case hm
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ Multiset.Nodup (Multiset.dedup (Equiv.Perm.cycleType g))
Tactic:
exact g.cycleType.nodup_dedup
State after:
no goals

State before:
case a.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g)) ⊆ Finset.range (Fintype.card α + 1)
Tactic:
intro i hi
State after:
case a.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i ∈ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))
⊢ i ∈ Finset.range (Fintype.card α + 1)

State before:
case a.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i ∈ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))
⊢ i ∈ Finset.range (Fintype.card α + 1)
Tactic:
rw [Finset.mem_range]
State after:
case a.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i ∈ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))
⊢ i < Fintype.card α + 1

State before:
case a.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i ∈ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))
⊢ i < Fintype.card α + 1
Tactic:
apply hl_lt
State after:
case a.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i ∈ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))
⊢ i ∈ Equiv.Perm.cycleType g

State before:
case a.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i ∈ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))
⊢ i ∈ Equiv.Perm.cycleType g
Tactic:
simpa only [Multiset.mem_toFinset, Multiset.mem_dedup] using hi
State after:
no goals

State before:
case a.hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ ∀ x ∈ Finset.range (Fintype.card α + 1) \ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g)),
    Nat.factorial (Multiset.count x (Equiv.Perm.cycleType g)) = 1
Tactic:
intro i hi
State after:
case a.hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i ∈ Finset.range (Fintype.card α + 1) \ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))
⊢ Nat.factorial (Multiset.count i (Equiv.Perm.cycleType g)) = 1

State before:
case a.hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i ∈ Finset.range (Fintype.card α + 1) \ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g))
⊢ Nat.factorial (Multiset.count i (Equiv.Perm.cycleType g)) = 1
Tactic:
simp only [Finset.mem_sdiff, Finset.mem_range, Multiset.mem_toFinset, Multiset.mem_dedup] at hi
State after:
case a.hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i < Fintype.card α + 1 ∧ i ∉ Equiv.Perm.cycleType g
⊢ Nat.factorial (Multiset.count i (Equiv.Perm.cycleType g)) = 1

State before:
case a.hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i < Fintype.card α + 1 ∧ i ∉ Equiv.Perm.cycleType g
⊢ Nat.factorial (Multiset.count i (Equiv.Perm.cycleType g)) = 1
Tactic:
rw [Multiset.count_eq_zero_of_not_mem hi.2]
State after:
case a.hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i < Fintype.card α + 1 ∧ i ∉ Equiv.Perm.cycleType g
⊢ Nat.factorial 0 = 1

State before:
case a.hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
i : ℕ
hi : i < Fintype.card α + 1 ∧ i ∉ Equiv.Perm.cycleType g
⊢ Nat.factorial 0 = 1
Tactic:
exact Nat.factorial_zero
State after:
no goals

State before:
case a.hfg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
hlc : ∀ (n : Fin (Fintype.card α + 1)), Fintype.card ↑{a | fsc a = n} = Multiset.count (↑n) (Equiv.Perm.cycleType g)
hl_lt : ∀ i ∈ Equiv.Perm.cycleType g, i < Fintype.card α + 1
⊢ ∀ x ∈ Multiset.toFinset (Multiset.dedup (Equiv.Perm.cycleType g)),
    Nat.factorial (Multiset.count x (Equiv.Perm.cycleType g)) =
      Nat.factorial (Multiset.count x (Equiv.Perm.cycleType g))
Tactic:
exact fun i _ ↦ rfl
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
x✝ : ↑{x | fsc x = { val := i, isLt := hi }}
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : { val := x, property := hx } ∈ {x | fsc x = { val := i, isLt := hi }}
⊢ x ∈ {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i}
Tactic:
simp only [fsc, Fin.mk.injEq, Set.mem_setOf_eq] at hx'
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
x✝ : ↑{x | fsc x = { val := i, isLt := hi }}
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : (Equiv.Perm.support x).card = i
⊢ x ∈ {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i}

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
x✝ : ↑{x | fsc x = { val := i, isLt := hi }}
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : (Equiv.Perm.support x).card = i
⊢ x ∈ {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i}
Tactic:
simp only [Function.comp_apply, Set.mem_setOf_eq]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
x✝ : ↑{x | fsc x = { val := i, isLt := hi }}
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : (Equiv.Perm.support x).card = i
⊢ x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
x✝ : ↑{x | fsc x = { val := i, isLt := hi }}
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : (Equiv.Perm.support x).card = i
⊢ x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
Tactic:
exact ⟨hx, hx'⟩
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
⊢ Function.Bijective u
Tactic:
constructor
State after:
case left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
⊢ Function.Injective u

case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
⊢ Function.Surjective u

State before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
⊢ Function.Surjective u
Tactic:
rintro ⟨x, hx⟩
State after:
case right.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i}
⊢ ∃ a, u a = { val := x, property := hx }

State before:
case right.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ {x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i}
⊢ ∃ a, u a = { val := x, property := hx }
Tactic:
simp only [Function.comp_apply, Set.mem_setOf_eq] at hx
State after:
case right.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ ∃ a, u a = { val := x, property := hx }

State before:
case right.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ ∃ a, u a = { val := x, property := hx }
Tactic:
use! x
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ x ∈ Equiv.Perm.cycleFactorsFinset g

case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ { val := x, property := ?property } ∈ {x | fsc x = { val := i, isLt := hi }}

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ x ∈ Equiv.Perm.cycleFactorsFinset g

case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ { val := x, property := ?property } ∈ {x | fsc x = { val := i, isLt := hi }}
Tactic:
exact hx.1
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ { val := x, property := ⋯ } ∈ {x | fsc x = { val := i, isLt := hi }}

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ { val := x, property := ⋯ } ∈ {x | fsc x = { val := i, isLt := hi }}
Tactic:
simp only [fsc, Fin.mk.injEq, Set.mem_setOf_eq]
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ (Equiv.Perm.support x).card = i

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Equiv.Perm.support x).card = i
⊢ (Equiv.Perm.support x).card = i
Tactic:
exact hx.2
State after:
no goals

State before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
⊢ Function.Injective u
Tactic:
rintro ⟨⟨x, hx⟩, hx'⟩ ⟨⟨y, hy⟩, hy'⟩ h
State after:
case left.mk.mk.mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : { val := x, property := hx } ∈ {x | fsc x = { val := i, isLt := hi }}
y : Equiv.Perm α
hy : y ∈ Equiv.Perm.cycleFactorsFinset g
hy' : { val := y, property := hy } ∈ {x | fsc x = { val := i, isLt := hi }}
h :
  u { val := { val := x, property := hx }, property := hx' } =
    u { val := { val := y, property := hy }, property := hy' }
⊢ { val := { val := x, property := hx }, property := hx' } = { val := { val := y, property := hy }, property := hy' }

State before:
case left.mk.mk.mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : { val := x, property := hx } ∈ {x | fsc x = { val := i, isLt := hi }}
y : Equiv.Perm α
hy : y ∈ Equiv.Perm.cycleFactorsFinset g
hy' : { val := y, property := hy } ∈ {x | fsc x = { val := i, isLt := hi }}
h :
  u { val := { val := x, property := hx }, property := hx' } =
    u { val := { val := y, property := hy }, property := hy' }
⊢ { val := { val := x, property := hx }, property := hx' } = { val := { val := y, property := hy }, property := hy' }
Tactic:
simp only [Function.comp_apply, Set.coe_setOf, Set.mem_setOf_eq, Subtype.mk.injEq, u] at h
State after:
case left.mk.mk.mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : { val := x, property := hx } ∈ {x | fsc x = { val := i, isLt := hi }}
y : Equiv.Perm α
hy : y ∈ Equiv.Perm.cycleFactorsFinset g
hy' : { val := y, property := hy } ∈ {x | fsc x = { val := i, isLt := hi }}
h : x = y
⊢ { val := { val := x, property := hx }, property := hx' } = { val := { val := y, property := hy }, property := hy' }

State before:
case left.mk.mk.mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
i : ℕ
hi : i < Fintype.card α + 1
u : ↑{x | fsc x = { val := i, isLt := hi }} →
  ↑{x | x ∈ Equiv.Perm.cycleFactorsFinset g ∧ (Finset.card ∘ Equiv.Perm.support) x = i} :=
  fun x =>
    match x with
    | { val := { val := x, property := hx }, property := hx' } => { val := x, property := ⋯ }
x : Equiv.Perm α
hx : x ∈ Equiv.Perm.cycleFactorsFinset g
hx' : { val := x, property := hx } ∈ {x | fsc x = { val := i, isLt := hi }}
y : Equiv.Perm α
hy : y ∈ Equiv.Perm.cycleFactorsFinset g
hy' : { val := y, property := hy } ∈ {x | fsc x = { val := i, isLt := hi }}
h : x = y
⊢ { val := { val := x, property := hx }, property := hx' } = { val := { val := y, property := hy }, property := hy' }
Tactic:
simp only [h, Set.coe_setOf, Set.mem_setOf_eq, Subtype.mk.injEq]
State after:
no goals