awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hx : (f : (a : α) → α) x = x
k : ℤ
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) f 1 : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
have neg : x = (f ^ k : (a : α) → α) x
Tactic: rw [pow_apply_eq_self_of_apply_eq_self hx, zpow_apply_eq_self_of_apply_eq_self hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hx : (f : (a : α) → α) x = x
k : ℤ
neg : x = (f ^ k : (a : α) → α) x
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) f 1 : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
have neg₁ : x = x
Tactic: rw [pow_apply_eq_self_of_apply_eq_self hx, zpow_apply_eq_self_of_apply_eq_self hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
⊢ Eq (α := α) ((g ^ m : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α) ↔
    m % (↑(#(g.cycleOf x).support) : ℤ) = n % (↑(#(g.cycleOf x).support) : ℤ)
have rw : Eq (α := α) ((g ^ m : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α) ↔ (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0
Tactic: rw [Int.emod_eq_emod_iff_emod_sub_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
| Eq (α := α) ((g ^ m : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α)
have rw : Eq (α := α) ((g ^ n * g ^ (m - n) : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α)
Tactic: rw [← Int.sub_add_cancel m n, Int.add_comm, zpow_add]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
⊢ Eq (α := α) ((g ^ m : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α) ↔
    (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0
have conv_lhs : Eq (α := α) ((g ^ n * g ^ (m - n) : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α) ↔
  (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0
Tactic: conv_lhs => rw [← Int.sub_add_cancel m n, Int.add_comm, zpow_add]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
⊢ Eq (α := α) ((g ^ n * g ^ (m - n) : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α) ↔
    (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0
have simp : (g ^ (m - n) : (a : α) → α) x = x ↔ (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0
Tactic: simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
⊢ (g ^ (m - n) : (a : α) → α) x = x ↔ (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0
have rw : (g ^ (m - n) : (a : α) → α) x = x ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
Tactic: rw [← Int.dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
⊢ (g ^ (m - n) : (a : α) → α) x = x ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
have rw : (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0 ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
Tactic: rw [← cycleOf_zpow_apply_self g x, cycle_zpow_mem_support_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
rw : (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0 ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
⊢ (g ^ (m - n) : (a : α) → α) x = x ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
have hg : (g.cycleOf x).IsCycle
Tactic: rw [← cycleOf_zpow_apply_self g x, cycle_zpow_mem_support_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
rw : (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0 ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
hg : (g.cycleOf x).IsCycle
⊢ (g ^ (m - n) : (a : α) → α) x = x ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
have hx₁ : (g.cycleOf x : (a : α) → α) x ≠ x
Tactic: rw [← cycleOf_zpow_apply_self g x, cycle_zpow_mem_support_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
⊢ (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0 ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
have rw : (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
Tactic: rw [← Int.dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
⊢ List.prod [] = g ∧
    (∀ (g' : Perm α), Membership.mem (γ := List (Perm α)) [] g' → g'.IsCycle) ∧
      List.Pairwise.{u_2} (α := Perm α) Disjoint []
have simp : ∀ (hg : ∀ {x : α}, (g : (a : α) → α) x = x), 1 = g
Tactic: simp only [imp_false, List.Pairwise.nil, List.not_mem_nil, forall_const, and_true,
          forall_prop_of_false, Classical.not_not, not_false_iff, List.prod_nil] at *
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, (g : (a : α) → α) x = x
⊢ 1 = g
have H : ∀ (x : α), Eq (α := α) ((1 : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
⊢ List.prod [] = g ∧
    (∀ (g' : Perm α), Membership.mem (γ := List (Perm α)) [] g' → g'.IsCycle) ∧
      List.Pairwise.{u_2} (α := Perm α) Disjoint []
have simp : ∀ (hg : ∀ {x : α}, (g : (a : α) → α) x = x), 1 = g
Tactic: { simp only [imp_false, List.Pairwise.nil, List.not_mem_nil, forall_const, and_true,
          forall_prop_of_false, Classical.not_not, not_false_iff, List.prod_nil] at *
        ext
        simp [*]}
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
simp : ∀ (hg : ∀ {x : α}, (g : (a : α) → α) x = x), 1 = g
⊢ List.prod [] = g ∧
    (∀ (g' : Perm α), Membership.mem (γ := List (Perm α)) [] g' → g'.IsCycle) ∧
      List.Pairwise.{u_2} (α := Perm α) Disjoint []
have H : ∀ (hg : ∀ {x : α}, (g : (a : α) → α) x = x) (x : α), Eq (α := α) ((1 : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
Tactic: { simp only [imp_false, List.Pairwise.nil, List.not_mem_nil, forall_const, and_true,
          forall_prop_of_false, Classical.not_not, not_false_iff, List.prod_nil] at *
        ext
        simp [*]}
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
⊢ ∀ {x_1 : α}, ((f.cycleOf x)⁻¹ * g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ l
have rw : ∀ {x_1 : α}, ((g.cycleOf x)⁻¹ * g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ l
Tactic: rw [hfg hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g : (a : α) → α) y ≠ y
h : y = x
⊢ False
have hy₁ : ¬Eq (α := α) ((g : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
Tactic: rw [h, mul_apply, Ne, inv_eq_iff_eq, cycleOf_apply_self] at hy
Cleared hypotheses: hy, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g : (a : α) → α) y ≠ y
h : (g : (a : α) → α) y = y
⊢ False
have hy₁ : ¬y = if g.SameCycle x y then (g : (a : α) → α) y else y
Tactic: rw [mul_apply, h, Ne, inv_eq_iff_eq, cycleOf_apply] at hy
Cleared hypotheses: hy, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬y = if g.SameCycle x y then (g : (a : α) → α) y else y
h : (g : (a : α) → α) y = y
⊢ False
have pos : g.SameCycle x y → ∀ (hy : ¬y = (g : (a : α) → α) y), False
Tactic: split_ifs at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h_1 : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬y = if g.SameCycle x y then (g : (a : α) → α) y else y
h : (g : (a : α) → α) y = y
pos : g.SameCycle x y → ∀ (hy : ¬y = (g : (a : α) → α) y), False
⊢ False
have neg : ¬g.SameCycle x y → ∀ (hy : ¬y = y), False
Tactic: split_ifs at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
⊢ ∀ {x_1 : α}, ((f.cycleOf x)⁻¹ * g : (a : α) → α) x_1 ≠ x_1 → f.cycleOf x_1 = ((f.cycleOf x)⁻¹ * g).cycleOf x_1
have rw : ∀ {x_1 : α}, ((g.cycleOf x)⁻¹ * g : (a : α) → α) x_1 ≠ x_1 → f.cycleOf x_1 = ((g.cycleOf x)⁻¹ * g).cycleOf x_1
Tactic: rw [hfg hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g : (a : α) → α) y ≠ y
⊢ f.cycleOf y = ((g.cycleOf x)⁻¹ * g).cycleOf y
have hy₁ : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
Tactic: simp [symm_apply_eq, cycleOf_apply, eq_comm (a := g y)] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
⊢ f.cycleOf y = ((g.cycleOf x)⁻¹ * g).cycleOf y
have rw : g.cycleOf y * ((g.cycleOf x)⁻¹ * g)⁻¹.cycleOf y = 1
Tactic: rw [hfg (Ne.symm hy.right), ← mul_inv_eq_one (a := g.cycleOf y), cycleOf_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
⊢ g.cycleOf y * ((g.cycleOf x)⁻¹ * g)⁻¹.cycleOf y = 1
have simp_rw : g.cycleOf y * (g⁻¹ * (g.cycleOf x)⁻¹⁻¹).cycleOf y = 1
Tactic: simp_rw [mul_inv_rev]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
⊢ g.cycleOf y * (g⁻¹ * (g.cycleOf x)⁻¹⁻¹).cycleOf y = 1
have h₁ : Commute g⁻¹ (g.cycleOf x)
Tactic: rw [inv_inv, cycleOf_mul_of_apply_right_eq_self, ← cycleOf_inv, mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
h₁ : Commute g⁻¹ (g.cycleOf x)
⊢ g.cycleOf y * (g⁻¹ * (g.cycleOf x)⁻¹⁻¹).cycleOf y = 1
have hx₁ : (g.cycleOf x : (a : α) → α) y = y
Tactic: rw [inv_inv, cycleOf_mul_of_apply_right_eq_self, ← cycleOf_inv, mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
⊢ Commute g⁻¹ (g.cycleOf x)
have h₁ : g * g.cycleOf x = g.cycleOf x * g
Tactic: rw [Commute.inv_left_iff, commute_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
⊢ g * g.cycleOf x = g.cycleOf x * g
have h₁ : ∀ (z : α), Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)
Tactic: ext z
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
z : α
⊢ Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)
have pos : ∀ (hz : g.SameCycle x z), Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)
Tactic: by_cases hz : SameCycle g x z
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = (g : (a : α) → α) y
z : α
pos :
  ∀ (hz : g.SameCycle x z), Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)
⊢ Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)
have neg : ∀ (hz : ¬g.SameCycle x z), Eq (α := α) ((g * g.cycleOf x : (a : α) → α) z : α) ((g.cycleOf x * g : (a : α) → α) z : α)
Tactic: by_cases hz : SameCycle g x z
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm : m.prod = (f.cycleOf x)⁻¹ * g ∧ (∀ g' ∈ m, g'.IsCycle) ∧ List.Pairwise Disjoint m
⊢ (f.cycleOf x :: m).prod = g ∧ (∀ g' ∈ f.cycleOf x :: m, g'.IsCycle) ∧ List.Pairwise Disjoint (f.cycleOf x :: m)
have hm₁ : m.prod = (f.cycleOf x)⁻¹ * g
Tactic: obtain ⟨hm₁, hm₂, hm₃⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm : m.prod = (f.cycleOf x)⁻¹ * g ∧ (∀ g' ∈ m, g'.IsCycle) ∧ List.Pairwise Disjoint m
hm₁ : m.prod = (f.cycleOf x)⁻¹ * g
⊢ (f.cycleOf x :: m).prod = g ∧ (∀ g' ∈ f.cycleOf x :: m, g'.IsCycle) ∧ List.Pairwise Disjoint (f.cycleOf x :: m)
have hm₂ : ∀ g' ∈ m, g'.IsCycle
Tactic: obtain ⟨hm₁, hm₂, hm₃⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm : m.prod = (f.cycleOf x)⁻¹ * g ∧ (∀ g' ∈ m, g'.IsCycle) ∧ List.Pairwise Disjoint m
hm₁ : m.prod = (f.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
⊢ (f.cycleOf x :: m).prod = g ∧ (∀ g' ∈ f.cycleOf x :: m, g'.IsCycle) ∧ List.Pairwise Disjoint (f.cycleOf x :: m)
have hm₃ : List.Pairwise Disjoint m
Tactic: obtain ⟨hm₁, hm₂, hm₃⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (f.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
⊢ (f.cycleOf x :: m).prod = g ∧ (∀ g' ∈ f.cycleOf x :: m, g'.IsCycle) ∧ List.Pairwise Disjoint (f.cycleOf x :: m)
have rw : ∀ (hm₁ : m.prod = (g.cycleOf x)⁻¹ * g) (hm₂ : ∀ g' ∈ m, g'.IsCycle) (hm₃ : List.Pairwise Disjoint m),
  (g.cycleOf x :: m).prod = g ∧ (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ List.Pairwise Disjoint (g.cycleOf x :: m)
Tactic: rw [hfg hx] at hm₁ ⊢
Cleared hypotheses: hm₁, hm₂, hm₃
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
⊢ (g.cycleOf x :: m).prod = g ∧ (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ List.Pairwise Disjoint (g.cycleOf x :: m)
have rw : (g.cycleOf x :: m).prod = g ∧
  (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ (∀ a' ∈ m, (g.cycleOf x).Disjoint a') ∧ List.Pairwise Disjoint m
Tactic: rw [List.pairwise_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
⊢ (g.cycleOf x :: m).prod = g ∧
    (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ (∀ a' ∈ m, (g.cycleOf x).Disjoint a') ∧ List.Pairwise Disjoint m
have refine_1 : (g.cycleOf x :: m).prod = g
Tactic: refine ⟨?_, fun g' hg' ↦ ?_, fun g' hg' y ↦ ?_, hm₃⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
refine_1 : (g.cycleOf x :: m).prod = g
⊢ (g.cycleOf x :: m).prod = g ∧
    (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ (∀ a' ∈ m, (g.cycleOf x).Disjoint a') ∧ List.Pairwise Disjoint m
have refine_2 : ∀ (g' : Perm α) (hg' : g' ∈ g.cycleOf x :: m), g'.IsCycle
Tactic: refine ⟨?_, fun g' hg' ↦ ?_, fun g' hg' y ↦ ?_, hm₃⟩