-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : DecidableEq ι
d : ι → R
g : Matrix ι ι R →ₗ[R] Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  { toFun := fromBlocks 0 0 0, map_add' := ⋯, map_smul' := ⋯ }
h₀ :
  Injective (α := ι → R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (Function.comp (β := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R))
h₁ :
  ∀ {d : ι → R},
    Eq (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (Matrix.diagonal (Sum.elim 0 d))
      ((g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d))
h₂ :
  Eq (α := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h)
    (image (α := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (image (α := ι → R) (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R)
        (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))))
simp_rw :
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
      Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
      ((g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
          ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) :
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↔
    Membership.mem (γ := Submodule R ((j : ι) → R))
      (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) d
simp_rw₁ :
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
      Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
      (span R
        (image (α := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
          (image (α := ι → R) (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R)
            (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R)))))
      ((g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
          ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) :
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↔
    Membership.mem (γ := Submodule R ((j : ι) → R))
      (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) d
⊢ Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
      (Matrix.diagonal (Sum.elim 0 d)) ↔
    Membership.mem (γ := Submodule R ((j : ι) → R))
      (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) d
have simp_rw₂ : Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (Submodule.map g
      (Submodule.map (diagonalLinearMap ι R R)
        (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R)))))
    ((g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↔
  Membership.mem (γ := Submodule R ((j : ι) → R))
    (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) d
Tactic: simp_rw [h₁, h₂, span_image, ← map_comp, ← comp_apply (f := g), mem_map, LinearMap.coe_comp,
    h₀.eq_iff, exists_eq_right]