internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.hφ_range_card
Proof 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]
Proof 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 α
Theorem: OnCycleFactors.hφ_range_card
Proof 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)
Proof 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
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_range_card
Proof 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]
Proof 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)))
Theorem: OnCycleFactors.hφ_range_card
Proof 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]
Proof 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)))
Theorem: OnCycleFactors.hφ_range_card
Proof 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]
Proof 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))
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof 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))
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof 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))
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof 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)
Theorem: OnCycleFactors.hφ_range_card
Proof 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]
Proof 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
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_range_card
Proof 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]
Proof 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
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_range_card
Proof 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'
Proof 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}
Theorem: OnCycleFactors.hφ_range_card
Proof 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]
Proof 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
Theorem: OnCycleFactors.hφ_range_card
Proof 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'⟩
Proof state after:
no goals
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof 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
Theorem: OnCycleFactors.hφ_range_card
Proof 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⟩
Proof 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 }
Theorem: OnCycleFactors.hφ_range_card
Proof 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
Proof 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 }