awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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 : f' = g'
refine :
  ∀ (k : ι) (hk : k ∈ b.support),
    HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
      HSMul.hSMul (β := M) (g k) ((P.root : (a : ι) → M) k : M)
⊢ Eq.{u_3 + 1} (α := M) (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M))

Tactic:
refine Finset.sum_congr rfl fun k hk ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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 : f' = g'
k : ι
hk : k ∈ b.support
⊢ f k = g k

Tactic:
replace this : f k = g k := congr_fun this ⟨k, hk⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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 : ι
hk : k ∈ b.support
this : f k = g k
rw rw₁ :
  HSMul.hSMul (β := M) (g k) ((P.root : (a : ι) → M) k : M) = HSMul.hSMul (β := M) (g k) ((P.root : (a : ι) → M) k : M)
⊢ HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) = HSMul.hSMul (β := M) (g k) ((P.root : (a : ι) → M) k : M)

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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)
suffices : f' = g'
⊢ i = j

Tactic:
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]
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
h : ∀ (x : ↥b.support), P.pairingIn ℤ i (↑x : ι) = (f' ᵥ* b.cartanMatrix) x
⊢ (fun (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)) = f' ᵥ* b.cartanMatrix

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
mp mpr mp₁ mp₂ mp₃ mpr₁ mpr₂ mpr₃ : ∀ x ∈ b.support, x ∈ b.support
⊢ ∀ (x : ι), x ∈ b.support ↔ x ∈ b.support

Tactic:
tauto
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
⊢ P.pairingIn ℤ i (↑x : ι) = (f' ᵥ* b.cartanMatrix) x

Tactic:
simp [f', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]

Premises used: RootPairing.Base.cartanMatrixIn, Finset.sum_subtype, RootPairing.Base.support, Matrix.vecMul_eq_sum
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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)
suffices : ∀ (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

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)]
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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

Tactic:
fun k ↦ algebraMap_injective ℤ R ?_

Premises used: Int, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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)
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)
⊢ ∀ (k : ι), P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k

Tactic:
refine fun k ↦ algebraMap_injective ℤ R ?_

Premises used: Int, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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 : ι
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)
⊢ 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:
simp_rw [algebraMap_pairingIn, map_sum, map_mul, algebraMap_pairingIn,
      ← P.root_coroot'_eq_pairing]

Premises used: RootPairing.algebraMap_pairingIn, map_sum, map_mul, RootPairing.root_coroot'_eq_pairing
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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.{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 [hf]
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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

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]
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
h : ∀ (x : ↥b.support), P.pairingIn ℤ j (↑x : ι) = (g' ᵥ* b.cartanMatrix) x
⊢ (fun (k : ↥b.support) ↦ P.pairingIn ℤ j (↑k : ι)) = g' ᵥ* b.cartanMatrix

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
mp mpr mp₁ mp₂ mp₃ mpr₁ mpr₂ mpr₃ : ∀ x ∈ b.support, x ∈ b.support
⊢ ∀ (x : ι), x ∈ b.support ↔ x ∈ b.support

Tactic:
tauto
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
⊢ P.pairingIn ℤ j (↑x : ι) = (g' ᵥ* b.cartanMatrix) x

Tactic:
simp [g', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]

Premises used: RootPairing.Base.cartanMatrixIn, Finset.sum_subtype, RootPairing.Base.support, Matrix.vecMul_eq_sum
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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
suffices : ∀ (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

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)]
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
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

Tactic:
fun k ↦ algebraMap_injective ℤ R ?_

Premises used: Int, FaithfulSMul.algebraMap_injective