-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst_1 : NeZero n
this_1 : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀
this : NeZero (d * χ.conductor * n)
a :
  Eq (α := DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor * n)) χ₀ :
      DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R (d * χ.conductor)) → DirichletCharacter R (d * χ.conductor * n))
        ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
          χ.primitiveCharacter) :
      DirichletCharacter R (d * χ.conductor * n))
a₁ :
  Eq (α := DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor * n)) χ₀ :
      DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor * n))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor * n))
a₂ :
  Eq (α := DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (d * χ.conductor * n))
        ((changeLevel hd : (a : DirichletCharacter R d) → DirichletCharacter R n) χ₀) :
      DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor * n))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor * n))
a₃ :
  Eq (α := DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R n) → DirichletCharacter R (d * χ.conductor * n)) χ :
      DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor * n))
        χ.primitiveCharacter :
      DirichletCharacter R (d * χ.conductor * n))
⊢ Eq (α := DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R (d * χ.conductor)) → DirichletCharacter R (d * χ.conductor * n))
        ((changeLevel ⋯ : (a : DirichletCharacter R d) → DirichletCharacter R (d * χ.conductor)) χ₀) :
      DirichletCharacter R (d * χ.conductor * n))
    ((changeLevel ⋯ : (a : DirichletCharacter R (d * χ.conductor)) → DirichletCharacter R (d * χ.conductor * n))
        ((changeLevel ⋯ : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R (d * χ.conductor))
          χ.primitiveCharacter) :
      DirichletCharacter R (d * χ.conductor * n))
have a₄ : Eq (α := DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R n) → DirichletCharacter R (d * χ.conductor * n)) χ :
    DirichletCharacter R (d * χ.conductor * n))
  ((changeLevel sorry : (a : DirichletCharacter R n) → DirichletCharacter R (d * χ.conductor * n))
      ((changeLevel sorry : (a : DirichletCharacter R χ.conductor) → DirichletCharacter R n) χ.primitiveCharacter) :
    DirichletCharacter R (d * χ.conductor * n))
Tactic: rw [← changeLevel_trans, ← changeLevel_trans,
    changeLevel_trans _ hd (n.dvd_mul_left (d * χ.conductor)), ← hχ₀,
    changeLevel_trans χ.primitiveCharacter χ.conductor_dvd_level, changeLevel_primitiveCharacter]