awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : ¬(f : (a : α) → α) ((f : (a : α) → α) x : α) = x
rw : #(swap x ((f : (a : α) → α) x) * f).support + 1 = #(insert x (f.support.erase x))
rw₁ : #(f.support \ {x}) + 1 = #(insert x (f.support.erase x))
rw₂ : #(f.support \ {x}) + 1 = #(f.support.erase x) + 1
rw₃ rw₄ : #(f.support.erase x) + 1 = #(f.support.erase x) + 1
⊢ #(swap x ((f : (a : α) → α) x) * f).support + 1 = #f.support

Tactic:
rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
            card_insert_of_notMem (notMem_erase _ _), sdiff_singleton_eq_erase]

Premises used: Iff.mpr, Finset.sdiff_singleton_eq_erase, Equiv.Perm.support_swap_mul_eq, Equiv.Perm.mem_support, Finset.card_insert_of_notMem, And.left, Finset.notMem_erase, Finset.insert_erase
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : ¬(f : (a : α) → α) ((f : (a : α) → α) x : α) = x
⊢ #(swap x ((f : (a : α) → α) x) * f).support + 1 = #f.support

Tactic:
have h : #(swap x (f x) * f).support + 1 = #f.support := by
          rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
            card_insert_of_notMem (notMem_erase _ _), sdiff_singleton_eq_erase]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : ¬(f : (a : α) → α) ((f : (a : α) → α) x : α) = x
h : #(swap x ((f : (a : α) → α) x) * f).support + 1 = #f.support
rw :
  -1 * -HPow.hPow (α := ℤˣ) (-1) #(swap x ((f : (a : α) → α) x) * f).support =
    -HPow.hPow (α := ℤˣ) (-1) (#(swap x ((f : (a : α) → α) x) * f).support + 1)
⊢ ((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f)) =
    -HPow.hPow (α := ℤˣ) (-1) #f.support

Tactic:
rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h]

Premises used: Ne.symm, Equiv.Perm.sign_mul, And.left, Equiv.Perm.IsCycle.swap_mul, Equiv.Perm.sign_swap
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : ¬(f : (a : α) → α) ((f : (a : α) → α) x : α) = x
h : #(swap x ((f : (a : α) → α) x) * f).support + 1 = #f.support
⊢ -1 * -HPow.hPow (α := ℤˣ) (-1) #(swap x ((f : (a : α) → α) x) * f).support =
    -HPow.hPow (α := ℤˣ) (-1) (#(swap x ((f : (a : α) → α) x) * f).support + 1)

Tactic:
simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one]

Premises used: pow_add, neg_neg, pow_one, neg_mul, mul_one, one_mul, mul_neg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
simp_rw : (f ^ n).support = f.support
⊢ ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x

Tactic:
simp_rw [← mem_support, ← Finset.ext_iff]

Premises used: Equiv.Perm.mem_support, Finset.ext_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ (f ^ n).support = f.support

Tactic:
(support_pow_le _ n).antisymm h2

Premises used: Equiv.Perm.support_pow_le, LE.le.antisymm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ (f ^ n).support = f.support

Tactic:
exact (support_pow_le _ n).antisymm h2

Premises used: Equiv.Perm.support_pow_le, LE.le.antisymm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x

Tactic:
have key : ∀ x : α, (f ^ n) x ≠ x ↔ f x ≠ x := by
    simp_rw [← mem_support, ← Finset.ext_iff]
    exact (support_pow_le _ n).antisymm h2
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
obtain :
  ∀ (x : α) (hx1 : (f ^ n : (a : α) → α) x ≠ x) (hx2 : ∀ ⦃y : α⦄, (f ^ n : (a : α) → α) y ≠ y → (f ^ n).SameCycle x y),
    f.IsCycle
⊢ f.IsCycle

Tactic:
obtain ⟨x, hx1, hx2⟩ := h1
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
x : α
hx1 : (f ^ n : (a : α) → α) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n : (a : α) → α) y ≠ y → (f ^ n).SameCycle x y
⊢ f.IsCycle

Tactic:
⟨x, (key x).mp hx1, fun y hy => ?_⟩

