awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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 : ι))
⊢ LinearIndependent ℤ (M := ι → ℤ) fun (i : ↥b.support) (x : ι) ↦ P.pairingIn ℤ x (↑i : ι)
have suffices : LinearIndependent ℤ (M := (j : ↥b.support) → ℤ) fun (i j : ↥b.support) ↦ P.pairingIn ℤ (↑j : ι) (↑i : ι)
Tactic: suffices LinearIndependent ℤ (fun i j : b.support ↦ P.pairingIn ℤ j i) from
    this.of_linearIndependent_subset b.support
-- 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 : 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 : ι))
⊢ LinearIndependent ℤ (M := (j : ↥b.support) → ℤ) fun (i j : ↥b.support) ↦ P.pairingIn ℤ (↑j : ι) (↑i : ι)
have apply : b.cartanMatrixᵀ.det ≠ 0
Tactic: apply b.cartanMatrix.transpose.linearIndependent_rows_of_det_ne_zero
-- 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 : 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ᵀ.det ≠ 0
have rw : b.cartanMatrix.Nondegenerate
Tactic: rw [Matrix.det_transpose, ← Matrix.nondegenerate_iff_det_ne_zero]
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
⊢ LinearIndependent (ι := ↥b.support) R h
have have : 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: classical
  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
  apply LinearIndependent.of_comp (Matrix.diagLinearMap _ _ _)
  rw [this, LinearMap.linearIndependent_iff_of_injOn _ Sum.elim_injective'.injOn,
    linearIndependent_algebraMap_comp_iff]
  suffices LinearIndependent ℤ (fun i j : b.support ↦ P.pairingIn ℤ j i) from
    this.of_linearIndependent_subset b.support
  apply b.cartanMatrix.transpose.linearIndependent_rows_of_det_ne_zero
  rw [Matrix.det_transpose, ← Matrix.nondegenerate_iff_det_ne_zero]
  exact b.cartanMatrix_nondegenerate
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
have :
  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 : ι))
⊢ LinearIndependent (ι := ↥b.support) R h
have have₁ : ∀
  (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 : ι))),
  LinearIndependent (ι := ↥b.support) R h
Tactic: classical
  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
  apply LinearIndependent.of_comp (Matrix.diagLinearMap _ _ _)
  rw [this, LinearMap.linearIndependent_iff_of_injOn _ Sum.elim_injective'.injOn,
    linearIndependent_algebraMap_comp_iff]
  suffices LinearIndependent ℤ (fun i j : b.support ↦ P.pairingIn ℤ j i) from
    this.of_linearIndependent_subset b.support
  apply b.cartanMatrix.transpose.linearIndependent_rows_of_det_ne_zero
  rw [Matrix.det_transpose, ← Matrix.nondegenerate_iff_det_ne_zero]
  exact b.cartanMatrix_nondegenerate
-- 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 ι
⊢ 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))
have rw : range h ⊆
  (↑(LinearMap.range (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R)) :
    Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
Tactic: rw [span_le]
-- 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 ι
i : ↥b.support
⊢ h i ∈
    (↑(LinearMap.range (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R)) :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
have 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))
Tactic: rw [h_eq_diagonal]
-- 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
x y : Matrix ι ι R
⊢ 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)
have 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)
Tactic: ext (i | i) (j | j)
-- 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
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)
⊢ 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)
have 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)
Tactic: ext (i | i) (j | j)
-- 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
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)
⊢ 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)
have 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)
Tactic: ext (i | i) (j | j)
-- 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
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)
⊢ 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)
have 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)
Tactic: ext (i | i) (j | j)
-- 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
t : R
x : Matrix ι ι R
⊢ fromBlocks 0 0 0 (t • x) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x)
have a : ∀ (i j : ↥b.support),
  fromBlocks 0 0 0 (t • x) (Sum.inl i) (Sum.inl j) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inl j)
Tactic: ext (i | i) (j | j)
-- 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
t : R
x : Matrix ι ι R
a :
  ∀ (i j : ↥b.support),
    fromBlocks 0 0 0 (t • x) (Sum.inl i) (Sum.inl j) =
      HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inl j)
⊢ fromBlocks 0 0 0 (t • x) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x)
have a₁ : ∀ (i : ↥b.support) (j : ι),
  fromBlocks (l := ↥b.support) 0 0 0 (t • x) (Sum.inl i) (Sum.inr j) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inr j)
Tactic: ext (i | i) (j | j)
-- 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
t : R
x : Matrix ι ι R
a :
  ∀ (i j : ↥b.support),
    fromBlocks 0 0 0 (t • x) (Sum.inl i) (Sum.inl j) =
      HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inl j)
a₁ :
  ∀ (i : ↥b.support) (j : ι),
    fromBlocks (l := ↥b.support) 0 0 0 (t • x) (Sum.inl i) (Sum.inr j) =
      HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inr j)
⊢ fromBlocks 0 0 0 (t • x) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x)
have a₂ : ∀ (i : ι) (j : ↥b.support),
  fromBlocks (n := ↥b.support) 0 0 0 (t • x) (Sum.inr i) (Sum.inl j) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x) (Sum.inr i) (Sum.inl j)
Tactic: ext (i | i) (j | j)
-- 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
t : R
x : Matrix ι ι R
a :
  ∀ (i j : ↥b.support),
    fromBlocks 0 0 0 (t • x) (Sum.inl i) (Sum.inl j) =
      HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inl j)
a₁ :
  ∀ (i : ↥b.support) (j : ι),
    fromBlocks (l := ↥b.support) 0 0 0 (t • x) (Sum.inl i) (Sum.inr j) =
      HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inr j)
a₂ :
  ∀ (i : ι) (j : ↥b.support),
    fromBlocks (n := ↥b.support) 0 0 0 (t • x) (Sum.inr i) (Sum.inl j) =
      HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x) (Sum.inr i) (Sum.inl j)
⊢ fromBlocks 0 0 0 (t • x) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x)
have a₃ : ∀ (i j : ι),
  fromBlocks (l := ↥b.support) (n := ↥b.support) 0 0 0 (t • x) (Sum.inr i) (Sum.inr j) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((RingHom.id R : (a : R) → R) t : R) (fromBlocks 0 0 0 x) (Sum.inr i) (Sum.inr j)
Tactic: ext (i | i) (j | j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (hypothesis)
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' := ⋯ }
⊢ 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 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))
Tactic: have h₀ : Injective (g ∘ diagonalLinearMap ι R R) := fun _ _ hd ↦ funext <| by simpa [g] using hd
-- 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_1 : ι → 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))
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))
have a : ∀ (i j : ↥b.support),
  Matrix.diagonal (Sum.elim 0 d) (Sum.inl i) (Sum.inl j) =
    (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inl i) (Sum.inl j)
Tactic: ext (i | i) (j | j)
-- 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_1 : ι → 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))
d : ι → R
a :
  ∀ (i j : ↥b.support),
    Matrix.diagonal (Sum.elim 0 d) (Sum.inl i) (Sum.inl j) =
      (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inl i) (Sum.inl j)
⊢ 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))
have a₁ : ∀ (i : ↥b.support) (j : ι),
  Matrix.diagonal (Sum.elim 0 d) (Sum.inl i) (Sum.inr j) =
    (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inl i) (Sum.inr j)
Tactic: ext (i | i) (j | j)