ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
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.610936
α✝ : Type ?u.610939
β : Type ?u.610942
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 zero
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f g : Perm α✝
x y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {b x : α} {f : Perm α},
    ↑(swap x (↑f x) * f) b ≠ b → ↑(f ^ Nat.zero) (↑f x) = b → ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b

case succ
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f g : Perm α✝
x y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
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 ^ Nat.succ n) (↑f x) = b → ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
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 hn
no goals
case zero
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f g : Perm α✝
x y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {b x : α} {f : Perm α},
    ↑(swap x (↑f x) * f) b ≠ b → ↑(f ^ Nat.zero) (↑f x) = b → ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
exact fun _ h => ⟨0, h⟩
case succ
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
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 ^ Nat.succ n) (↑f x) = b
⊢ ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
case succ
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f g : Perm α✝
x y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
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 ^ Nat.succ n) (↑f x) = b → ∃ i, ↑((swap x (↑f x) * f) ^ i) (↑f x) = b
intro b x f hb h
no goals
case succ
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
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 ^ Nat.succ 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, apply_inv_self, swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx), Ne.def, ←
        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)]⟩
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
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 ^ Nat.succ n) (↑f x) = b
hfbx : ¬↑f x = b
this : ↑f b ≠ b ∧ b ≠ x
⊢ ¬↑f b = b
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
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 ^ Nat.succ 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, apply_inv_self, swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx), Ne.def, ←
  f.injective.eq_iff, apply_inv_self]
no goals
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
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 ^ Nat.succ n) (↑f x) = b
hfbx : ¬↑f x = b
this : ↑f b ≠ b ∧ b ≠ x
⊢ ¬↑f b = b
exact this.1
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
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 ^ Nat.succ 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 (↑(f ^ n) (↑f x)) = b
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
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 ^ Nat.succ 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 (↑(f ^ n) (↑f x)) = ↑f (↑f⁻¹ b)
rw [apply_inv_self]
no goals
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
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 ^ Nat.succ 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 (↑(f ^ n) (↑f x)) = b
rwa [pow_succ, mul_apply] at h
no goals
ι : Type ?u.610936
α✝ : Type ?u.610939
β : Type ?u.610942
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
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 ^ Nat.succ 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) ^ (i + 1)) (↑f x) = b
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)]