awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
hx : l.length < 2
⊢ l.formPerm = 1
have intro : l.length ≤ 1
Tactic: rw [formPerm_eq_one_iff _ hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
⊢ x ∈ l
have intro : x ∈ l.toFinset
Tactic: rw [← mem_toFinset]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
⊢ x ∈ l.toFinset
have intro : x ∈ l.formPerm.support
Tactic: refine support_formPerm_le l ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ ∃! s : { s : Cycle α // s.Nodup }, (↑s : Cycle α).formPerm ⋯ = f
have obtain : ∀ (s : Cycle α) (hs : s.Nodup) (hf : (s.formPerm hs).IsCycle)
  (hs' : ∀ (y : Cycle α), (fun (s_1 : Cycle α) ↦ ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s),
  ∃! s_1 : { s : Cycle α // s.Nodup }, (↑s_1 : Cycle α).formPerm sorry = s.formPerm hs
Tactic: obtain ⟨s, ⟨hs, rfl⟩, hs'⟩ := hf.existsUnique_cycle
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun (s_1 : Cycle α) ↦ ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
⊢ ∃! s_1 : { s : Cycle α // s.Nodup }, (↑s_1 : Cycle α).formPerm ⋯ = s.formPerm hs
have refine : ∀ (y : { s : Cycle α // s.Nodup }),
  (fun (s_1 : { s : Cycle α // s.Nodup }) ↦ (↑s_1 : Cycle α).formPerm sorry = s.formPerm hs) y →
    y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hs
Tactic: refine ⟨⟨s, hs⟩, rfl, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ ∃! s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑s : Cycle α).formPerm ⋯ = f
have obtain : ∀ (s : Cycle α) (hn : s.Nodup) (hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm sorry = f)
  (hs' :
    ∀ (y : { s : Cycle α // s.Nodup }),
      (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm sorry = f) y →
        y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn),
  ∃! s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑s : Cycle α).formPerm sorry = f
Tactic: obtain ⟨⟨s, hn⟩, hs, hs'⟩ := hf.existsUnique_cycle_subtype
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
⊢ ∃! s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑s : Cycle α).formPerm ⋯ = f
have refine_1 : s.Nontrivial
Tactic: refine ⟨⟨s, hn, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
refine_1 : s.Nontrivial
⊢ ∃! s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑s : Cycle α).formPerm ⋯ = f
have refine_2 : (fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦ (↑s : Cycle α).formPerm sorry = f)
  (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) s sorry)
Tactic: refine ⟨⟨s, hn, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
refine_1 : s.Nontrivial
refine_2 :
  (fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦ (↑s : Cycle α).formPerm ⋯ = f)
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) s ⋯)
⊢ ∃! s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑s : Cycle α).formPerm ⋯ = f
have refine_3 : ∀ (y : { s : Cycle α // s.Nodup ∧ s.Nontrivial }),
  (fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦ (↑s : Cycle α).formPerm sorry = f) y →
    y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) s sorry
Tactic: refine ⟨⟨s, hn, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
⊢ s.Nontrivial
have refine_1 : ¬s.Subsingleton
Tactic: rw [hn.nontrivial_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
⊢ ¬s.Subsingleton
have hf₁ : ((↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm sorry).IsCycle
Tactic: subst f
Cleared hypotheses: f, hf, hs, hs'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
hf₁ : ((↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯).IsCycle
⊢ ¬s.Subsingleton
have hs'₁ : ∀ (y : { s : Cycle α // s.Nodup }),
  (fun (s_1 : { s : Cycle α // s.Nodup }) ↦
        (↑s_1 : Cycle α).formPerm sorry = (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm sorry)
      y →
    y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
Tactic: subst f
Cleared hypotheses: f, hf, hs, hs'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
s : Cycle α
hn : s.Nodup
hf : ((↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯).IsCycle
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s_1 : { s : Cycle α // s.Nodup }) ↦
          (↑s_1 : Cycle α).formPerm ⋯ = (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯)
        y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
H : s.Subsingleton
⊢ False
have refine_1 : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm sorry = 1
Tactic: refine hf.ne_one ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : { s : Cycle α // s.Nodup ∧ s.Nontrivial } → { f : Perm α // f.IsCycle } :=
  fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
    Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯
⊢ Function.Bijective f
have rw : ∀ (b : { f : Perm α // f.IsCycle }), ∃! a : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, f a = b
Tactic: rw [Function.bijective_iff_existsUnique]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f_1 : { s : Cycle α // s.Nodup ∧ s.Nontrivial } → { f : Perm α // f.IsCycle } :=
  fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
    Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯
f : Perm α
hf : f.IsCycle
⊢ ∃! a : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, f_1 a = Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) f hf
have simp : ∃! a : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑(f_1 a) : Perm α) = f
Tactic: simp only [Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) y : α) (if f.SameCycle x y then (f : (a : α) → α) y else y : α)
have dsimp : Eq (α := α)
  ((((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
            (f.subtypePerm (p := f.SameCycle x) sorry) :
          Perm α) :
        (a : α) → α)
      y :
    α)
  (if f.SameCycle x y then (f : (a : α) → α) y else y : α)
Tactic: dsimp only [cycleOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
              (f.subtypePerm (p := f.SameCycle x) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (if f.SameCycle x y then (f : (a : α) → α) y else y : α)
have pos : ∀ (h : f.SameCycle x y),
  Eq (α := α)
    ((((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
              (f.subtypePerm (p := f.SameCycle x) sorry) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    ((f : (a : α) → α) y : α)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
pos :
  ∀ (h : f.SameCycle x y),
    Eq (α := α)
      ((((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
                (f.subtypePerm (p := f.SameCycle x) ⋯) :
              Perm α) :
            (a : α) → α)
          y :
        α)
      ((f : (a : α) → α) y : α)
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
              (f.subtypePerm (p := f.SameCycle x) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (if f.SameCycle x y then (f : (a : α) → α) y else y : α)
have neg : ∀ (h : ¬f.SameCycle x y),
  (((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
            (f.subtypePerm (p := f.SameCycle x) sorry) :
          Perm α) :
        (a : α) → α)
      y =
    y
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
⊢ Eq (α := α) (((f.cycleOf x)⁻¹ : (a : α) → α) y : α) ((f⁻¹.cycleOf x : (a : α) → α) y : α)
have rw : y =
  if f.SameCycle x (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y) then
    (f : (a : α) → α) (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y : α)
  else if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y
Tactic: rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
⊢ y =
    if f.SameCycle x (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y) then
      (f : (a : α) → α) (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y : α)
    else if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y
have pos : f⁻¹.SameCycle x y → f.SameCycle x ((f⁻¹ : (a : α) → α) y) → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
pos : f⁻¹.SameCycle x y → f.SameCycle x ((f⁻¹ : (a : α) → α) y) → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
⊢ y =
    if f.SameCycle x (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y) then
      (f : (a : α) → α) (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y : α)
    else if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y
have neg : f⁻¹.SameCycle x y → ¬f.SameCycle x ((f⁻¹ : (a : α) → α) y) → y = (f⁻¹ : (a : α) → α) y
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
pos : f⁻¹.SameCycle x y → f.SameCycle x ((f⁻¹ : (a : α) → α) y) → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
neg : f⁻¹.SameCycle x y → ¬f.SameCycle x ((f⁻¹ : (a : α) → α) y) → y = (f⁻¹ : (a : α) → α) y
⊢ y =
    if f.SameCycle x (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y) then
      (f : (a : α) → α) (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y : α)
    else if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y
have pos₁ : ¬f⁻¹.SameCycle x y → f.SameCycle x y → y = (f : (a : α) → α) y
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
pos : f⁻¹.SameCycle x y → f.SameCycle x ((f⁻¹ : (a : α) → α) y) → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
neg : f⁻¹.SameCycle x y → ¬f.SameCycle x ((f⁻¹ : (a : α) → α) y) → y = (f⁻¹ : (a : α) → α) y
pos₁ : ¬f⁻¹.SameCycle x y → f.SameCycle x y → y = (f : (a : α) → α) y
⊢ y =
    if f.SameCycle x (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y) then
      (f : (a : α) → α) (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y : α)
    else if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y
have neg₁ : ¬f⁻¹.SameCycle x y → ¬f.SameCycle x y → y = y
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
n : ℕ
hn : Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((f ^ (n + 1) : (a : α) → α) x : α)
have succ : f.SameCycle x ((f ^ n : (a : α) → α) x)
Tactic: rw [pow_succ', mul_apply, cycleOf_apply, hn, if_pos, pow_succ', mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
n : ℕ
⊢ Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have zero : Eq (α := α) ((HPow.hPow (β := ℕ) (f.cycleOf x) 0 : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
Tactic: induction n with
  | zero => rfl
  | succ n hn =>
    rw [pow_succ', mul_apply, cycleOf_apply, hn, if_pos, pow_succ', mul_apply]
    exact ⟨n, rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
n : ℕ
zero :
  Eq (α := α) ((HPow.hPow (β := ℕ) (f.cycleOf x) 0 : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have succ : ∀ (n : ℕ) (hn : Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)),
  Eq (α := α) ((f.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((f ^ (n + 1) : (a : α) → α) x : α)
Tactic: induction n with
  | zero => rfl
  | succ n hn =>
    rw [pow_succ', mul_apply, cycleOf_apply, hn, if_pos, pow_succ', mul_apply]
    exact ⟨n, rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ Eq (α := α) ((f.cycleOf x ^ Int.negSucc z : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
have negSucc : Eq (α := α) (((f.cycleOf x ^ (z + 1))⁻¹ : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
Tactic: rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℕ
negSucc : Eq (α := α) (((f.cycleOf x ^ (z + 1))⁻¹ : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x ^ Int.negSucc z : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
have negSucc₁ : Eq (α := α) (((f.cycleOf x)⁻¹ ^ (z + 1) : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
Tactic: rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℕ
negSucc : Eq (α := α) (((f.cycleOf x ^ (z + 1))⁻¹ : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₁ : Eq (α := α) (((f.cycleOf x)⁻¹ ^ (z + 1) : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x ^ Int.negSucc z : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
have negSucc₂ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
Tactic: rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℕ
negSucc : Eq (α := α) (((f.cycleOf x ^ (z + 1))⁻¹ : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₁ : Eq (α := α) (((f.cycleOf x)⁻¹ ^ (z + 1) : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₂ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x ^ Int.negSucc z : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
have negSucc₃ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) (((f ^ (z + 1))⁻¹ : (a : α) → α) x : α)
Tactic: rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℕ
negSucc : Eq (α := α) (((f.cycleOf x ^ (z + 1))⁻¹ : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₁ : Eq (α := α) (((f.cycleOf x)⁻¹ ^ (z + 1) : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₂ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₃ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) (((f ^ (z + 1))⁻¹ : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x ^ Int.negSucc z : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
have negSucc₄ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) ((f⁻¹ ^ (z + 1) : (a : α) → α) x : α)
Tactic: rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℕ
negSucc : Eq (α := α) (((f.cycleOf x ^ (z + 1))⁻¹ : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₁ : Eq (α := α) (((f.cycleOf x)⁻¹ ^ (z + 1) : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₂ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₃ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) (((f ^ (z + 1))⁻¹ : (a : α) → α) x : α)
negSucc₄ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) ((f⁻¹ ^ (z + 1) : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x ^ Int.negSucc z : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
have negSucc₅ : Eq (α := α) ((f⁻¹ ^ (z + 1) : (a : α) → α) x : α) ((f⁻¹ ^ (z + 1) : (a : α) → α) x : α)
Tactic: rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℤ
⊢ Eq (α := α) ((f.cycleOf x ^ z : (a : α) → α) x : α) ((f ^ z : (a : α) → α) x : α)
have ofNat : ∀ (z : ℕ), Eq (α := α) ((f.cycleOf x ^ Int.ofNat z : (a : α) → α) x : α) ((f ^ Int.ofNat z : (a : α) → α) x : α)
Tactic: cases z with
  | ofNat z => exact cycleOf_pow_apply_self f x z
  | negSucc z =>
    rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℤ
ofNat : ∀ (z : ℕ), Eq (α := α) ((f.cycleOf x ^ Int.ofNat z : (a : α) → α) x : α) ((f ^ Int.ofNat z : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x ^ z : (a : α) → α) x : α) ((f ^ z : (a : α) → α) x : α)
have negSucc : ∀ (z : ℕ), Eq (α := α) ((f.cycleOf x ^ Int.negSucc z : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
Tactic: cases z with
  | ofNat z => exact cycleOf_pow_apply_self f x z
  | negSucc z =>
    rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
h : f.SameCycle x y
⊢ f.cycleOf x = f.cycleOf y
have H : ∀ (z : α), Eq (α := α) ((f.cycleOf x : (a : α) → α) z : α) ((f.cycleOf y : (a : α) → α) z : α)
Tactic: ext z
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) z : α) ((f.cycleOf y : (a : α) → α) z : α)
have H : Eq (α := α) (if f.SameCycle x z then (f : (a : α) → α) z else z : α) ((f.cycleOf y : (a : α) → α) z : α)
Tactic: rw [Equiv.Perm.cycleOf_apply]