-- 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 : ℕ
hn : ∀ {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
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : ¬f x = b
this : f b ≠ b ∧ b ≠ x
⊢ ¬f b = b

Tactic:
exact this.1

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:
induction n with
| zero => exact fun _ h => ⟨0, h⟩
| succ n hn =>
  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, apply_inv_self, swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx), Ne, ←
          f.injective.eq_iff, apply_inv_self]
        exact this.1
      let ⟨i, hi⟩ := hn hb' (f.injective <| by
        rw [apply_inv_self]; rwa [pow_succ', mul_apply] at h)
      ⟨i + 1, by
        rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_inv_self,
          swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (Ne.symm hfbx)]⟩

Result:
no goals

Proof state:
case succ
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {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
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (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, apply_inv_self, swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx), Ne, ←
        f.injective.eq_iff, apply_inv_self]
      exact this.1
    let ⟨i, hi⟩ := hn hb' (f.injective <| by
      rw [apply_inv_self]; rwa [pow_succ', mul_apply] at h)
    ⟨i + 1, by
      rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_inv_self,
        swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (Ne.symm hfbx)]⟩

Result:
no goals

Proof state:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {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
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : ¬f x = b
this : f b ≠ b ∧ b ≠ x
hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b
⊢ f ((f ^ n) (f x)) = f (f⁻¹ b)

Tactic:
rw [apply_inv_self]

Result:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {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
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : ¬f x = b
this : f b ≠ b ∧ b ≠ x
hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b
⊢ f ((f ^ n) (f x)) = b

Proof state:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {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
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (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, apply_inv_self, swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx), Ne, ←
  f.injective.eq_iff, apply_inv_self]

Result:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {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
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : ¬f x = b
this : f b ≠ b ∧ b ≠ x
⊢ ¬f b = b

Proof state:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {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
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : ¬f x = b
this : f b ≠ b ∧ b ≠ x
hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b
⊢ f ((f ^ n) (f x)) = b

Tactic:
rwa [pow_succ', mul_apply] at h

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:
case succ
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {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
⊢ ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ (n + 1)) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
intro b x f hb h

Result:
case succ
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {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
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Proof state:
case zero
α : Type u_4
inst✝ : DecidableEq α
⊢ ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ 0) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
exact fun _ h => ⟨0, h⟩

Result:
no goals

Proof state:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {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
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (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) ^ (i + 1)) (f x) = b

Tactic:
rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_inv_self,
  swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (Ne.symm hfbx)]

Result:
no goals