awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
i : ↥b.support
a :
  ∀ (j k : ↥b.support),
    h i (Sum.inl j) (Sum.inl k) =
      Matrix.diagonal (n := ↥b.support ⊕ ι) (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inl j)
        (Sum.inl k)
a₁ :
  ∀ (j : ↥b.support) (k : ι),
    h i (Sum.inl j) (Sum.inr k) =
      Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inl j) (Sum.inr k)
a₂ :
  ∀ (j : ι) (k : ↥b.support),
    h i (Sum.inr j) (Sum.inl k) =
      Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inr j) (Sum.inl k)
a₃ :
  ∀ (j k : ι),
    h i (Sum.inr j) (Sum.inr k) =
      Matrix.diagonal (n := ↥b.support ⊕ ι) (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inr j)
        (Sum.inr k)
⊢ h i = Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))

Tactic:
ext (j | j) (k | k)
-- 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 ι
i j k : ↥b.support
⊢ h i (Sum.inl j) (Sum.inl k) =
    Matrix.diagonal (n := ↥b.support ⊕ ι) (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inl j)
      (Sum.inl k)

Tactic:
simp [h, Matrix.diagonal_apply]

Premises used: RootPairing.GeckConstruction.h, Matrix.diagonal_apply
-- 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 ι
i j : ↥b.support
k : ι
⊢ h i (Sum.inl j) (Sum.inr k) =
    Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inl j) (Sum.inr k)

Tactic:
simp [h, Matrix.diagonal_apply]

Premises used: RootPairing.GeckConstruction.h, Matrix.diagonal_apply
-- 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 ι
i : ↥b.support
j : ι
k : ↥b.support
⊢ h i (Sum.inr j) (Sum.inl k) =
    Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inr j) (Sum.inl k)

Tactic:
simp [h, Matrix.diagonal_apply]

Premises used: RootPairing.GeckConstruction.h, Matrix.diagonal_apply
-- 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 ι
i : ↥b.support
j k : ι
⊢ h i (Sum.inr j) (Sum.inr k) =
    Matrix.diagonal (n := ↥b.support ⊕ ι) (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inr j)
      (Sum.inr k)

Tactic:
simp [h, Matrix.diagonal_apply]

Premises used: RootPairing.GeckConstruction.h, Matrix.diagonal_apply
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
h :
  ∀ (x : ↥b.support) (x_1 : ↥b.support ⊕ ι),
    Eq.{u_2 + 1} (α := R)
      (((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
            (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
          GeckConstruction.h)
        x x_1)
      (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R)
        (fun (i : ↥b.support) ↦ comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
        x x_1)
⊢ Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      GeckConstruction.h)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
      comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))

Tactic:
ext
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
x : ↥b.support
x_1 : ↥b.support ⊕ ι
h :
  Eq.{u_2 + 1} (α := R)
    ((Matrix.diagLinearMap (↥b.support ⊕ ι) R R : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R)
        (Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x_2 : ι) ↦ (↑(P.pairingIn ℤ x_2 (↑x : ι)) : R))) x_1 :
      R)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R)
        (fun (i : ↥b.support) ↦ comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
        x x_1 :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    (((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
          (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
        GeckConstruction.h)
      x x_1)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R)
      (fun (i : ↥b.support) ↦ comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι)) x
      x_1)

Tactic:
rw [comp_apply, h_def]

Premises used: RootPairing.GeckConstruction.h_def, Function.comp_apply
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
x : ↥b.support
x_1 : ↥b.support ⊕ ι
⊢ Eq.{u_2 + 1} (α := R)
    ((Matrix.diagLinearMap (↥b.support ⊕ ι) R R : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R)
        (Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x_2 : ι) ↦ (↑(P.pairingIn ℤ x_2 (↑x : ι)) : R))) x_1 :
      R)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R)
        (fun (i : ↥b.support) ↦ comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
        x x_1 :
      R)

Tactic:
aesop
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
⊢ Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
      comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))

