-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
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
simp_rw₃ :
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (Submodule.map (g ∘ₗ 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
simp_rw₄ :
  Function.comp (β := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R) d ∈
      Submodule.map (g ∘ₗ diagonalLinearMap ι R R)
        (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) ↔
    Membership.mem (γ := Submodule R ((j : ι) → R))
      (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) d
simp_rw₅ :
  (∃ (y : ι → R),
      Membership.mem (γ := Submodule R (ι → R))
          (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) y ∧
        Eq (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
          ((g ∘ₗ diagonalLinearMap ι R R : (a : ι → R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) y :
            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) 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₆ :
  (∃ (y : ι → R),
      Membership.mem (γ := Submodule R (ι → R))
          (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) y ∧
        Eq (α := 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) y)
          (Function.comp (β := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
            (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R) d)) ↔
    Membership.mem (γ := Submodule R ((j : ι) → R))
      (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) d
simp_rw₇ :
  (∃ (y : ι → R),
      Membership.mem (γ := Submodule R (ι → R))
          (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) y ∧
        y = d) ↔
    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

Tactic:
simp_rw [h₁, h₂, span_image, ← map_comp, ← comp_apply (f := g), mem_map, LinearMap.coe_comp,
    h₀.eq_iff, exists_eq_right]

Premises used: Submodule.mem_map, Function.Injective.eq_iff, exists_eq_right, Submodule.map_comp, LinearMap.coe_comp, Function.comp_apply, Submodule.span_image