induction

Stream: mathlib4

[BANGJI HU]

Hello, when I was dealing with the objective function using mathematical induction and applying rw, I encountered the error "tactic 'rewrite' failed, did not find instance of the pattern in the target expression". Is there any convenient way to directly achieve this?

import Mathlib.GroupTheory.Sylow
import Mathlib.Data.Nat.Factors

open Nat

theorem commutator_identity {G : Type*} [Group G] (x y : G) (hx : x * y * x⁻¹ * y⁻¹ = y * x * y⁻¹ * x⁻¹) :
    ∀ n : ℕ, x ^ n * y ^ n = (x * y) ^ n * (x * y * x⁻¹ * y⁻¹) ^ (n * (n - 1) / 2) := by
  let c := x * y * x⁻¹ * y⁻¹
  intro n
  induction n with
  | zero =>
    simp [pow_zero]
  | succ n ih =>

    simp_all [pow_succ, mul_assoc, mul_comm, mul_left_comm]
    rw [ih]
 ```

[Aaron Liu]

I think I agree with rw here. Where do you see the expression in your goal?

[Aaron Liu]

Actually, what do you expect rw to do?

[Kevin Buzzard]

Can you post the full error message?

[BANGJI HU]

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
x ^ n * y ^ n
G : Type u_1
inst✝ : Group G
x y : G
c : G := x * y * x⁻¹ * y⁻¹
n : ℕ
hx : x * (y * (x⁻¹ * y⁻¹)) = y * (x * (y⁻¹ * x⁻¹))
ih : x ^ n * y ^ n = (x * y) ^ n * (y * (x * (y⁻¹ * x⁻¹))) ^ (n * (n - 1) / 2)
⊢ x ^ n * (x * (y ^ n * y)) = (x * y) ^ n * (x * (y * (y * (x * (y⁻¹ * x⁻¹))) ^ (n * (n + 1) / 2)))

[Kevin Buzzard]

Yes, I also cannot find it, so the error message is telling you everything you need to know