awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
h : map (α := List α) length (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) = c
⊢ map (α := List α) length (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) = c ∧
    (∀ (s : List α),
        Membership.mem (γ := List (List α))
            (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) s →
          s.Nodup) ∧
      Pairwise (α := List α) Disjoint
        (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l)
have h₁ : (∀ (s : List α),
    Membership.mem (γ := List (List α))
        (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) s →
      s.Nodup) ∧
  Pairwise (α := List α) Disjoint (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
⊢ map (α := List α) length (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) = c
have h : map (α := List α) length (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) =
  map length c.ranges
Tactic: rw [← ranges_length c]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
⊢ (∀ (s : List α),
      Membership.mem (γ := List (List α))
          (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) s →
        s.Nodup) ∧
    Pairwise (α := List α) Disjoint (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l)
have h : ∀ (s : List α),
  Membership.mem (γ := List (List α))
      (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) s →
    s.Nodup
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
h :
  ∀ (s : List α),
    Membership.mem (γ := List (List α))
        (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) s →
      s.Nodup
⊢ (∀ (s : List α),
      Membership.mem (γ := List (List α))
          (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) s →
        s.Nodup) ∧
    Pairwise (α := List α) Disjoint (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l)
have h₁ : Pairwise (α := List α) Disjoint (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
s : List α
⊢ Membership.mem (γ := List (List α))
      (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) s →
    s.Nodup
have h : (∃ a ∈ l, map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α) a = s) → s.Nodup
Tactic: rw [mem_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
t : List (Fin (Fintype.card α))
ht : t ∈ l
⊢ Nodup (α := α) (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α) t)
have h : t.Nodup
Tactic: apply Nodup.map (Equiv.injective _)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
t : List (Fin (Fintype.card α))
ht : t ∈ l
⊢ t.Nodup
have h : ∀ (u : List ℕ) (hu : u ∈ c.ranges) (ht : klift' u sorry ∈ l), (klift' u sorry).Nodup
Tactic: obtain ⟨u, hu, rfl⟩ := mem_pmap.mp ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
u : List ℕ
hu : u ∈ c.ranges
ht : klift' u ⋯ ∈ l
⊢ (klift' u ⋯).Nodup
have h : Nodup (α := ℕ) (map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' u sorry))
Tactic: apply Nodup.of_map
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
u : List ℕ
hu : u ∈ c.ranges
ht : klift' u ⋯ ∈ l
h : Nodup (α := ℕ) (map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' u ⋯))
⊢ (klift' u ⋯).Nodup
have h₁ : Type
Tactic: apply Nodup.of_map
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
u : List ℕ
hu : u ∈ c.ranges
ht : klift' u ⋯ ∈ l
h : Nodup (α := ℕ) (map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' u ⋯))
h₁ : Type
⊢ (klift' u ⋯).Nodup
have h₂ : Fin (Fintype.card α) → ℕ
Tactic: apply Nodup.of_map
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
⊢ Pairwise (α := List α) Disjoint (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l)
have h : Pairwise (fun (s t : List (Fin (Fintype.card α))) ↦ s.Disjoint t) l
Tactic: refine Pairwise.map _ (fun s t ↦ disjoint_map (Equiv.injective _)) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
⊢ Pairwise (fun (s t : List (Fin (Fintype.card α))) ↦ s.Disjoint t) l
have h : ∀ ⦃x : List ℕ⦄ (hx : ∀ a ∈ x, a < Fintype.card α) ⦃y : List ℕ⦄ (hy : ∀ a ∈ y, a < Fintype.card α),
  x.Disjoint y → (klift' x hx).Disjoint (klift' y hy)
Tactic: apply Pairwise.pmap (List.ranges_disjoint c)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_2
inst : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → (hn : n < Fintype.card α) → Fin (Fintype.card α) := fun (n : ℕ) (hn : n < Fintype.card α) ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (hl : ∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) :=
  fun (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) ↦ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α) klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) :=
  pmap (P := fun (a : List ℕ) ↦ ∀ a_1 ∈ a, a_1 < Fintype.card α) klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
v : List ℕ
hv : ∀ a ∈ v, a < Fintype.card α
huv : u.Disjoint v
⊢ (klift' u hu).Disjoint (klift' v hv)
have h : ∀ (a a' : ℕ) (ha : a < Fintype.card α) (ha' : a' < Fintype.card α), klift a ha = klift a' ha' → a = a'
Tactic: apply disjoint_pmap
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
⊢ (∃ (g : Perm α), g.cycleType = m) ↔ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
have mp : (∃ (g : Perm α), g.cycleType = m) → m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
mp : (∃ (g : Perm α), g.cycleType = m) → m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (∃ (g : Perm α), g.cycleType = m) ↔ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
have mpr : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) → ∃ (g : Perm α), g.cycleType = m
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
h : ∃ (g : Perm α), g.cycleType = m
⊢ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
have mp : ∀ (g : Perm α) (hg : g.cycleType = m), m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic: obtain ⟨g, hg⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
⊢ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
have mp : m.sum ≤ Fintype.card α
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
mp : m.sum ≤ Fintype.card α
⊢ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
have mp₁ : ∀ a ∈ m, 2 ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
⊢ m.sum ≤ Fintype.card α
have mp : g.support.card ≤ Fintype.card α
Tactic: rw [← hg, Equiv.Perm.sum_cycleType]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
a : ℕ
⊢ a ∈ m → 2 ≤ a
have mp : a ∈ g.cycleType → 2 ≤ a
Tactic: rw [← hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ ∃ (g : Perm α), g.cycleType = m
have hc' : m.toList.sum ≤ Fintype.card α
Tactic: have hc' : m.toList.sum ≤ Fintype.card α := by
      simp only [Multiset.sum_toList]
      exact hc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
⊢ ∃ (g : Perm α), g.cycleType = m
have mpr : ∀ (p : List (List α)) (hp_length : List.map List.length p = m.toList) (hp_nodup : ∀ s ∈ p, s.Nodup)
  (hp_disj : List.Pairwise List.Disjoint p), ∃ (g : Perm α), g.cycleType = m
Tactic: obtain ⟨p, hp_length, hp_nodup, hp_disj⟩ := List.exists_pw_disjoint_with_card hc'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
⊢ ∃ (g : Perm α), g.cycleType = m
have h : cycleType (α := α) (List.prod (List.map (fun (l : List α) ↦ l.formPerm) p)) = m
Tactic: use List.prod (List.map (fun l => List.formPerm l) p)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ 2 ≤ x.length
have apply : x.length ∈ m
Tactic: apply h2c x.length
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ x.length ∈ m
have rw : ∃ a ∈ p, a.length = x.length
Tactic: rw [← Multiset.mem_toList, ← hp_length, List.mem_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
⊢ cycleType (α := α) (List.prod (List.map (fun (l : List α) ↦ l.formPerm) p)) = m
have hp2 : ∀ x ∈ p, 2 ≤ x.length
Tactic: have hp2 : ∀ x ∈ p, 2 ≤ x.length := by
      intro x hx
      apply h2c x.length
      rw [← Multiset.mem_toList, ← hp_length, List.mem_map]
      exact ⟨x, hx, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ cycleType (α := α) (List.prod (List.map (fun (l : List α) ↦ l.formPerm) p)) = m
have h : (↑(List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p)) : Multiset ℕ) = m
Tactic: rw [Equiv.Perm.cycleType_eq _ rfl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
h : (↑(List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p)) : Multiset ℕ) = m
⊢ cycleType (α := α) (List.prod (List.map (fun (l : List α) ↦ l.formPerm) p)) = m
have h₁ : ∀ (σ : Perm α), Membership.mem (γ := List (Perm α)) (List.map (fun (l : List α) ↦ l.formPerm) p) σ → σ.IsCycle
Tactic: rw [Equiv.Perm.cycleType_eq _ rfl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
h : (↑(List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p)) : Multiset ℕ) = m
h₁ : ∀ (σ : Perm α), Membership.mem (γ := List (Perm α)) (List.map (fun (l : List α) ↦ l.formPerm) p) σ → σ.IsCycle
⊢ cycleType (α := α) (List.prod (List.map (fun (l : List α) ↦ l.formPerm) p)) = m
have h₂ : List.Pairwise (α := Perm α) Disjoint (List.map (fun (l : List α) ↦ l.formPerm) p)
Tactic: rw [Equiv.Perm.cycleType_eq _ rfl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ (↑(List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p)) : Multiset ℕ) = m
have h : (↑(List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p)) : Multiset ℕ) =
  (↑m.toList : Multiset ℕ)
Tactic: rw [← Multiset.coe_toList m]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ (↑(List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p)) : Multiset ℕ) =
    (↑m.toList : Multiset ℕ)
have h : List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p) = m.toList
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.map (α := Perm α) (Finset.card ∘ support) (List.map (fun (l : List α) ↦ l.formPerm) p) = m.toList
have h : List.map (Function.comp (β := Perm α) (Finset.card ∘ support) fun (l : List α) ↦ l.formPerm) p = m.toList
Tactic: rw [List.map_map]