Premises used: Equiv.Perm.IsCycle, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
x : α
hx1 : (f ^ n : (a : α) → α) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n : (a : α) → α) y ≠ y → (f ^ n).SameCycle x y
refine : ∀ (y : α) (hy : (f : (a : α) → α) y ≠ y), f.SameCycle x y
⊢ f.IsCycle

Tactic:
refine ⟨x, (key x).mp hx1, fun y hy => ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
x : α
hx1 : (f ^ n : (a : α) → α) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n : (a : α) → α) y ≠ y → (f ^ n).SameCycle x y
y : α
hy : (f : (a : α) → α) y ≠ y
obtain : ∀ (i : ℤ), ((f ^ n) ^ i : (a : α) → α) x = y → f.SameCycle x y
⊢ f.SameCycle x y

Tactic:
obtain ⟨i, _⟩ := hx2 ((key y).mpr hy)

Premises used: Iff.mpr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
x : α
hx1 : (f ^ n : (a : α) → α) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n : (a : α) → α) y ≠ y → (f ^ n).SameCycle x y
y : α
hy : (f : (a : α) → α) y ≠ y
i : ℤ
h : ((f ^ n) ^ i : (a : α) → α) x = y
rwa rwa₁ rwa₂ rwa₃ : (HPow.hPow (β := ℤ) f (↑n : ℤ) ^ i : (a : α) → α) x = y
⊢ (f ^ ((↑n : ℤ) * i) : (a : α) → α) x = y

Tactic:
rwa [zpow_mul]

Premises used: zpow_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
x : α
hx1 : (f ^ n : (a : α) → α) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n : (a : α) → α) y ≠ y → (f ^ n).SameCycle x y
y : α
hy : (f : (a : α) → α) y ≠ y
i : ℤ
h : ((f ^ n) ^ i : (a : α) → α) x = y
⊢ f.SameCycle x y

Tactic:
exact ⟨n * i, by rwa [zpow_mul]⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℤ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
ofNat : ∀ (a : ℕ) (h1 : (f ^ Int.ofNat a).IsCycle) (h2 : f.support ⊆ (f ^ Int.ofNat a).support), f.IsCycle
negSucc : ∀ (a : ℕ) (h1 : (f ^ Int.negSucc a).IsCycle) (h2 : f.support ⊆ (f ^ Int.negSucc a).support), f.IsCycle
⊢ f.IsCycle

Tactic:
cases n
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
a : ℕ
h1 : (f ^ Int.ofNat a).IsCycle
h2 : f.support ⊆ (f ^ Int.ofNat a).support
⊢ f.IsCycle

Tactic:
h1.of_pow h2

Premises used: Equiv.Perm.IsCycle.of_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
a : ℕ
h1 : (f ^ Int.ofNat a).IsCycle
h2 : f.support ⊆ (f ^ Int.ofNat a).support
⊢ f.IsCycle

Tactic:
exact h1.of_pow h2

Premises used: Equiv.Perm.IsCycle.of_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
a : ℕ
h1 : (f ^ Int.negSucc a).IsCycle
h2 : f.support ⊆ (f ^ Int.negSucc a).support
⊢ (f ^ (a + 1))⁻¹.IsCycle

Tactic:
simp only [zpow_negSucc, Perm.support_inv] at h1 h2

Premises used: zpow_negSucc, Equiv.Perm.support_inv
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
a : ℕ
h1 : (f ^ Int.negSucc a).IsCycle
h2 : f.support ⊆ (f ^ Int.negSucc a).support
h1₁ : (f ^ (a + 1))⁻¹.IsCycle
⊢ f.support ⊆ (f ^ (a + 1)).support

Tactic:
simp only [zpow_negSucc, Perm.support_inv] at h1 h2

Premises used: zpow_negSucc, Equiv.Perm.support_inv
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
a : ℕ
h1 : (f ^ (a + 1))⁻¹.IsCycle
h2 : f.support ⊆ (f ^ (a + 1)).support
⊢ f.IsCycle

Tactic:
exact (inv_inv (f ^ _) ▸ h1.inv).of_pow h2
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
l : List (Perm β)
h1 : ∀ f ∈ l, f.IsCycle
h2 : List.Pairwise Disjoint l
⊢ l.Nodup

