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 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
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)
⊢ ∀ (k : ι), P.pairingIn ℤ j k = ∑ l ∈ b.support, g 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 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 : ι
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)
⊢ 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:
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 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.{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 [hg]
-- 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
⊢ (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]
-- 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 : ι → ℤ
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
this : Injective (β := ↥b.support → ℤ) fun (v : ↥b.support → ℤ) ↦ v ᵥ* b.cartanMatrix
⊢ Eq.{max (u_1 + 1) 1} (α := ↥b.support → ℤ) ((fun (v : ↥b.support → ℤ) ↦ v ᵥ* b.cartanMatrix) f')
    ((fun (v : ↥b.support → ℤ) ↦ v ᵥ* b.cartanMatrix) g')

Tactic:
simpa [← hf, ← hg]
-- 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 : ι → ℤ
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
suffices : Injective (β := ↥b.support → ℤ) fun (v : ↥b.support → ℤ) ↦ v ᵥ* b.cartanMatrix
⊢ f' = g'

Tactic:
suffices Injective fun v ↦ v ᵥ* b.cartanMatrix from this <| by simpa [← hf, ← hg]
-- 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 : ι → ℤ
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
rw : LinearIndependent ℤ b.cartanMatrix.row
⊢ Injective (β := ↥b.support → ℤ) fun (v : ↥b.support → ℤ) ↦ v ᵥ* b.cartanMatrix

Tactic:
rw [Matrix.vecMul_injective_iff]

Premises used: Matrix.vecMul_injective_iff
-- 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 : ι → ℤ
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
hA : Matrix.det b.cartanMatrix.row ≠ 0
⊢ LinearIndependent ℤ b.cartanMatrix.row

Tactic:
apply Matrix.linearIndependent_rows_of_det_ne_zero

Premises used: Matrix.linearIndependent_rows_of_det_ne_zero
-- 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 : ι → ℤ
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
hA : Matrix.Nondegenerate b.cartanMatrix.row
⊢ Matrix.det b.cartanMatrix.row ≠ 0

Tactic:
rw [← Matrix.nondegenerate_iff_det_ne_zero]

Premises used: Matrix.nondegenerate_iff_det_ne_zero
-- 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 : ι → ℤ
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.Nondegenerate b.cartanMatrix.row

Tactic:
b.cartanMatrix_nondegenerate

Premises used: RootPairing.Base.cartanMatrixIn, RootPairing.Base.cartanMatrix_nondegenerate, Matrix.row
-- 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 : ι → ℤ
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.Nondegenerate b.cartanMatrix.row

Tactic:
exact b.cartanMatrix_nondegenerate

Premises used: RootPairing.Base.cartanMatrix_nondegenerate
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
set :
  let p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K));
  ∃ d ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
⊢ ∃ (d : (j : ι) → K),
    Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)

Tactic:
set p := span K (range fun (i : b.support) j ↦ (P.pairingIn ℤ j i : K))

Premises used: Int.cast, RootPairing.pairingIn, Int, Submodule.span, Set.range, Subtype.val
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
this :
  ∃ d ∈ p,
    ∀
      (i :
        ι ⊕
          (↑{x : ι × ι |
                match (motive := ι × ι → Prop) x with
                | (i, j) => i ≠ j} :
            Type u_1)),
      Ne.{u_6 + 1} (α := K) ((f i : (a : ι → K) → K) d : K) (0 : K)
obtain :
  ∀ (d : (j : ι) → K) (hp : d ∈ p)
    (hf :
      ∀
        (i :
          ι ⊕
            (↑{x : ι × ι |
                  match (motive := ι × ι → Prop) x with
                  | (i, j) => i ≠ j} :
              Type u_1)),
        Ne.{u_6 + 1} (α := K) ((f i : (a : ι → K) → K) d : K) (0 : K)),
    ∃ d ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
⊢ ∃ d ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)

