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
intro intro₁ intro₂ :
  ∀ ⦃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)),
    i = j
⊢ Injective (β := (k : ↥b.support) → ℤ) fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)
have intro₃ : ∀ ⦃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)),
  i = j
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
-- 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
intro intro₁ intro₂ :
  ∀ ⦃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)),
    i = j
intro₃ :
  ∀ ⦃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)),
    i = j
⊢ Injective (β := (k : ↥b.support) → ℤ) fun (i : ι) (k : ↥b.support) ↦ P.pairingIn ℤ i (↑k : ι)
have intro₄ : ∀ ⦃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)),
  i = j
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
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)
⊢ ∃ d ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
have 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)
Tactic: obtain ⟨d, hp, hf⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
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)
have refine : ∀ (i j : ι) (h : i ≠ j), ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) i j
Tactic: refine ⟨d, hp, fun i ↦ hf (Sum.inl i), fun i j h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
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 ∈ p, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
have 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)
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⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
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 ∈ 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)
have 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)
Tactic: apply Module.Dual.exists_forall_mem_ne_zero_of_forall_exists p f
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
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)
i : ι
⊢ ∃ x ∈ p, Ne.{u_6 + 1} (α := K) ((f (Sum.inl i) : (a : (j : ι) → K) → K) x : K) (0 : K)
have inl : ∀ (j : ι) (hj : j ∈ b.support) (hj₀ : P.pairingIn ℤ j i ≠ 0),
  ∃ x ∈ p, Ne.{u_6 + 1} (α := K) ((f (Sum.inl i) : (a : (j : ι) → K) → K) x : K) (0 : K)
Tactic: obtain ⟨j, hj, hj₀⟩ := b.exists_mem_support_pos_pairingIn_ne_zero i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
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)
i j : ι
hj : j ∈ b.support
hj₀ : P.pairingIn ℤ j i ≠ 0
⊢ ∃ x ∈ p, Ne.{u_6 + 1} (α := K) ((f (Sum.inl i) : (a : (j : ι) → K) → K) x : K) (0 : K)
have inl : Ne.{u_6 + 1} (α := K) ((f (Sum.inl i) : (a : (j : ι) → K) → K) fun (i : ι) ↦ (↑(P.pairingIn ℤ i j) : K) : K) (0 : K)
Tactic: refine ⟨fun i ↦ P.pairingIn ℤ i j, subset_span ⟨⟨j, hj⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (hypothesis)
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)
i j : ι
hj : j ∈ b.support
hj₀ : P.pairingIn ℤ j i ≠ 0
⊢ Ne.{u_6 + 1} (α := K) ((f (Sum.inl i) : (a : (j : ι) → K) → K) fun (i : ι) ↦ (↑(P.pairingIn ℤ i j) : K) : K) (0 : K)
have hj₁ : ¬P.pairingIn ℤ i j = 0
Tactic: rw [ne_eq, P.pairingIn_eq_zero_iff] at hj₀
Cleared hypotheses: hj₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
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)
i j : ι
h : i ≠ j
⊢ ∃ k ∈ b.support, P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k
have contrapose! : ∀ (h : ∀ (k : ι) (_ : k ∈ b.support), P.pairingIn ℤ i k = P.pairingIn ℤ j k), i = j
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
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)
i j : ι
h : ∀ (k : ι) (_ : k ∈ b.support), P.pairingIn ℤ i k = P.pairingIn ℤ j k
⊢ i = j
have 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 : ι)) j)
Tactic: apply b.injective_pairingIn
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (goal)
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)
i j : ι
h : i ≠ j
⊢ ∃ x ∈ p,
    Ne.{u_6 + 1} (α := K)
      ((f
              (Sum.inr
                (Subtype.mk (p := fun (x : ι × ι) ↦
                  Membership.mem (γ := Set (ι × ι))
                    {x : ι × ι |
                      match (motive := ι × ι → Prop) x with
                      | (i, j) => i ≠ j}
                    x)
                  (i, j) h)) :
            (a : (j : ι) → K) → K)
          x :
        K)
      (0 : K)
have inr : ∀ (k : ι) (hk : k ∈ b.support) (hk' : P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k),
  ∃ x ∈ p,
    Ne.{u_6 + 1} (α := K)
      ((f
              (Sum.inr
                (Subtype.mk (p := fun (x : ι × ι) ↦
                  Membership.mem (γ := Set (ι × ι))
                    {x : ι × ι |
                      match (motive := ι × ι → Prop) x with
                      | (i, j) => i ≠ j}
                    x)
                  (i, j) h)) :
            (a : (j : ι) → K) → K)
          x :
        K)
      (0 : K)
Tactic: obtain ⟨k, hk, hk'⟩ : ∃ k ∈ b.support, P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k := by
      contrapose! h
      apply b.injective_pairingIn
      aesop
-- 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 ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : AddCommGroup N₂
inst_11 : Module R N₂
P : RootPairing ι R M N
inst_12 : P.IsRootSystem
inst_13 : P.IsCrystallographic
inst_14 : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst_15 : P₂.IsCrystallographic
b₂ : P₂.Base
e : Equiv.{u_1 + 1, u_6 + 1} ↥b.support ↥b₂.support
f : M ≃ₗ[R] M₂
hf :
  ∀ (i : ↥b.support),
    Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑i : ι) : M) : M₂)
      ((P₂.root : (a : ι₂) → M₂) (↑((e : (a : ↥b.support) → ↥b₂.support) i) : ι₂) : M₂)
m : M
hm : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) m
he :
  ∀ (i j : ↥b.support),
    b₂.cartanMatrix ((e : (a : ↥b.support) → ↥b₂.support) i) ((e : (a : ↥b.support) → ↥b₂.support) j) =
      b.cartanMatrix i j
k : ↥b.support
this :
  ∀ (j : ↥b.support),
    Eq.{u_7 + 1} (α := M₂) ((P.reflection (↑k : ι) ≪≫ₗ f : (a : M) → M₂) ((P.root : (a : ι) → M) (↑j : ι) : M) : M₂)
      ((f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂) : (a : M) → M₂)
          ((P.root : (a : ι) → M) (↑j : ι) : M) :
        M₂)
⊢ Eq (α := M ≃ₗ[R] M₂) (P.reflection (↑k : ι) ≪≫ₗ f)
    (f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂))
have rw : (↑(P.reflection (↑k : ι) ≪≫ₗ f) : M →ₗ[R] M₂) =
  (↑(f ≪≫ₗ P₂.reflection (↑((e : (a : ↥b.support) → ↥b₂.support) k) : ι₂)) : M →ₗ[R] M₂)
Tactic: rw [← LinearEquiv.toLinearMap_inj]