awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
a : List ℕ
ha : a ∈ c.ranges
rw :
  pmap (P := fun (a : ℕ) ↦ a < Fintype.card α)
      (fun (a : ℕ) (h : a < Fintype.card α) ↦ (Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift a h)) a ⋯ =
    map id a
⊢ map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = map id a

Tactic:
rw [List.map_pmap]

Premises used: List.map_pmap
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
a : List ℕ
ha : a ∈ c.ranges
⊢ pmap (P := fun (a : ℕ) ↦ a < Fintype.card α)
      (fun (a : ℕ) (h : a < Fintype.card α) ↦ (Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift a h)) a ⋯ =
    map id a

Tactic:
simp [klift, Fin.valEmbedding_apply, List.pmap_eq_map, List.map_id']

Premises used: List.map_id', Fin.valEmbedding_apply, List.pmap_eq_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
⊢ ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a

Tactic:
have hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges),
    (klift' a (hc'_lt a ha)).map Fin.valEmbedding = a := by
    intro a ha
    conv_rhs => rw [← List.map_id a]
    rw [List.map_pmap]
    simp [klift, Fin.valEmbedding_apply, List.pmap_eq_map, List.map_id']
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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 ∧
    (∀ (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)
⊢ ∃ (o : List (List α)), map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o

Tactic:
use l.map (List.map (Fintype.equivFin α).symm)

Premises used: List.map, Fintype.equivFin, Equiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
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)
⊢ 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)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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) =
    map length c.ranges
⊢ map (α := List α) length (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) = c

Tactic:
rw [← ranges_length c]

Premises used: List.ranges_length
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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) =
    map length c.ranges

Tactic:
simp only [l, klift', map_pmap, length_pmap,
      pmap_eq_map]

Premises used: List.map_pmap, List.length_pmap, List.pmap_eq_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
h₁ : Pairwise (α := List α) Disjoint (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l)
⊢ (∀ (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
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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 α
h : (∃ a ∈ l, map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α) a = s) → s.Nodup
⊢ Membership.mem (γ := List (List α))
      (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) s →
    s.Nodup

Tactic:
rw [mem_map]

Premises used: List.mem_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
h : t.Nodup
⊢ Nodup (α := α) (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α) t)

Tactic:
apply Nodup.map (Equiv.injective _)

Premises used: List.Nodup.map, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
h : ∀ (u : List ℕ) (hu : u ∈ c.ranges) (ht : klift' u ⋯ ∈ l), (klift' u ⋯).Nodup
⊢ t.Nodup

Tactic:
obtain ⟨u, hu, rfl⟩ := mem_pmap.mp ht

Premises used: List.mem_pmap, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
h₂ : Fin (Fintype.card α) → ℕ
⊢ (klift' u ⋯).Nodup

Tactic:
apply Nodup.of_map

Premises used: List.Nodup.of_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
⊢ u.Nodup

Tactic:
ranges_nodup hu

Premises used: List.ranges_nodup
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
⊢ u.Nodup

Tactic:
exact ranges_nodup hu

Premises used: List.ranges_nodup
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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)

Tactic:
Pairwise.map _ (fun s t ↦ disjoint_map (Equiv.injective _)) ?_

Premises used: Fintype.equivFin, List.Pairwise.map, Equiv.injective, Equiv.symm, List.disjoint_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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 : Pairwise (fun (s t : List (Fin (Fintype.card α))) ↦ s.Disjoint t) l
⊢ Pairwise (α := List α) Disjoint (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l)

Tactic:
refine Pairwise.map _ (fun s t ↦ disjoint_map (Equiv.injective _)) ?_

Premises used: List.Pairwise.map, Equiv.injective, List.disjoint_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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 :
  ∀ ⦃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)
⊢ Pairwise (fun (s t : List (Fin (Fintype.card α))) ↦ s.Disjoint t) l

Tactic:
apply Pairwise.pmap (List.ranges_disjoint c)

Premises used: List.Pairwise.pmap, List.ranges_disjoint
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
h : ∀ (a a' : ℕ) (ha : a < Fintype.card α) (ha' : a' < Fintype.card α), klift a ha = klift a' ha' → a = a'
h₁ : u.Disjoint v
⊢ (klift' u hu).Disjoint (klift' v hv)

Tactic:
apply disjoint_pmap

Premises used: List.disjoint_pmap
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
a a' : ℕ
ha : a < Fintype.card α
ha' : a' < Fintype.card α
h : klift a ha = klift a' ha'
⊢ a = a'

Tactic:
simpa only [klift, Fin.mk_eq_mk] using h

Premises used: Fin.mk_eq_mk
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
⊢ u.Disjoint v

Tactic:
huv
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
⊢ u.Disjoint v

Tactic:
exact huv
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
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
mpr : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) → ∃ (g : Perm α), g.cycleType = m
⊢ (∃ (g : Perm α), g.cycleType = m) ↔ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
h : ∃ (g : Perm α), g.cycleType = m
mp : ∀ (g : Perm α) (hg : g.cycleType = m), m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

Tactic:
obtain ⟨g, hg⟩ := h
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
mp : m.sum ≤ Fintype.card α
mp₁ : ∀ a ∈ m, 2 ≤ a
⊢ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
mp : g.support.card ≤ Fintype.card α
⊢ m.sum ≤ Fintype.card α

Tactic:
rw [← hg, Equiv.Perm.sum_cycleType]

Premises used: Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
⊢ g.support.card ≤ Fintype.card α

Tactic:
(Equiv.Perm.support g).card_le_univ

Premises used: Equiv.Perm.support, Finset.card_le_univ
-- Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
⊢ g.support.card ≤ Fintype.card α

Tactic:
exact (Equiv.Perm.support g).card_le_univ

Premises used: Equiv.Perm.support, Finset.card_le_univ