ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f g : Perm α✝
x y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℤ
⊢ ∀ {b x : α} {f : Perm α},
    ↑(swap x (↑f x) * f) b ≠ b → ↑(f ^ n) (↑f x) = b → ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f g : Perm α✝
x y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (n : ℤ) {b x : α} {f : Perm α},
    ↑(swap x (↑f x) * f) b ≠ b → ↑(f ^ n) (↑f x) = b → ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
intro n
case ofNat
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f g : Perm α✝
x y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
⊢ ∀ {b x : α} {f : Perm α},
    ↑(swap x (↑f x) * f) b ≠ b → ↑(f ^ Int.ofNat n) (↑f x) = b → ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b

case negSucc
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f g : Perm α✝
x y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
⊢ ∀ {b x : α} {f : Perm α},
    ↑(swap x (↑f x) * f) b ≠ b → ↑(f ^ Int.negSucc n) (↑f x) = b → ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f g : Perm α✝
x y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℤ
⊢ ∀ {b x : α} {f : Perm α},
    ↑(swap x (↑f x) * f) b ≠ b → ↑(f ^ n) (↑f x) = b → ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
induction' n with n n
no goals
case ofNat
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f g : Perm α✝
x y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
⊢ ∀ {b x : α} {f : Perm α},
    ↑(swap x (↑f x) * f) b ≠ b → ↑(f ^ Int.ofNat n) (↑f x) = b → ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
exact isCycle_swap_mul_aux₁ n
case negSucc
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ↑(swap x (↑f x) * f) b ≠ b
h : ↑(f ^ Int.negSucc n) (↑f x) = b
⊢ ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
case negSucc
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f g : Perm α✝
x y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
⊢ ∀ {b x : α} {f : Perm α},
    ↑(swap x (↑f x) * f) b ≠ b → ↑(f ^ Int.negSucc n) (↑f x) = b → ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
