-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CharZero R
inst_4 : IsDomain R
inst_5 : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
f g : Dual R M
hf₁ : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hf₂ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hg₁ : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hg₂ : MapsTo (⇑(preReflection x g) : (a : M) → M) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : (↑u : M →ₗ[R] M) = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih :
  (↑(u ^ n) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
this :
  Eq (α := M →ₗ[R] M)
    (LinearMap.smulRight (f - g) x ∘ₗ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x))
    0
succ :
  LinearMap.id ∘ₗ LinearMap.id +
        LinearMap.id ∘ₗ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
      HAdd.hAdd (α := M →ₗ[R] M) (LinearMap.smulRight (f - g) x ∘ₗ LinearMap.id)
        (LinearMap.smulRight (f - g) x ∘ₗ
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
succ₁ :
  LinearMap.id +
        LinearMap.id ∘ₗ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
      HAdd.hAdd (α := M →ₗ[R] M) (LinearMap.smulRight (f - g) x)
        (LinearMap.smulRight (f - g) x ∘ₗ
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
succ₂ :
  LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
      HAdd.hAdd (α := M →ₗ[R] M) (LinearMap.smulRight (f - g) x)
        (LinearMap.smulRight (f - g) x ∘ₗ
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
succ₃ :
  LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
      HAdd.hAdd (α := M →ₗ[R] M) (LinearMap.smulRight (f - g) x) 0 =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
succ₄ :
  LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
      LinearMap.smulRight (f - g) x =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
⊢ HMul.hMul (α := M →ₗ[R] M) LinearMap.id LinearMap.id +
        LinearMap.id * HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
      (LinearMap.smulRight (f - g) x * LinearMap.id +
        LinearMap.smulRight (f - g) x *
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
have succ₅ : LinearMap.id +
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
      LinearMap.smulRight (f - g) x) =
  LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
Tactic: simp_rw [Module.End.mul_eq_comp, LinearMap.comp_id, LinearMap.id_comp, this, add_zero,
        add_assoc, Nat.cast_succ, add_smul, one_smul]