-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ)
    ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
        (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) (↑p : ZMod q)) :
      ℤ)
nc : ∀ (n r : ℕ), Eq (α := ZMod r) (↑(↑n : ℤ) : ZMod r) (↑n : ZMod r)
nc' : (↑(HPow.hPow (α := ℤ) (-1) (p / 2)) : ZMod q) = HPow.hPow (α := ZMod q) (-1) (p / 2)
rw :
  HMul.hMul (α := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ) (legendreSym p (↑q : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₁ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑(↑p : ℤ) : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₂ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(↑q : ℤ) : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₃ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑q : ZMod p) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₄ :
  HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ)
          (HMul.hMul (α := ZMod q) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) (↑p : ZMod q)) :
        ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₅ :
  HMul.hMul (α := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
      (HMul.hMul (α := ℤ) (β := ℤ)
        ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) : ℤ)
        ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₆ :
  HMul.hMul (α := ℤ)
      ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) : ℤ)
      (HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
        ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
rw₇ :
  HMul.hMul (α := ℤ)
      ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) : ℤ)
      (HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)
        ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (q / 2 * (p / 2))
rw₈ :
  HMul.hMul (α := ℤ)
      ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) : ℤ)
      (HPow.hPow (α := ℤ) (β := ℕ) ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑p : ZMod q) : ℤ) 2) =
    HPow.hPow (α := ℤ) (-1) (q / 2 * (p / 2))
rw₉ :
  HMul.hMul (α := ℤ) (β := ℤ)
      ((quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) : ℤ) (1 : ℤ) =
    HPow.hPow (α := ℤ) (-1) (q / 2 * (p / 2))
rw₁₀ :
  (quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) =
    HPow.hPow (α := ℤ) (-1) (q / 2 * (p / 2))
⊢ legendreSym q (↑p : ℤ) * legendreSym p (↑q : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2))
have rw₁₁ : (quadraticChar (ZMod q) : (a : ZMod q) → ℤ) (↑((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)) : ZMod q) =
  HPow.hPow (α := ℤ) (-1) (q / 2) ^ (p / 2)
Tactic: rw [legendreSym, legendreSym, nc, nc, h, map_mul, mul_rotate', mul_comm (p / 2), ← pow_two,
    quadraticChar_sq_one (prime_ne_zero q p hpq.symm), mul_one, pow_mul, χ₄_eq_neg_one_pow hp₁, nc',
    map_pow, quadraticChar_neg_one hq₂, card q, χ₄_eq_neg_one_pow hq₁]