-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
rintro :
  ∀ (x₁ y₁ x₂ y₂ : ℝ),
    (HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
          (a : ℂ) → A)
        ({ re := x₁, im := y₁ : ℂ } * { re := x₂, im := y₂ : ℂ }) =
      HMul.hMul (α := A) (β := A)
        ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
              (a : ℂ) → A)
            { re := x₁, im := y₁ : ℂ } :
          A)
        ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
              (a : ℂ) → A)
            { re := x₂, im := y₂ : ℂ } :
          A)
rintro₁ :
  ∀ (x₁ y₁ x₂ y₂ : ℝ),
    (HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
          (a : ℂ) → A)
        { re := x₁ * x₂ - y₁ * y₂, im := x₁ * y₂ + y₁ * x₂ : ℂ } =
      HMul.hMul (α := A) (β := A)
        ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
              (a : ℂ) → A)
            { re := x₁, im := y₁ : ℂ } :
          A)
        ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
              (a : ℂ) → A)
            { re := x₂, im := y₂ : ℂ } :
          A)
rintro₂ :
  ∀ (x₁ y₁ x₂ y₂ : ℝ),
    HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) : A) ((x₁ * y₂ + y₁ * x₂) • I') =
      HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) (y₁ • I') *
        HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) (y₂ • I')
rintro₃ :
  ∀ (x₁ y₁ x₂ y₂ : ℝ),
    HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) : A) ((x₁ * y₂ + y₁ * x₂) • I') =
      HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) +
          y₁ • I' * y₂ • I' +
        (HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) (y₂ • I') +
          HMul.hMul (β := A) (y₁ • I') ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A))
⊢ ∀ (x y : ℂ),
    (HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
          (a : ℂ) → A)
        (x * y) =
      HMul.hMul (α := A) (β := A)
        ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
              (a : ℂ) → A)
            x :
          A)
        ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
              (a : ℂ) → A)
            y :
          A)
have e_a : ∀ (x₁ y₁ x₂ y₂ : ℝ),
  (algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) =
    HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) +
      y₁ • I' * y₂ • I'
Tactic: finally
  rintro ⟨x₁, y₁⟩ ⟨x₂, y₂⟩
  rw [mk_mul_mk]
  change
    algebraMap ℝ A (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
      (algebraMap ℝ A x₁ + y₁ • I') * (algebraMap ℝ A x₂ + y₂ • I')
  rw [add_mul, mul_add, mul_add, add_comm _ (y₁ • I' * y₂ • I'), add_add_add_comm]
  congr 1
  -- equate "real" and "imaginary" parts
  · rw [smul_mul_smul_comm, hf, smul_neg, ← algebraMap_eq_smul_one, ← sub_eq_add_neg,
      ← map_mul, ← map_sub]
  · rw [smul_def, smul_def, smul_def, ← right_comm _ x₂,
      ← mul_assoc, ← add_mul, ← map_mul, ← map_mul, ← map_add]