-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
rw :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
rw₁ :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((LinearEquiv.symm (AddEquiv.toIntLinearEquiv (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((LinearEquiv.symm (AddEquiv.toIntLinearEquiv (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
rw₂ :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((AddEquiv.toIntLinearEquiv (AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((AddEquiv.toIntLinearEquiv (AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
rw₃ :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
rw₄ :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) ((AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ) : (a : ℤ) → 𝓞 ℚ) 1)
          ((AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ) : (a : ℤ) → 𝓞 ℚ) 1)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
⊢ Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
have rw₅ : Eq (α := ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((ringOfIntegersEquiv.symm : (a : ℤ) → 𝓞 ℚ) 1)
        ((ringOfIntegersEquiv.symm : (a : ℤ) → 𝓞 ℚ) 1)) :
    ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
Tactic: rw [Basis.map_apply, RingEquiv.toAddEquiv_eq_coe, ← AddEquiv.toIntLinearEquiv_symm,
        AddEquiv.coe_toIntLinearEquiv, Basis.singleton_apply,
        show (AddEquiv.symm ↑ringOfIntegersEquiv) (1 : ℤ) = ringOfIntegersEquiv.symm 1 by rfl,
        map_one, mul_one]