awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
⊢ Ne.{u_3 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g : (a : α) → α) a)) : β) (↑((f : (a : α) → Subtype p) a) : β)

Tactic:
Subtype.coe_injective.ne (f.injective.ne ha)

Premises used: Function.Injective.ne, Subtype.coe_injective, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
⊢ Ne.{u_3 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g : (a : α) → α) a)) : β) (↑((f : (a : α) → Subtype p) a) : β)

Tactic:
exact Subtype.coe_injective.ne (f.injective.ne ha)

Premises used: Function.Injective.ne, Subtype.coe_injective, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b
rw : b = (↑(Subtype.mk (p := p) b ⋯) : β)
rw₁ rw₂ : b = b
⊢ b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)

Tactic:
rw [apply_symm_apply, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Equiv.apply_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b
⊢ b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)

Tactic:
have h : b = f (f.symm ⟨b, of_not_not <| hb ∘ extendDomain_apply_not_subtype _ _⟩) := by
    rw [apply_symm_apply, Subtype.coe_mk]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b
h : b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)
refine_2 :
  ∀
    (hb_1 :
      Ne (α := β)
        ((g.extendDomain (p := p) f : (a : β) → β)
            (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β) :
          β)
        ((↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β) : β))
    (h : b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)),
    (g.extendDomain (p := p) f).SameCycle (↑((f : (a : α) → Subtype p) a) : β)
      (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)
⊢ (g.extendDomain (p := p) f).SameCycle (↑((f : (a : α) → Subtype p) a) : β) b

Tactic:
rw [h] at hb ⊢
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
b : β
hb_1 : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b
hb :
  Ne (α := β)
    ((g.extendDomain (p := p) f : (a : β) → β)
        (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β) :
      β)
    ((↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β) : β)
h : b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)
⊢ Ne (α := α) ((g : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯) : α)

Tactic:
simp only [extendDomain_apply_image, Subtype.coe_injective.ne_iff, f.injective.ne_iff] at hb

Premises used: Equiv.Perm.extendDomain_apply_image, Function.Injective.ne_iff, Subtype.coe_injective, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
b : β
hb_1 : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b
h : b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)
hb :
  Ne (α := α) ((g : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯) : α)
⊢ (g.extendDomain (p := p) f).SameCycle (↑((f : (a : α) → Subtype p) a) : β)
    (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)

Tactic:
(ha' hb).extendDomain

Premises used: Equiv.Perm.SameCycle.extendDomain
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
b : β
hb_1 : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b
h : b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)
hb :
  Ne (α := α) ((g : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯) : α)
⊢ (g.extendDomain (p := p) f).SameCycle (↑((f : (a : α) → Subtype p) a) : β)
    (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)

Tactic:
exact (ha' hb).extendDomain

Premises used: Equiv.Perm.SameCycle.extendDomain
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
hx : (f : (a : α) → α) x ≠ x
hf : f.IsCycle
y : α
h : f.SameCycle x y
hy : (f : (a : α) → α) y = y
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
⊢ x = y

Tactic:
rw [← zpow_apply_eq_self_of_apply_eq_self hy i, (f ^ i).injective.eq_iff] at hi

Premises used: Function.Injective.eq_iff, Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self, HPow.hPow, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
hx : (f : (a : α) → α) x ≠ x
hf : f.IsCycle
y : α
h : f.SameCycle x y
hy : (f : (a : α) → α) y = y
i : ℤ
hi : x = y
rw : (f : (a : α) → α) y = y
rw₁ rw₂ : y = y
⊢ (f : (a : α) → α) x = x

Tactic:
rw [hi, hy]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
let : ∀ (n : ℤ) (hn : (f ^ n : (a : α) → α) x = y), ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y
⊢ ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y

Tactic:
let ⟨n, hn⟩ := hf.exists_zpow_eq hx hy
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
n : ℤ
hn : (f ^ n : (a : α) → α) x = y
⊢ 0 ≤ n % (↑(orderOf f) : ℤ)

Tactic:
have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
n : ℤ
hn : (f ^ n : (a : α) → α) x = y
this : 0 ≤ n % (↑(orderOf f) : ℤ)
rwa : (HPow.hPow (β := ℤ) f (↑(n % (↑(orderOf f) : ℤ)).toNat : ℤ) : (a : α) → α) x = y
rwa₁ : (f ^ (n % (↑(orderOf f) : ℤ)) : (a : α) → α) x = y
rwa₂ rwa₃ rwa₄ rwa₅ : (f ^ n : (a : α) → α) x = y
⊢ (f ^ (n % (↑(orderOf f) : ℤ)).toNat : (a : α) → α) x = y

Tactic:
rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]