Tactic:
have : Matrix.diagLinearMap (b.support ⊕ ι) R R ∘ h =
      Sum.elimZeroLeft ∘ fun i : b.support ↦ algebraMap ℤ R ∘ (P.pairingIn ℤ · i) := by
    ext; rw [comp_apply, h_def]; aesop
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
this :
  Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
      comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
apply :
  LinearIndependent (ι := ↥b.support) R (M := ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
⊢ LinearIndependent (ι := ↥b.support) R h

Tactic:
apply LinearIndependent.of_comp (Matrix.diagLinearMap _ _ _)

Premises used: Matrix.diagLinearMap, LinearIndependent.of_comp
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
this :
  Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
      comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
rw : LinearIndependent ℤ (M := ι → ℤ) fun (i : ↥b.support) (x : ι) ↦ P.pairingIn ℤ x (↑i : ι)
⊢ LinearIndependent (ι := ↥b.support) R (M := ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)

Tactic:
rw [this, LinearMap.linearIndependent_iff_of_injOn _ Sum.elim_injective'.injOn,
    linearIndependent_algebraMap_comp_iff]

Premises used: linearIndependent_algebraMap_comp_iff, LinearMap.linearIndependent_iff_of_injOn
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
this :
  Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
      comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
suffices : LinearIndependent ℤ (M := (j : ↥b.support) → ℤ) fun (i j : ↥b.support) ↦ P.pairingIn ℤ (↑j : ι) (↑i : ι)
⊢ LinearIndependent ℤ (M := ι → ℤ) fun (i : ↥b.support) (x : ι) ↦ P.pairingIn ℤ x (↑i : ι)

Tactic:
suffices LinearIndependent ℤ (fun i j : b.support ↦ P.pairingIn ℤ j i) from
    this.of_linearIndependent_subset b.support
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
this :
  Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
      comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
apply : b.cartanMatrixᵀ.det ≠ 0
⊢ LinearIndependent ℤ (M := (j : ↥b.support) → ℤ) fun (i j : ↥b.support) ↦ P.pairingIn ℤ (↑j : ι) (↑i : ι)

Tactic:
apply b.cartanMatrix.transpose.linearIndependent_rows_of_det_ne_zero

Premises used: Matrix.linearIndependent_rows_of_det_ne_zero
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
this :
  Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
      comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
rw : b.cartanMatrix.Nondegenerate
⊢ b.cartanMatrixᵀ.det ≠ 0

Tactic:
rw [Matrix.det_transpose, ← Matrix.nondegenerate_iff_det_ne_zero]

Premises used: Matrix.det_transpose, Matrix.nondegenerate_iff_det_ne_zero
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
this :
  Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
      comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
⊢ b.cartanMatrix.Nondegenerate

Tactic:
b.cartanMatrix_nondegenerate

Premises used: RootPairing.Base.cartanMatrix_nondegenerate
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
this :
  Eq (α := ↥b.support → ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
    (comp (β := ι → R) (⇑Sum.elimZeroLeft : (a : ι → R) → ↥b.support ⊕ ι → R) fun (i : ↥b.support) ↦
      comp (β := ℤ) (⇑(algebraMap ℤ R) : (a : ℤ) → R) fun (x : ι) ↦ P.pairingIn ℤ x (↑i : ι))
⊢ b.cartanMatrix.Nondegenerate

Tactic:
exact b.cartanMatrix_nondegenerate

Premises used: RootPairing.Base.cartanMatrix_nondegenerate
-- 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 ι
rw :
  range h ⊆
    (↑(LinearMap.range (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R)) :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
⊢ LE.le (α := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
    (LinearMap.range (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R))

Tactic:
rw [span_le]

Premises used: Submodule.span_le
-- 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 ι
i : ↥b.support
rw :
  Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) ∈
    (↑(LinearMap.range (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R)) :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
⊢ h i ∈
    (↑(LinearMap.range (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R)) :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))

Tactic:
rw [h_eq_diagonal]

Premises used: RootPairing.GeckConstruction.h_eq_diagonal
-- 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 ι
i : ↥b.support
⊢ Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) ∈
    (↑(LinearMap.range (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R)) :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))

Tactic:
LinearMap.mem_range_self _ _

Premises used: Set.Mem, LinearMap.mem_range_self, Matrix.diagonal
-- 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 ι
i : ↥b.support
⊢ Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) ∈
    (↑(LinearMap.range (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R)) :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))