Tactic:
nodup_of_pairwise_disjoint (fun h => (h1 1 h).ne_one rfl) h2

Premises used: Equiv.Perm.nodup_of_pairwise_disjoint, Equiv.Perm.IsCycle.ne_one, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ f.support = g.support

Tactic:
le_antisymm h ?_

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
refine : g.support ≤ f.support
⊢ f.support = g.support

Tactic:
refine le_antisymm h ?_

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
obtain :
  ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x), (∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y) → z ∈ f.support
⊢ z ∈ f.support

Tactic:
obtain ⟨x, hx, _⟩ := id hf

Premises used: id
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x : α
hx : (f : (a : α) → α) x ≠ x
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
rwa rwa₁ rwa₂ rwa₃ : (f : (a : α) → α) x ≠ x
⊢ (g : (a : α) → α) x ≠ x

Tactic:
rwa [← h' x (mem_support.mpr hx)]

Premises used: Iff.mpr, Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x : α
hx : (f : (a : α) → α) x ≠ x
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
⊢ (g : (a : α) → α) x ≠ x

Tactic:
have hx' : g x ≠ x := by rwa [← h' x (mem_support.mpr hx)]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x : α
hx : (f : (a : α) → α) x ≠ x
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
hx' : (g : (a : α) → α) x ≠ x
obtain : ∀ (m : ℕ) (hm : (g ^ m : (a : α) → α) x = z), z ∈ f.support
⊢ z ∈ f.support

Tactic:
obtain ⟨m, hm⟩ := hg.exists_pow_eq hx' (mem_support.mp hz)

Premises used: Equiv.Perm.IsCycle.exists_pow_eq, Equiv.Perm.mem_support, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x_1 : α
hx_1 : (f : (a : α) → α) x_1 ≠ x_1
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x_1 y
hx' : (g : (a : α) → α) x_1 ≠ x_1
m : ℕ
hm : (g ^ m : (a : α) → α) x_1 = z
x : α
hx : x ∈ f.support ∩ g.support
⊢ Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)

Tactic:
h' x (mem_of_mem_inter_left hx)

Premises used: Finset.mem_of_mem_inter_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x_1 : α
hx_1 : (f : (a : α) → α) x_1 ≠ x_1
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x_1 y
hx' : (g : (a : α) → α) x_1 ≠ x_1
m : ℕ
hm : (g ^ m : (a : α) → α) x_1 = z
x : α
hx : x ∈ f.support ∩ g.support
⊢ Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)

Tactic:
exact h' x (mem_of_mem_inter_left hx)

Premises used: Finset.mem_of_mem_inter_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x : α
hx : (f : (a : α) → α) x ≠ x
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
hx' : (g : (a : α) → α) x ≠ x
m : ℕ
hm : (g ^ m : (a : α) → α) x = z
⊢ ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)

Tactic:
have h'' : ∀ x ∈ f.support ∩ g.support, f x = g x := by
      intro x hx
      exact h' x (mem_of_mem_inter_left hx)
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
z : α
hz : z ∈ g.support
x : α
hx : (f : (a : α) → α) x ≠ x
right : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
hx' : (g : (a : α) → α) x ≠ x
m : ℕ
hm : (g ^ m : (a : α) → α) x = z
h'' : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
rwa : Membership.mem (α := α) f.support ((g ^ m : (a : α) → α) x : α)
rwa₁ : Membership.mem (α := α) f.support ((f ^ m : (a : α) → α) x : α)
rwa₂ : x ∈ f.support
rwa₃ rwa₄ rwa₅ rwa₆ : (f : (a : α) → α) x ≠ x
⊢ z ∈ f.support

