awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
this : ∀ (k : ι), P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k
⊢ (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
have h : ∀ (x : ↥b.support), P.pairingIn ℤ i (↑x : ι) = (f' ᵥ* b.cartanMatrix) x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
this : ∀ (k : ι), P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k
x : ↥b.support
tauto tauto₁ : ∀ (x : ι), x ∈ b.support ↔ x ∈ b.support
⊢ ∀ (x : ι), x ∈ b.support ↔ x ∈ b.support
have mp : ∀ x ∈ b.support, x ∈ b.support
Tactic: tauto
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
⊢ (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
have suffices : ∀ (k : ι), P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k
Tactic: suffices ∀ k, P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k by
      ext; simp [f', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
⊢ ∀ (k : ι), P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k
have refine : ∀ (k : ι),
  Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i k) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ l ∈ b.support, f l * P.pairingIn ℤ l k) : R)
Tactic: refine fun k ↦ algebraMap_injective ℤ R ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
k : ι
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i k) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ l ∈ b.support, f l * P.pairingIn ℤ l k) : R)
have simp_rw : Eq.{u_2 + 1} (α := R) ((P.coroot' k : (a : M) → R) ((P.root : (a : ι) → M) i : M) : R)
  (∑ x ∈ b.support,
      HMul.hMul (α := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) (f x) : R)
        ((P.coroot' k : (a : M) → R) ((P.root : (a : ι) → M) x : M) : R) :
    R)
Tactic: simp_rw [algebraMap_pairingIn, map_sum, map_mul, algebraMap_pairingIn,
      ← P.root_coroot'_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
⊢ f' = g'
have hf₁ : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
Tactic: replace hf : (fun k : b.support ↦ P.pairingIn ℤ i k) = f' ᵥ* b.cartanMatrix := by
    suffices ∀ k, P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k by
      ext; simp [f', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]
    refine fun k ↦ algebraMap_injective ℤ R ?_
    simp_rw [algebraMap_pairingIn, map_sum, map_mul, algebraMap_pairingIn,
      ← P.root_coroot'_eq_pairing]
    simp [hf]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
this : ∀ (k : ι), P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k
⊢ (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix
have h : ∀ (x : ↥b.support), P.pairingIn ℤ j (↑x : ι) = (g' ᵥ* b.cartanMatrix) x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
this : ∀ (k : ι), P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k
x : ↥b.support
tauto tauto₁ : ∀ (x : ι), x ∈ b.support ↔ x ∈ b.support
⊢ ∀ (x : ι), x ∈ b.support ↔ x ∈ b.support
have mp : ∀ x ∈ b.support, x ∈ b.support
Tactic: tauto
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
⊢ (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix
have suffices : ∀ (k : ι), P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k
Tactic: suffices ∀ k, P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k by
      ext; simp [g', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
⊢ ∀ (k : ι), P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k
have refine : ∀ (k : ι),
  Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ j k) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ l ∈ b.support, g l * P.pairingIn ℤ l k) : R)
Tactic: refine fun k ↦ algebraMap_injective ℤ R ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
k : ι
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ j k) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ l ∈ b.support, g l * P.pairingIn ℤ l k) : R)
have simp_rw : Eq.{u_2 + 1} (α := R) ((P.coroot' k : (a : M) → R) ((P.root : (a : ι) → M) j : M) : R)
  (∑ x ∈ b.support,
      HMul.hMul (α := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) (g x) : R)
        ((P.coroot' k : (a : M) → R) ((P.root : (a : ι) → M) x : M) : R) :
    R)
Tactic: simp_rw [algebraMap_pairingIn, map_sum, map_mul, algebraMap_pairingIn,
      ← P.root_coroot'_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
⊢ f' = g'
have hg₁ : (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix
Tactic: replace hg : (fun k : b.support ↦ P.pairingIn ℤ j k) = g' ᵥ* b.cartanMatrix := by
    suffices ∀ k, P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k by
      ext; simp [g', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]
    refine fun k ↦ algebraMap_injective ℤ R ?_
    simp_rw [algebraMap_pairingIn, map_sum, map_mul, algebraMap_pairingIn,
      ← P.root_coroot'_eq_pairing]
    simp [hg]
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f g : ι → ℤ
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
hg : (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix
⊢ f' = g'
have suffices : Injective (β := ↥b.support → ℤ) fun (v : ↥b.support → ℤ) ↦ v ᵥ* b.cartanMatrix
Tactic: suffices Injective fun v ↦ v ᵥ* b.cartanMatrix from this <| by simpa [← hf, ← hg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f g : ι → ℤ
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
hg : (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix
⊢ Injective (β := ↥b.support → ℤ) fun (v : ↥b.support → ℤ) ↦ v ᵥ* b.cartanMatrix
have rw : LinearIndependent ℤ b.cartanMatrix.row
Tactic: rw [Matrix.vecMul_injective_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f g : ι → ℤ
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
hg : (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix
⊢ LinearIndependent ℤ b.cartanMatrix.row
have hA : Matrix.det b.cartanMatrix.row ≠ 0
Tactic: apply Matrix.linearIndependent_rows_of_det_ne_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
i j : ι
hij :
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
    ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) j)
f g : ι → ℤ
f' : ↥b.support → ℤ := f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
g' : ↥b.support → ℤ := g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support)
hf : (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix
hg : (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix
⊢ Matrix.det b.cartanMatrix.row ≠ 0
have hA : Matrix.Nondegenerate b.cartanMatrix.row
Tactic: rw [← Matrix.nondegenerate_iff_det_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : Finite ι
P : RootPairing ι R M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
⊢ Injective (β := (k : ↥b.support) → ℤ) fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)
have intro : ∀ ⦃i a₂ : ι⦄,
  Eq.{u_1 + 1} (α := (k : ↥b.support) → ℤ) ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) i)
      ((fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) a₂) →
    i = a₂
Tactic: classical
  intro i j hij
  obtain ⟨f, -, -, hf⟩ := b.exists_root_eq_sum_int i
  obtain ⟨g, -, -, hg⟩ := b.exists_root_eq_sum_int j
  let f' : b.support → ℤ := f ∘ (↑)
  let g' : b.support → ℤ := g ∘ (↑)
  suffices f' = g' by
    rw [← P.root.apply_eq_iff_eq, hf, hg]
    refine Finset.sum_congr rfl fun k hk ↦ ?_
    replace this : f k = g k := congr_fun this ⟨k, hk⟩
    rw [this]
  replace hf : (fun k : b.support ↦ P.pairingIn ℤ i k) = f' ᵥ* b.cartanMatrix := by
    suffices ∀ k, P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k by
      ext; simp [f', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]
    refine fun k ↦ algebraMap_injective ℤ R ?_
    simp_rw [algebraMap_pairingIn, map_sum, map_mul, algebraMap_pairingIn,
      ← P.root_coroot'_eq_pairing]
    simp [hf]
  replace hg : (fun k : b.support ↦ P.pairingIn ℤ j k) = g' ᵥ* b.cartanMatrix := by
    suffices ∀ k, P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k by
      ext; simp [g', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]
    refine fun k ↦ algebraMap_injective ℤ R ?_
    simp_rw [algebraMap_pairingIn, map_sum, map_mul, algebraMap_pairingIn,
      ← P.root_coroot'_eq_pairing]
    simp [hg]
  suffices Injective fun v ↦ v ᵥ* b.cartanMatrix from this <| by simpa [← hf, ← hg]
  rw [Matrix.vecMul_injective_iff]
  apply Matrix.linearIndependent_rows_of_det_ne_zero
  rw [← Matrix.nondegenerate_iff_det_ne_zero]
  exact b.cartanMatrix_nondegenerate