awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
i : ι
⊢ (P.coroot : (a : ι) → N) i =
    HSMul.hSMul (β := N)
      (HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R))
      ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
have h₀ : Ne.{u_2 + 1} (α := R)
  ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M) :
    R)
  (0 : R)
Tactic: have h₀ := IsAnisotropic.rootForm_root_ne_zero (P := P) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
i : ι
h₀ :
  Ne.{u_2 + 1} (α := R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    (0 : R)
⊢ (P.coroot : (a : ι) → N) i =
    HSMul.hSMul (β := N)
      (HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R))
      ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
have rw : HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) =
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
Tactic: rw [polarizationEquiv_apply, ← (smul_right_injective N h₀).eq_iff, P.rootForm_self_smul_coroot i,
    smul_smul, mul_div_cancel₀ _ h₀]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
i : ι
h₀ :
  Ne.{u_2 + 1} (α := R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    (0 : R)
⊢ HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
have norm_cast : HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) =
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
⊢ LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) s
have obtain : ∀ (f : (↑s : Type u_1) → Rˣ)
  (hf :
    ∀ (i : (↑s : Type u_1)),
      (P.coroot : (a : ι) → N) (↑i : ι) =
        HSMul.hSMul (β := N) (f i) ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) (↑i : ι) : M) : N)),
  LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) s
Tactic: obtain ⟨f, hf⟩ : ∃ f : s → Rˣ, ∀ i : s, P.coroot i = f i • P.PolarizationEquiv (P.root i) :=
    ⟨fun i ↦ Units.mk0 (2 / P.RootForm (P.root i) (P.root i))
      (by simp [two_ne_zero, IsAnisotropic.rootForm_root_ne_zero]),
     fun i ↦ by simp [coroot_eq_polarizationEquiv_apply_root]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : (↑s : Type u_1) → Rˣ
hf :
  ∀ (i : (↑s : Type u_1)),
    (P.coroot : (a : ι) → N) (↑i : ι) =
      HSMul.hSMul (β := N) (f i) ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) (↑i : ι) : M) : N)
⊢ Eq (α := (a : (↑s : Type u_1)) → N)
    (s.restrict (π := fun (a : ι) ↦ N) (⇑P.coroot : (a : ι) → N) : (a : (↑s : Type u_1)) → N)
    ((⇑(↑P.PolarizationEquiv : M →ₗ[R] N) : (a : M) → N) ∘
        HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
          (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M) :
      (↑s : Type u_1) → N)
have h₁ : ∀ (x : (↑s : Type u_1)),
  Eq.{u_4 + 1} (α := N) (s.restrict (π := fun (a : ι) ↦ N) (⇑P.coroot : (a : ι) → N) x : N)
    (((⇑(↑P.PolarizationEquiv : M →ₗ[R] N) : (a : M) → N) ∘
          HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
            (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M))
        x :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : (↑s : Type u_1) → Rˣ
hf :
  ∀ (i : (↑s : Type u_1)),
    (P.coroot : (a : ι) → N) (↑i : ι) =
      HSMul.hSMul (β := N) (f i) ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) (↑i : ι) : M) : N)
⊢ LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) s
have this : Eq (α := (a : (↑s : Type u_1)) → N)
  (s.restrict (π := fun (a : ι) ↦ N) (⇑P.coroot : (a : ι) → N) : (a : (↑s : Type u_1)) → N)
  ((⇑(↑P.PolarizationEquiv : M →ₗ[R] N) : (a : M) → N) ∘
      HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
        (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M) :
    (↑s : Type u_1) → N)
Tactic: have : (s.restrict P.coroot) = P.PolarizationEquiv.toLinearMap ∘ (f • (s.restrict P.root)) := by
    ext; simp [hf, polarizationEquiv_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : P.IsRootSystem
inst_8 : NeZero.{u_2} (R := R) 2
s : Set ι
h : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : (↑s : Type u_1) → Rˣ
hf :
  ∀ (i : (↑s : Type u_1)),
    (P.coroot : (a : ι) → N) (↑i : ι) =
      HSMul.hSMul (β := N) (f i) ((P.PolarizationEquiv : (a : M) → N) ((P.root : (a : ι) → M) (↑i : ι) : M) : N)
this :
  Eq (α := (a : (↑s : Type u_1)) → N)
    (s.restrict (π := fun (a : ι) ↦ N) (⇑P.coroot : (a : ι) → N) : (a : (↑s : Type u_1)) → N)
    ((⇑(↑P.PolarizationEquiv : M →ₗ[R] N) : (a : M) → N) ∘
        HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
          (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M) :
      (↑s : Type u_1) → N)
⊢ LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) s
have rw : LinearIndependent R
  (HSMul.hSMul (β := (a : (↑s : Type u_1)) → M) f
    (s.restrict (π := fun (a : ι) ↦ M) (⇑P.root : (a : ι) → M) : (a : (↑s : Type u_1)) → M))