Tactic:
obtain ⟨d, hp, hf⟩ := this
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
d : (j : ι) → K
hp : d ∈ p
hf :
  ∀
    (i :
      ι ⊕
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)),
    Ne.{u_6 + 1} (α := K) ((f i : (a : ι → K) → K) d : K) (0 : K)
⊢ ∃ d ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)

Tactic:
⟨d, hp, fun i ↦ hf (Sum.inl i), fun i j h ↦ ?_⟩

Premises used: Sum.inl, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
d : (j : ι) → K
hp : d ∈ p
hf :
  ∀
    (i :
      ι ⊕
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)),
    Ne.{u_6 + 1} (α := K) ((f i : (a : ι → K) → K) d : K) (0 : K)
refine : ∀ (i j : ι) (h : i ≠ j), ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) i j
⊢ ∃ d ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)

Tactic:
refine ⟨d, hp, fun i ↦ hf (Sum.inl i), fun i j h ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
d : (j : ι) → K
hp : d ∈ p
hf :
  ∀
    (i :
      ι ⊕
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)),
    Ne.{u_6 + 1} (α := K) ((f i : (a : ι → K) → K) d : K) (0 : K)
i j : ι
h : i ≠ j
⊢ ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) i j

Tactic:
simpa [f, sub_eq_zero] using hf (Sum.inr ⟨⟨i, j⟩, h⟩)

Premises used: sub_eq_zero, Prod.mk, Subtype.mk, Sum.inr
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
suffices :
  ∃ d ∈ p,
    ∀
      (i :
        ι ⊕
          (↑{x : ι × ι |
                match (motive := ι × ι → Prop) x with
                | (i, j) => i ≠ j} :
            Type u_1)),
      Ne.{u_6 + 1} (α := K) ((f i : (a : ι → K) → K) d : K) (0 : K)
⊢ ∃ d ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)

Tactic:
suffices ∃ d ∈ p, ∀ i, f i d ≠ 0 by
    obtain ⟨d, hp, hf⟩ := this
    refine ⟨d, hp, fun i ↦ hf (Sum.inl i), fun i j h ↦ ?_⟩
    simpa [f, sub_eq_zero] using hf (Sum.inr ⟨⟨i, j⟩, h⟩)
-- Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Finite ι
K : Type u_6
inst_3 : Field K
inst_4 : CharZero K
inst_5 : Module K M
inst_6 : Module K N
P : RootPairing ι K M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
b : P.Base
p : Submodule K ((j : ι) → K) := span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))
f : ι ⊕
    (↑{x : ι × ι |
          match (motive := ι × ι → Prop) x with
          | (i, j) => i ≠ j} :
      Type u_1) →
  Module.Dual K (ι → K) :=
  Sum.elim (LinearMap.proj (φ := fun (a : ι) ↦ K))
    fun
      (x :
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)) ↦
    HSub.hSub (α := ((i : ι) → K) →ₗ[K] K) (β := ((i : ι) → K) →ₗ[K] K)
      (LinearMap.proj (φ := fun (x : ι) ↦ K) (↑x : ι × ι).1) (LinearMap.proj (φ := fun (i : ι) ↦ K) (↑x : ι × ι).2)
apply :
  ∀
    (i :
      ι ⊕
        (↑{x : ι × ι |
              match (motive := ι × ι → Prop) x with
              | (i, j) => i ≠ j} :
          Type u_1)),
    ∃ x ∈ p, Ne.{u_6 + 1} (α := K) ((f i : (a : (j : ι) → K) → K) x : K) (0 : K)
⊢ ∃ d ∈ p,
    ∀
      (i :
        ι ⊕
          (↑{x : ι × ι |
                match (motive := ι × ι → Prop) x with
                | (i, j) => i ≠ j} :
            Type u_1)),
      Ne.{u_6 + 1} (α := K) ((f i : (a : ι → K) → K) d : K) (0 : K)

Tactic:
apply Module.Dual.exists_forall_mem_ne_zero_of_forall_exists p f

Premises used: Module.Dual.exists_forall_mem_ne_zero_of_forall_exists