Tactic:
rwa [← hm, ←
      pow_eq_on_of_mem_support h'' _ x
        (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
      pow_apply_mem_support, mem_support]

Premises used: Iff.mpr, Equiv.Perm.pow_eq_on_of_mem_support, Equiv.Perm.mem_support, Equiv.Perm.pow_apply_mem_support, Finset.mem_inter_of_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ f.support = g.support

Tactic:
have : f.support = g.support := by
    refine le_antisymm h ?_
    intro z hz
    obtain ⟨x, hx, _⟩ := id hf
    have hx' : g x ≠ x := by rwa [← h' x (mem_support.mpr hx)]
    obtain ⟨m, hm⟩ := hg.exists_pow_eq hx' (mem_support.mp hz)
    have h'' : ∀ x ∈ f.support ∩ g.support, f x = g x := by
      intro x hx
      exact h' x (mem_of_mem_inter_left hx)
    rwa [← hm, ←
      pow_eq_on_of_mem_support h'' _ x
        (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
      pow_apply_mem_support, mem_support]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
this : f.support = g.support
⊢ f = g

Tactic:
Equiv.Perm.support_congr h ?_

Premises used: Equiv.Perm.support_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
this : f.support = g.support
refine : ∀ x ∈ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ f = g

Tactic:
refine Equiv.Perm.support_congr h ?_

Premises used: Equiv.Perm.support_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
this : f.support = g.support
⊢ ∀ x ∈ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)

Tactic:
simpa [← this] using h'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
rwa : (g : (a : α) → α) x ≠ x
rwa₁ : (f : (a : α) → α) x ≠ x
rwa₂ rwa₃ rwa₄ rwa₅ : x ∈ f.support
⊢ x ∈ g.support

Tactic:
rwa [mem_support, ← hx, ← mem_support]

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
⊢ x ∈ g.support

Tactic:
have hx'' : x ∈ g.support := by rwa [mem_support, ← hx, ← mem_support]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
y : α
hy : y ∈ f.support
obtain :
  ∀ (k : ℕ) (hy : Membership.mem (α := α) f.support ((f ^ k : (a : α) → α) x : α)),
    Membership.mem (α := α) g.support ((f ^ k : (a : α) → α) x : α)
⊢ y ∈ g.support

Tactic:
obtain ⟨k, rfl⟩ := hf.exists_pow_eq (mem_support.mp hx') (mem_support.mp hy)

Premises used: Equiv.Perm.IsCycle.exists_pow_eq, Equiv.Perm.mem_support, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
k : ℕ
hy : Membership.mem (α := α) f.support ((f ^ k : (a : α) → α) x : α)
rwa : Membership.mem (α := α) g.support ((g ^ k : (a : α) → α) x : α)
rwa₁ rwa₂ rwa₃ rwa₄ : x ∈ g.support
⊢ Membership.mem (α := α) g.support ((f ^ k : (a : α) → α) x : α)

Tactic:
rwa [pow_eq_on_of_mem_support h _ _ (mem_inter_of_mem hx' hx''), pow_apply_mem_support]

Premises used: Equiv.Perm.pow_eq_on_of_mem_support, Equiv.Perm.pow_apply_mem_support, Finset.mem_inter_of_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
⊢ f.support ⊆ g.support

Tactic:
have : f.support ⊆ g.support := by
    intro y hy
    obtain ⟨k, rfl⟩ := hf.exists_pow_eq (mem_support.mp hx') (mem_support.mp hy)
    rwa [pow_eq_on_of_mem_support h _ _ (mem_inter_of_mem hx' hx''), pow_apply_mem_support]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
⊢ ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)

Tactic:
rw [inter_eq_left.mpr this] at h

Premises used: Iff.mpr, Finset.inter_eq_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
h₁ : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)

Tactic:
rw [inter_eq_left.mpr this] at h

Premises used: Iff.mpr, Finset.inter_eq_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
h₁ : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx₁ : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ x ∈ f.support

Tactic:
rw [inter_eq_left.mpr this] at h

Premises used: Iff.mpr, Finset.inter_eq_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
h₁ : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx₁ : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx'₁ : x ∈ f.support
⊢ x ∈ g.support

Tactic:
rw [inter_eq_left.mpr this] at h

Premises used: Iff.mpr, Finset.inter_eq_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
h₁ : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx₁ : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx'₁ : x ∈ f.support
hx''₁ : x ∈ g.support
⊢ f.support ⊆ g.support

Tactic:
rw [inter_eq_left.mpr this] at h

Premises used: Iff.mpr, Finset.inter_eq_left