Tactic: rw [← linearIndependent_restrict_iff, this,
    LinearMap.linearIndependent_iff_of_injOn _ P.PolarizationEquiv.injective.injOn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
x : M
hx : Membership.mem (γ := Submodule R M) (P.rootSpan R) x
hx' : Eq.{u_2 + 1} (α := R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
⊢ x = 0
have this : x ∈ P.rootSpan R ⊓ LinearMap.ker P.RootForm
Tactic: have : x ∈ P.rootSpan R ⊓ LinearMap.ker P.RootForm := ⟨hx, P.rootForm_self_eq_zero_iff.mp hx'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
x : M
hx : Membership.mem (γ := Submodule R M) (P.rootSpan R) x
h : x ≠ 0
⊢ LT.lt.{u_2} (α := R) (0 : R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
have apply : Ne.{u_2 + 1} (α := R) (0 : R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
Tactic: apply (P.zero_le_rootForm x).lt_of_ne
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : Module R M
inst_7 : Module R N
P : RootPairing ι R M N
x : M
hx : Membership.mem (γ := Submodule R M) (P.rootSpan R) x
h : x ≠ 0
⊢ Ne.{u_2 + 1} (α := R) (0 : R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
have contrapose : ∀ (h : Eq.{u_2 + 1} (α := R) (0 : R) ((((P.RootForm : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)), x = 0
Tactic: contrapose h
Cleared hypotheses: h
-- 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 = Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
have a : ∀ (j k : ↥b.support),
  h i (Sum.inl j) (Sum.inl k) =
    Matrix.fromBlocks (m := ι) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inl j)
      (Sum.inl k)
Tactic: ext (j | j) (k | k)
-- 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
a :
  ∀ (j k : ↥b.support),
    h i (Sum.inl j) (Sum.inl k) =
      Matrix.fromBlocks (m := ι) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inl j)
        (Sum.inl k)
⊢ h i = Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
have a₁ : ∀ (j : ↥b.support) (k : ι),
  h i (Sum.inl j) (Sum.inr k) =
    Matrix.fromBlocks (l := ↥b.support) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
      (Sum.inl j) (Sum.inr k)
Tactic: ext (j | j) (k | k)
-- 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
a :
  ∀ (j k : ↥b.support),
    h i (Sum.inl j) (Sum.inl k) =
      Matrix.fromBlocks (m := ι) 0 0 0 (Matrix.diagonal 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.fromBlocks (l := ↥b.support) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
        (Sum.inl j) (Sum.inr k)
⊢ h i = Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
have a₂ : ∀ (j : ι) (k : ↥b.support),
  h i (Sum.inr j) (Sum.inl k) =
    Matrix.fromBlocks (n := ↥b.support) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
      (Sum.inr j) (Sum.inl k)
Tactic: ext (j | j) (k | k)
-- 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
a :
  ∀ (j k : ↥b.support),
    h i (Sum.inl j) (Sum.inl k) =
      Matrix.fromBlocks (m := ι) 0 0 0 (Matrix.diagonal 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.fromBlocks (l := ↥b.support) 0 0 0 (Matrix.diagonal 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.fromBlocks (n := ↥b.support) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
        (Sum.inr j) (Sum.inl k)
⊢ h i = Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
have a₃ : ∀ (j k : ι),
  h i (Sum.inr j) (Sum.inr k) =
    Matrix.fromBlocks (l := ↥b.support) (n := ↥b.support) 0 0 0
      (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (Sum.inr j) (Sum.inr k)
Tactic: ext (j | j) (k | k)
-- 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 = Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
have 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)
Tactic: ext (j | j) (k | k)
-- 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
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)
⊢ h i = Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
have 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)
Tactic: ext (j | j) (k | k)
-- 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
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)
⊢ h i = Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
have 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)
Tactic: ext (j | j) (k | k)
-- 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
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)
⊢ h i = Matrix.diagonal (Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
have 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)
Tactic: ext (j | j) (k | k)
-- 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
⊢ 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 : ι))
have 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) ∘
        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: ext
-- 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
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) ∘
        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)
have 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)
Tactic: rw [comp_apply, h_def]
-- 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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : P.IsRootSystem
⊢ LinearIndependent (ι := ↥b.support) R h
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 : ι))
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
-- 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 (ι := ↥b.support) R h
have 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)
Tactic: apply LinearIndependent.of_comp (Matrix.diagLinearMap _ _ _)
-- 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 (ι := ↥b.support) R (M := ↥b.support ⊕ ι → R)
    ((⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) :
        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → ↥b.support ⊕ ι → R) ∘
      h)
have rw : LinearIndependent ℤ (M := ι → ℤ) fun (i : ↥b.support) (x : ι) ↦ P.pairingIn ℤ x (↑i : ι)
Tactic: rw [this, LinearMap.linearIndependent_iff_of_injOn _ Sum.elim_injective'.injOn,
    linearIndependent_algebraMap_comp_iff]