-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : Ne.{u_2 + 1} (α := FF') (↑(Fintype.card F) : FF') 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
a :
  gaussSum (χ' * φ') ψ.char * jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
      (gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ *
        jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ *
      ((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F')
a₁ :
  gaussSum χ' ψ.char * gaussSum φ' ψ.char *
      (gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ *
        jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ *
      ((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F')
a₂ :
  gaussSum χ' ψ.char * gaussSum φ' ψ.char *
      (gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ *
        jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ *
      ((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F')
a₃ :
  gaussSum χ' ψ.char * gaussSum φ' ψ.char *
      (gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ *
        jacobiSum (χ.ringHomComp (algebraMap F' FF'))⁻¹ (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ *
      ((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F')
⊢ gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ *
      (jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
        jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ *
      ((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F')
have a₄ : gaussSum χ' ψ.char * gaussSum φ' ψ.char *
    (gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ *
      jacobiSum (χ.ringHomComp (algebraMap F' FF'))⁻¹ (φ.ringHomComp (algebraMap F' FF'))⁻¹) =
  gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ *
    ((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F')
Tactic: rw [mul_mul_mul_comm, jacobiSum_mul_nontrivial Hχφ, mul_inv, ← ringHomComp_inv,
    ← ringHomComp_inv, jacobiSum_mul_nontrivial Hχφ', map_natCast, ← mul_mul_mul_comm,
    gaussSum_mul_gaussSum_eq_card Hχ ψ.prim, gaussSum_mul_gaussSum_eq_card Hφ ψ.prim,
    ← mul_inv, gaussSum_mul_gaussSum_eq_card Hχφ ψ.prim]