Tactic:
exact LinearMap.mem_range_self _ _

Premises used: LinearMap.mem_range_self
-- 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
x y : Matrix ι ι R
a :
  ∀ (i j : ↥b.support),
    fromBlocks 0 0 0 (x + y) (Sum.inl i) (Sum.inl j) =
      HAdd.hAdd (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (β :=
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (fromBlocks 0 0 0 x) (fromBlocks 0 0 0 y)
        (Sum.inl i) (Sum.inl j)
a₁ :
  ∀ (i : ↥b.support) (j : ι),
    fromBlocks (l := ↥b.support) 0 0 0 (x + y) (Sum.inl i) (Sum.inr j) =
      HAdd.hAdd (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (β :=
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (fromBlocks 0 0 0 x) (fromBlocks 0 0 0 y)
        (Sum.inl i) (Sum.inr j)
a₂ :
  ∀ (i : ι) (j : ↥b.support),
    fromBlocks (n := ↥b.support) 0 0 0 (x + y) (Sum.inr i) (Sum.inl j) =
      HAdd.hAdd (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (β :=
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (fromBlocks 0 0 0 x) (fromBlocks 0 0 0 y)
        (Sum.inr i) (Sum.inl j)
a₃ :
  ∀ (i j : ι),
    fromBlocks (l := ↥b.support) (n := ↥b.support) 0 0 0 (x + y) (Sum.inr i) (Sum.inr j) =
      HAdd.hAdd (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (β :=
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (fromBlocks 0 0 0 x) (fromBlocks 0 0 0 y)
        (Sum.inr i) (Sum.inr j)
⊢ fromBlocks 0 0 0 (x + y) =
    HAdd.hAdd (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (fromBlocks 0 0 0 x)
      (fromBlocks 0 0 0 y)

Tactic:
ext (i | i) (j | j)
-- 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
x y : Matrix ι ι R
i j : ↥b.support
⊢ fromBlocks 0 0 0 (x + y) (Sum.inl i) (Sum.inl j) =
    HAdd.hAdd (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (β :=
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (fromBlocks 0 0 0 x) (fromBlocks 0 0 0 y) (Sum.inl i)
      (Sum.inl j)

Tactic:
simp
-- 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
x y : Matrix ι ι R
i : ↥b.support
j : ι
⊢ fromBlocks (l := ↥b.support) 0 0 0 (x + y) (Sum.inl i) (Sum.inr j) =
    HAdd.hAdd (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (β :=
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (fromBlocks 0 0 0 x) (fromBlocks 0 0 0 y) (Sum.inl i)
      (Sum.inr j)

Tactic:
simp
-- 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
x y : Matrix ι ι R
i : ι
j : ↥b.support
⊢ fromBlocks (n := ↥b.support) 0 0 0 (x + y) (Sum.inr i) (Sum.inl j) =
    HAdd.hAdd (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (β :=
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (fromBlocks 0 0 0 x) (fromBlocks 0 0 0 y) (Sum.inr i)
      (Sum.inl j)

Tactic:
simp
-- 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
x y : Matrix ι ι R
i j : ι
⊢ fromBlocks (l := ↥b.support) (n := ↥b.support) 0 0 0 (x + y) (Sum.inr i) (Sum.inr j) =
    HAdd.hAdd (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (β :=
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (fromBlocks 0 0 0 x) (fromBlocks 0 0 0 y) (Sum.inr i)
      (Sum.inr j)

Tactic:
simp