-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem isCycle_swap_mul_aux₂ {α : Type*} [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

Proof state:
α : Type u_4
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

Tactic:
rw [mul_apply, swap_apply_def]

Result:
α : Type u_4
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

Proof state:
α : Type u_4
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

Tactic:
rw [← add_sub_cancel_right 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')]

Result:
no goals

Proof state:
α : Type u_4
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

Tactic:
rw [← zpow_natCast, ← h, ← mul_apply, ← mul_apply, ← mul_apply, zpow_negSucc,
  ← inv_pow, pow_succ, mul_assoc, mul_assoc, inv_mul_cancel, mul_one, zpow_natCast,
  ← pow_succ', ← pow_succ]

Result:
no goals

Proof state:
α : Type u_4
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

Tactic:
intro n

Result:
α : Type u_4
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

Proof state:
α : Type u_4
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

Tactic:
cases n with
| ofNat n => exact isCycle_swap_mul_aux₁ n
| negSucc n =>
  intro b x f hb h
  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, 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_natCast, ← h, ← mul_apply, ← mul_apply, ← mul_apply, zpow_negSucc,
              ← inv_pow, pow_succ, mul_assoc, mul_assoc, inv_mul_cancel, mul_one, zpow_natCast,
              ← 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_right 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')]⟩

Result:
no goals

Proof state:
α : Type u_4
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

Tactic:
split_ifs <;>
  simp only [inv_eq_iff_eq, Perm.mul_apply, zpow_negSucc, Ne, Perm.apply_inv_self] at *
    <;> tauto

Result:
no goals

Proof state:
case negSucc
α : Type u_4
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

Tactic:
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, 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_natCast, ← h, ← mul_apply, ← mul_apply, ← mul_apply, zpow_negSucc,
            ← inv_pow, pow_succ, mul_assoc, mul_assoc, inv_mul_cancel, mul_one, zpow_natCast,
            ← 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_right 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')]⟩

Result:
no goals

Proof state:
α : Type u_4
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

Tactic:
rw [mul_apply, inv_apply_self, swap_apply_left]

Result:
no goals

Proof state:
case negSucc
α : Type u_4
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

Tactic:
intro b x f hb h

Result:
case negSucc
α : Type u_4
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

Proof state:
case ofNat
α : Type u_4
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

Tactic:
exact isCycle_swap_mul_aux₁ n

Result:
no goals