intro b x f hb h
no goals
case negSucc
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ↑(swap x (↑f x) * f) b ≠ b
h : ↑(f ^ Int.negSucc n) (↑f x) = b
⊢ ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
exact if hfbx' : f x = b then ⟨0, hfbx'⟩
  else
    have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
    have hb : (swap x (f⁻¹ x) * f⁻¹) (f⁻¹ b) ≠ f⁻¹ b := by
      rw [mul_apply, swap_apply_def]
      split_ifs <;>
          simp only [inv_eq_iff_eq, Perm.mul_apply, zpow_negSucc,
            Ne.def, Perm.apply_inv_self] at
            * <;> tauto
    let ⟨i, hi⟩ :=
      isCycle_swap_mul_aux₁ n hb
        (show (f⁻¹ ^ n) (f⁻¹ x) = f⁻¹ b by
          rw [← zpow_ofNat, ← h, ← mul_apply, ← mul_apply, ← mul_apply, zpow_negSucc, ← inv_pow,
            pow_succ', mul_assoc, mul_assoc, inv_mul_self, mul_one, zpow_ofNat, ← pow_succ', ←
            pow_succ])
    have h : (swap x (f⁻¹ x) * f⁻¹) (f x) = f⁻¹ x := by
      rw [mul_apply, inv_apply_self, swap_apply_left]
    ⟨-i, by
      rw [← add_sub_cancel i 1, neg_sub, sub_eq_add_neg, zpow_add, zpow_one, zpow_neg,
        ← inv_zpow, mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x,
        zpow_add, zpow_one, mul_apply, mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self,
        swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx')]⟩
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ↑(swap x (↑f x) * f) b ≠ b
h : ↑(f ^ Int.negSucc n) (↑f x) = b
hfbx' : ¬↑f x = b
this : ↑f b ≠ b ∧ b ≠ x
⊢ (if ↑f⁻¹ (↑f⁻¹ b) = x then ↑f⁻¹ x else if ↑f⁻¹ (↑f⁻¹ b) = ↑f⁻¹ x then x else ↑f⁻¹ (↑f⁻¹ b)) ≠ ↑f⁻¹ b
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ↑(swap x (↑f x) * f) b ≠ b
h : ↑(f ^ Int.negSucc n) (↑f x) = b
hfbx' : ¬↑f x = b
this : ↑f b ≠ b ∧ b ≠ x
⊢ ↑(swap x (↑f⁻¹ x) * f⁻¹) (↑f⁻¹ b) ≠ ↑f⁻¹ b
rw [mul_apply, swap_apply_def]
no goals
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ↑(swap x (↑f x) * f) b ≠ b
h : ↑(f ^ Int.negSucc n) (↑f x) = b
hfbx' : ¬↑f x = b
this : ↑f b ≠ b ∧ b ≠ x
⊢ (if ↑f⁻¹ (↑f⁻¹ b) = x then ↑f⁻¹ x else if ↑f⁻¹ (↑f⁻¹ b) = ↑f⁻¹ x then x else ↑f⁻¹ (↑f⁻¹ b)) ≠ ↑f⁻¹ b
split_ifs <;>
    simp only [inv_eq_iff_eq, Perm.mul_apply, zpow_negSucc,
      Ne.def, Perm.apply_inv_self] at
      * <;> tauto
no goals
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb✝ : ↑(swap x (↑f x) * f) b ≠ b
h : ↑(f ^ Int.negSucc n) (↑f x) = b
hfbx' : ¬↑f x = b
this : ↑f b ≠ b ∧ b ≠ x
hb : ↑(swap x (↑f⁻¹ x) * f⁻¹) (↑f⁻¹ b) ≠ ↑f⁻¹ b
⊢ ↑(f⁻¹ ^ n) (↑f⁻¹ x) = ↑f⁻¹ b
rw [← zpow_ofNat, ← h, ← mul_apply, ← mul_apply, ← mul_apply, zpow_negSucc, ← inv_pow,
  pow_succ', mul_assoc, mul_assoc, inv_mul_self, mul_one, zpow_ofNat, ← pow_succ', ←
  pow_succ]
no goals
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb✝ : ↑(swap x (↑f x) * f) b ≠ b
h : ↑(f ^ Int.negSucc n) (↑f x) = b
hfbx' : ¬↑f x = b
this : ↑f b ≠ b ∧ b ≠ x
hb : ↑(swap x (↑f⁻¹ x) * f⁻¹) (↑f⁻¹ b) ≠ ↑f⁻¹ b
i : ℤ
hi : ↑((swap x (↑f⁻¹ x) * f⁻¹) ^ i) (↑f⁻¹ x) = ↑f⁻¹ b
⊢ ↑(swap x (↑f⁻¹ x) * f⁻¹) (↑f x) = ↑f⁻¹ x
rw [mul_apply, inv_apply_self, swap_apply_left]
no goals
ι : Type ?u.676454
α✝ : Type ?u.676457
β : Type ?u.676460
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb✝ : ↑(swap x (↑f x) * f) b ≠ b
h✝ : ↑(f ^ Int.negSucc n) (↑f x) = b
hfbx' : ¬↑f x = b
this : ↑f b ≠ b ∧ b ≠ x
hb : ↑(swap x (↑f⁻¹ x) * f⁻¹) (↑f⁻¹ b) ≠ ↑f⁻¹ b
i : ℤ
hi : ↑((swap x (↑f⁻¹ x) * f⁻¹) ^ i) (↑f⁻¹ x) = ↑f⁻¹ b
h : ↑(swap x (↑f⁻¹ x) * f⁻¹) (↑f x) = ↑f⁻¹ x
⊢ ↑((swap x (↑f x) * f) ^ (-i)) (↑f x) = b
rw [← add_sub_cancel i 1, neg_sub, sub_eq_add_neg, zpow_add, zpow_one, zpow_neg,
  ← inv_zpow, mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x,
  zpow_add, zpow_one, mul_apply, mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self,
  swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx')]