awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
⊢ (σ : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) = x
have hx₁ : (f : (a : α) → α) x = x
Tactic: rw [← hf.right _ (mem_support.mpr hfx)] at hx
Cleared hypotheses: hx, hfx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}
have refine_3 : σ.Disjoint (τ * f⁻¹)
Tactic: rw [union_sdiff_distrib, sdiff_singleton_eq_erase, erase_eq_of_notMem, mul_assoc,
        Disjoint.cycleFactorsFinset_mul_eq_union, hτ hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
refine_3 : σ.Disjoint (τ * f⁻¹)
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}
have refine_3₁ : f ∉ σ.cycleFactorsFinset
Tactic: rw [union_sdiff_distrib, sdiff_singleton_eq_erase, erase_eq_of_notMem, mul_assoc,
        Disjoint.cycleFactorsFinset_mul_eq_union, hτ hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
⊢ σ.Disjoint (τ * f⁻¹)
have hf₁ : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
Tactic: rw [mem_cycleFactorsFinset_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
⊢ (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x
have refine_3 : ∀ (hx : (σ : (a : α) → α) x = x), (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x
Tactic: rcases hd x with hx | hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
refine_3 : ∀ (hx : (σ : (a : α) → α) x = x), (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x
⊢ (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x
have refine_3₁ : ∀ (hx : (τ : (a : α) → α) x = x), (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x
Tactic: rcases hd x with hx | hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
⊢ (σ : (a : α) → α) x = x ∨ (τ * f⁻¹ : (a : α) → α) x = x
have refine_3 : (τ * f⁻¹ : (a : α) → α) x = x
Tactic: refine Or.inr ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
⊢ (τ * f⁻¹ : (a : α) → α) x = x
have pos : ∀ (hfx : (f : (a : α) → α) x = x), (τ * f⁻¹ : (a : α) → α) x = x
Tactic: by_cases hfx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
pos : ∀ (hfx : (f : (a : α) → α) x = x), (τ * f⁻¹ : (a : α) → α) x = x
⊢ (τ * f⁻¹ : (a : α) → α) x = x
have neg : ∀ (hfx : ¬(f : (a : α) → α) x = x), (τ * f⁻¹ : (a : α) → α) x = x
Tactic: by_cases hfx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
hfx : (f : (a : α) → α) x = x
⊢ (τ * f⁻¹ : (a : α) → α) x = x
have pos : Eq (α := α) ((τ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
Tactic: rw [← hfx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
⊢ (τ * f⁻¹ : (a : α) → α) x = x
have neg : (τ : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) = x
Tactic: rw [mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
x : α
hx : (τ : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
⊢ (τ : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) = x
have hx₁ : (f : (a : α) → α) x = x
Tactic: rw [← hf.right _ (mem_support.mpr hfx)] at hx
Cleared hypotheses: hx, hfx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g z : Perm α
⊢ (∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔
    ∀ c ∈ g.cycleFactorsFinset,
      ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support ((z : (a : α) → α) x : α) ↔ x ∈ c.support),
        Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (Subgroup.zpowers c)
          ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
              (z.subtypePerm (p := Membership.mem c.support) hc) :
            Perm α)
have h : ∀ (a : Perm α),
  a ∈ g.cycleFactorsFinset → Commute z a ↔
    a ∈ g.cycleFactorsFinset →
      ∃ (hc : ∀ (x : α), Membership.mem (α := α) a.support ((z : (a : α) → α) x : α) ↔ x ∈ a.support),
        Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (Subgroup.zpowers a)
          ((ofSubtype (p := fun (x : α) ↦ x ∈ a.support) : (a : Perm ↥a.support) → Perm α)
              (z.subtypePerm (p := Membership.mem a.support) hc) :
            Perm α)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g z c : Perm α
⊢ c ∈ g.cycleFactorsFinset → Commute z c ↔
    c ∈ g.cycleFactorsFinset →
      ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support ((z : (a : α) → α) x : α) ↔ x ∈ c.support),
        Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (Subgroup.zpowers c)
          ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
              (z.subtypePerm (p := Membership.mem c.support) hc) :
            Perm α)
have h : c ∈ g.cycleFactorsFinset →
  (Commute z c ↔
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support ((z : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (Subgroup.zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            (z.subtypePerm (p := Membership.mem c.support) hc) :
          Perm α))
Tactic: apply imp_congr_right
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ g.subtypePerm (p := Membership.mem c.support) ⋯ = c.subtypePermOfSupport
have H : ∀ (x : α) (hx : x ∈ c.support),
  Eq.{u_2 + 1} (α := α)
    (↑((g.subtypePerm (p := Membership.mem c.support) sorry : (a : ↥c.support) → ↥c.support)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
      α)
    (↑((c.subtypePermOfSupport : (a : ↥c.support) → ↥c.support) (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
      α)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ Eq.{u_2 + 1} (α := α)
    (↑((g.subtypePerm (p := Membership.mem c.support) ⋯ : (a : ↥c.support) → ↥c.support)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
      α)
    (↑((c.subtypePermOfSupport : (a : ↥c.support) → ↥c.support) (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
      α)
have H : Eq (α := α) ((g : (a : α) → α) x : α) ((c : (a : α) → α) x : α)
Tactic: simp only [subtypePerm_apply, Subtype.coe_mk, subtypePermOfSupport]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute k c ↔
    ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support))
        (Subgroup.zpowers (g.subtypePerm (p := Membership.mem c.support) ⋯))
        (k.subtypePerm (p := Membership.mem c.support) hc')
have rw : (∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
    Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
      (k.subtypePerm (p := Membership.mem c.support) hc')) ↔
  ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
    Membership.mem (γ := Subgroup (Perm ↥c.support))
      (Subgroup.zpowers (g.subtypePerm (p := Membership.mem c.support) sorry))
      (k.subtypePerm (p := Membership.mem c.support) hc')
Tactic: rw [IsCycle.commute_iff' (mem_cycleFactorsFinset_iff.mp hc).1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ (∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
        (k.subtypePerm (p := Membership.mem c.support) hc')) ↔
    ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support))
        (Subgroup.zpowers (g.subtypePerm (p := Membership.mem c.support) ⋯))
        (k.subtypePerm (p := Membership.mem c.support) hc')
have h : ∀ (a : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support),
  Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
      (k.subtypePerm (p := Membership.mem c.support) a) ↔
    Membership.mem (γ := Subgroup (Perm ↥c.support))
      (Subgroup.zpowers (g.subtypePerm (p := Membership.mem c.support) sorry))
      (k.subtypePerm (p := Membership.mem c.support) a)
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support
⊢ (∃ (k_1 : ℤ),
      HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport k_1 = k.subtypePerm (p := Membership.mem c.support) hc') ↔
    ∃ (k_1 : ℤ),
      g.subtypePerm (p := Membership.mem c.support) ⋯ ^ k_1 = k.subtypePerm (p := Membership.mem c.support) hc'
have h : ∀ (a : ℤ),
  HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport a = k.subtypePerm (p := Membership.mem c.support) hc' ↔
    g.subtypePerm (p := Membership.mem c.support) sorry ^ a = k.subtypePerm (p := Membership.mem c.support) hc'
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((k : (a : α) → α) x : α) ↔ x ∈ c.support
n : ℤ
⊢ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport n = k.subtypePerm (p := Membership.mem c.support) hc' ↔
    g.subtypePerm (p := Membership.mem c.support) ⋯ ^ n = k.subtypePerm (p := Membership.mem c.support) hc'
have h : HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport n = k.subtypePerm (p := Membership.mem c.support) hc' ↔
  HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport n = k.subtypePerm (p := Membership.mem c.support) hc'
Tactic: rw [Equiv.Perm.subtypePerm_on_cycleFactorsFinset hc]
-- 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
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
⊢ n < Fintype.card α
have apply : n < c.sum
Tactic: apply lt_of_lt_of_le _ hc
-- 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
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
⊢ n < c.sum
have rw : ∃ s ∈ c.ranges, n ∈ s
Tactic: rw [← mem_mem_ranges_iff_lt_sum]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (hypothesis)
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
⊢ ∃ (o : List (List α)), map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o
have hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
Tactic: have hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α := by
    intro l hl n hn
    apply lt_of_lt_of_le _ hc
    rw [← mem_mem_ranges_iff_lt_sum]
    exact ⟨l, hl, hn⟩
-- 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
a : List ℕ
ha : a ∈ c.ranges
| a
have rw : map id a
Tactic: rw [← List.map_id a]
-- 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
a : List ℕ
ha : a ∈ c.ranges
⊢ map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = a
have conv_rhs : map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a sorry) = map id a
Tactic: conv_rhs => rw [← List.map_id a]
-- 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
a : List ℕ
ha : a ∈ c.ranges
⊢ map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a ⋯) = map id a
have rw : pmap (P := fun (a : ℕ) ↦ a < Fintype.card α)
    (fun (a : ℕ) (h : a < Fintype.card α) ↦ (Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift a h)) a sorry =
  map id a
Tactic: rw [List.map_pmap]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.PossibleTypes (hypothesis)
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
⊢ ∃ (o : List (List α)), map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o
have hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding : (a : Fin (Fintype.card α)) → ℕ) (klift' a sorry) = 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']
-- 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
⊢ ∃ (o : List (List α)), map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o
have 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)
Tactic: use l.map (List.map (Fintype.equivFin α).symm)
-- 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 ∧
    (∀ (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 : map (α := List α) length (map (map (⇑(Equiv.symm (Fintype.equivFin α)) : (a : Fin (Fintype.card α)) → α)) l) = c
Tactic: constructor