Premises used: zpow_natCast, zpow_mod_orderOf, Int.toNat_of_nonneg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
n : ℤ
hn : (f ^ n : (a : α) → α) x = y
rwa rwa₁ rwa₂ : ∀ (this : 0 ≤ n % (↑(orderOf f) : ℤ)), (f ^ (n % (↑(orderOf f) : ℤ)).toNat : (a : α) → α) x = y
⊢ (f ^ (n % (↑(orderOf f) : ℤ)).toNat : (a : α) → α) x = y

Tactic:
{have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
         rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]}

Premises used: zpow_natCast, zpow_mod_orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
n : ℤ
hn : (f ^ n : (a : α) → α) x = y
⊢ ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y

Tactic:
exact
      ⟨(n % orderOf f).toNat, by
        {have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
         rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]}⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
n : ℤ
hn : (f ^ n : (a : α) → α) x = y
⊢ ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y

Tactic:
classical exact
      ⟨(n % orderOf f).toNat, by
        {have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
         rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]}⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy rwa rwa₁ rwa₂ rwa₃ : x ≠ y
⊢ (swap x y : (a : α) → α) y ≠ y

Tactic:
rwa [swap_apply_right]

Premises used: Equiv.swap_apply_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
rw : (if y = x then y else if y = y then x else y) = a
⊢ (HPow.hPow (β := ℤ) (swap x y) 1 : (a : α) → α) y = a

Tactic:
rw [zpow_one, swap_apply_def]

Premises used: zpow_one, Equiv.swap_apply_def
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
pos : y = x → a = x → ∀ (ha : y ≠ a), y = a
pos₁ : y = x → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
neg : y = x → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), y = a
pos₂ : ¬y = x → y = y → a = x → ∀ (ha : y ≠ a), x = a
pos₃ : ¬y = x → y = y → ¬a = x → a = y → ∀ (ha : x ≠ a), x = a
neg₁ : ¬y = x → y = y → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), x = a
pos₄ : ¬y = x → ¬y = y → a = x → ∀ (ha : y ≠ a), y = a
pos₅ : ¬y = x → ¬y = y → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
neg₂ : ¬y = x → ¬y = y → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), y = a
⊢ (if y = x then y else if y = y then x else y) = a

Tactic:
split_ifs at *
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h : y = x
h_1 : a = x
ha : y ≠ a
⊢ y = a

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h : y = x
h_1 : ¬a = x
h_2 : a = y
ha : x ≠ a
⊢ y = a

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h : y = x
h_1 : ¬a = x
h_2 : ¬a = y
ha : a ≠ a
⊢ y = a

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h : ¬y = x
h_1 : y = y
h_2 : a = x
ha : y ≠ a
⊢ x = a

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h : ¬y = x
h_1 : y = y
h_2 : ¬a = x
h_3 : a = y
ha : x ≠ a
⊢ x = a

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h : ¬y = x
h_1 : y = y
h_2 : ¬a = x
h_3 : ¬a = y
ha : a ≠ a
⊢ x = a

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h : ¬y = x
h_1 : ¬y = y
h_2 : a = x
ha : y ≠ a
⊢ y = a

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h : ¬y = x
h_1 : ¬y = y
h_2 : ¬a = x
h_3 : a = y
ha : x ≠ a
⊢ y = a

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h : ¬y = x
h_1 : ¬y = y
h_2 : ¬a = x
h_3 : ¬a = y
ha : a ≠ a
⊢ y = a

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
hxy : x ≠ y
⊢ (swap x y).IsCycle

Tactic:
isCycle_swap hxy

Premises used: Equiv.Perm.isCycle_swap
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
hxy : x ≠ y
⊢ (swap x y).IsCycle

Tactic:
exact isCycle_swap hxy

