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 ι
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)
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)
⊢ 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)

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
t : R
x : Matrix ι ι R
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:
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
t : R
x : Matrix ι ι R
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:
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
t : R
x : Matrix ι ι R
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:
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
t : R
x : Matrix ι ι R
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:
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
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' := ⋯ }
x x_1 : ι → R
hd :
  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) x)
    (Function.comp (β := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R) x_1)
⊢ ∀ (x_2 : ι), x x_2 = x_1 x_2

Tactic:
simpa [g] using hd
-- 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' := ⋯ }
⊢ 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
-- 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_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)
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)
a₂ :
  ∀ (i : ι) (j : ↥b.support),
    Matrix.diagonal (Sum.elim 0 d) (Sum.inr i) (Sum.inl j) =
      (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inr i) (Sum.inl j)
a₃ :
  ∀ (i j : ι),
    Matrix.diagonal (n := ↥b.support ⊕ ι) (Sum.elim 0 d) (Sum.inr i) (Sum.inr j) =
      (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inr i) (Sum.inr 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))

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_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
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:
simp [g]
-- 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_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
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:
simp [g]
-- 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_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
i : ι
j : ↥b.support
⊢ Matrix.diagonal (Sum.elim 0 d) (Sum.inr i) (Sum.inl j) =
    (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inr i) (Sum.inl j)

Tactic:
simp [g]
-- 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_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
i j : ι
⊢ Matrix.diagonal (n := ↥b.support ⊕ ι) (Sum.elim 0 d) (Sum.inr i) (Sum.inr j) =
    (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inr i) (Sum.inr j)

Tactic:
simp [g]
-- 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))
⊢ ∀ {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))

Tactic:
have h₁ {d : ι → R} : diagonal (Sum.elim 0 d) = g (diagonalLinearMap ι R R d) := by
    ext (i | i) (j | j) <;> simp [g]
-- 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 :
  ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
    Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range GeckConstruction.h)
        x ↔
      Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) 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))))
        x
⊢ Eq (α := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range GeckConstruction.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))))

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 : 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))
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) x ↔
    Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) 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))))
      x

Tactic:
simp [g, h_def]

Premises used: RootPairing.GeckConstruction.h_def
-- 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))
⊢ 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))))

Tactic:
have h₂ : range h = g '' (diagonalLinearMap ι R R ''
    (range <| fun (i : b.support) j ↦ (P.pairingIn ℤ j i : R))) := by ext; simp [g, h_def]
-- 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
i : ↥b.support
j : ↥b.support ⊕ ι
x_1 x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
h : Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range GeckConstruction.h) x
mem : ∀ (i_1 : ↥b.support), GeckConstruction.h i_1 j (Sum.inl i) = 0
⊢ x j (Sum.inl i) = 0

Tactic:
obtain ⟨i, rfl⟩ := h

Premises used: rfl
-- 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
i_1 : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
mem : ∀ (val : ↥b.support), h i (Sum.inl val) (Sum.inl i_1) = 0
mem₁ : ∀ (val : ι), h i (Sum.inr val) (Sum.inl i_1) = 0
⊢ h i j (Sum.inl i_1) = 0

Tactic:
cases 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
i_1 : ↥b.support
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i val : ↥b.support
⊢ h i (Sum.inl val) (Sum.inl i_1) = 0

Tactic:
simp [h]

Premises used: RootPairing.GeckConstruction.h
-- 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
i_1 : ↥b.support
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
val : ι
⊢ h i (Sum.inr val) (Sum.inl i_1) = 0

Tactic:
simp [h]

Premises used: RootPairing.GeckConstruction.h
-- 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
i : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ Eq.{u_2 + 1} (α := R) (0 j (Sum.inl i)) 0

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
i : ↥b.support
j : ↥b.support ⊕ ι
x u v : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) u
hy : Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) v
hu : u j (Sum.inl i) = 0
hv : v j (Sum.inl i) = 0
⊢ (u + v) j (Sum.inl i) = 0

Tactic:
simp [hu, hv]
-- 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
i : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
t : R
u : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) u
hu : u j (Sum.inl i) = 0
⊢ (t • u) j (Sum.inl i) = 0

Tactic:
simp [hu]
-- 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
i : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) x
mem :
  ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (h : Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) x),
    x j (Sum.inl i) = 0
zero : Eq.{u_2 + 1} (α := R) (0 j (Sum.inl i)) 0
add :
  ∀ (u v : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
    Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
        u →
      Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
          v →
        ∀ (hu : u j (Sum.inl i) = 0) (hv : v j (Sum.inl i) = 0), (u + v) j (Sum.inl i) = 0
smul :
  ∀ (t : R) (u : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
    Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
        u →
      ∀ (hu : u j (Sum.inl i) = 0), (t • u) j (Sum.inl i) = 0
⊢ x j (Sum.inl i) = 0

Tactic:
induction hx using span_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; cases j <;> simp [h]
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]

Premises used: RootPairing.GeckConstruction.h, Submodule.smul, Submodule.zero, Submodule.add, rfl