Premises used: Equiv.Perm.isCycle_swap
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
mp : (swap a b).IsSwap → a ≠ b
mpr : a ≠ b → (swap a b).IsSwap
⊢ (swap a b).IsSwap ↔ a ≠ b

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
h : (swap a b).IsSwap
hab : a = b
mp : swap a b = 1
⊢ False

Tactic:
apply h.isCycle.ne_one

Premises used: Equiv.Perm.IsCycle.ne_one, Equiv.Perm.IsSwap.isCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
h : (swap a b).IsSwap
hab : a = b
⊢ swap a b = 1

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
h : a ≠ b
w w₁ : α
h₁ : a ≠ b ∧ swap a b = swap a b
⊢ (swap a b).IsSwap

Tactic:
use a, b
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
h : f.IsCycle
⊢ 2 ≤ #f.support

Tactic:
two_le_card_support_of_ne_one h.ne_one

Premises used: Equiv.Perm.two_le_card_support_of_ne_one, Equiv.Perm.IsCycle.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)
obtain :
  ∀ (n : ℤ),
    ((↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ (↑(Subgroup.zpowers σ) : Set (Perm α))) ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
            Perm α) :
          (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) ∈
      σ.support
⊢ Membership.mem (α := α) σ.support
    (((↑τ : Perm α) : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
      α)

Tactic:
obtain ⟨τ, n, rfl⟩ := τ

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℤ
rw :
  (σ : (a : α) → α)
      (Classical.choose (p := fun (x : α) ↦
        (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) ≠
    Classical.choose (p := fun (x : α) ↦ (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y)
      hσ
⊢ ((↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ (↑(Subgroup.zpowers σ) : Set (Perm α))) ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
          Perm α) :
        (a : α) → α)
      (Classical.choose (p := fun (x : α) ↦
        (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) ∈
    σ.support

Tactic:
rw [Subtype.coe_mk, zpow_apply_mem_support, mem_support]

Premises used: Subtype.coe_mk, Equiv.Perm.mem_support, Equiv.Perm.zpow_apply_mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℤ
⊢ (σ : (a : α) → α)
      (Classical.choose (p := fun (x : α) ↦
        (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) ≠
    Classical.choose (p := fun (x : α) ↦ (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y)
      hσ

Tactic:
(Classical.choose_spec hσ).1

Premises used: Classical.choose_spec, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℤ
⊢ (σ : (a : α) → α)
      (Classical.choose (p := fun (x : α) ↦
        (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) ≠
    Classical.choose (p := fun (x : α) ↦ (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y)
      hσ

Tactic:
exact (Classical.choose_spec hσ).1

Premises used: Classical.choose_spec, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
left :
  Injective (β := ↥σ.support) fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
      (((↑τ : Perm α) : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
      ⋯
right :
  Surjective (β := ↥σ.support) fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
      (((↑τ : Perm α) : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
      ⋯
⊢ Bijective (β := ↥σ.support) fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
      (((↑τ : Perm α) : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
      ⋯

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  Eq.{u_2 + 1} (α := ↥σ.support)
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) m) ⋯))
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) n) ⋯))
left :
  ∀ (y : α),
    Eq (α := α)
      (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                  ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
              Perm α) :
            (a : α) → α)
          y :
        α)
      (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                  ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
              Perm α) :
            (a : α) → α)
          y :
        α)
⊢ Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
      ((fun (x : ℤ) ↦ σ ^ x) m) ⋯ =
    Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
      ((fun (x : ℤ) ↦ σ ^ x) n) ⋯

Tactic:
ext y
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  Eq.{u_2 + 1} (α := ↥σ.support)
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) m) ⋯))
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) n) ⋯))
y : α
pos :
  ∀ (hy : (σ : (a : α) → α) y = y),
    Eq (α := α)
      (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                  ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
              Perm α) :
            (a : α) → α)
          y :
        α)
      (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                  ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
              Perm α) :
            (a : α) → α)
          y :
        α)
neg :
  ∀ (hy : ¬(σ : (a : α) → α) y = y),
    Eq (α := α)
      (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                  ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
              Perm α) :
            (a : α) → α)
          y :
        α)
      (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                  ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
              Perm α) :
            (a : α) → α)
          y :
        α)
⊢ Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)

Tactic:
by_cases hy : σ y = y

Premises used: DFunLike.coe