awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
a : ∀ (k l : ↥b.support), ⁅e i, f i⁆ (Sum.inl k) (Sum.inl l) = h i (Sum.inl k) (Sum.inl l)
⊢ ⁅e i, f i⁆ = h i
have a₁ : ∀ (k : ↥b.support) (l : ι), ⁅e i, f i⁆ (Sum.inl k) (Sum.inr l) = h i (Sum.inl k) (Sum.inr l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [e, f, h]
  · have h₁ (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ k = i ∧ x = -i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero, sub_eq_add_neg] at contra
    have h₂ (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ k = i ∧ x = i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero] at contra
    simp [e, f, h, h₁, h₂, -indexNeg_neg, ← ite_and]
  · simp [e, f, h]
  · rcases eq_or_ne k i with rfl | hki
    · have hx (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ P.root i = P.root x - P.root i) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := i) ⟨x, ?_⟩
        rwa [eq_sub_iff_add_eq, ← two_smul ℕ, eq_comm] at contra
      simp only [e, f, h, P.ne_zero, P.ne_neg, Ring.lie_def, Fintype.sum_sum_type, Matrix.sub_apply,
        Matrix.mul_apply, Matrix.fromBlocks_apply₂₁, Matrix.of_apply, Matrix.fromBlocks_apply₂₂,
        left_eq_add, zero_mul, mul_zero, ite_mul, mul_ite, ← ite_and]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [hx, eq_comm]
    rcases eq_or_ne k (-i) with rfl | hki'
    · have hx (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ P.root (-i) = P.root i + P.root x) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := -i) ⟨x, ?_⟩
        replace contra : P.root x = -(P.root i + P.root i) := by
          simpa [neg_eq_iff_add_eq_zero, ← add_assoc, add_eq_zero_iff_eq_neg'] using contra
        simp [contra, two_smul]
      have aux (x : ι) : ¬ P.root (-i) = P.root x - P.root i := by
        simp [P.ne_zero x, eq_comm]
      simp only [e, f, h, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
        Matrix.fromBlocks_apply₂₁, Matrix.of_apply, hki, reduceIte, zero_mul, Finset.sum_const_zero,
        Matrix.fromBlocks_apply₂₂, mul_ite, ite_mul, mul_zero, ← ite_and, if_neg (hx _), add_zero,
        aux, zero_sub, Matrix.diagonal_apply]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [eq_comm, apply_ite ((-·) : R → R)]
    rcases eq_or_ne k l with rfl | hkl
    · exact lie_e_f_same_aux i k hki hki'
    · simp_all [h, e, f]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
a : ∀ (k l : ↥b.support), ⁅e i, f i⁆ (Sum.inl k) (Sum.inl l) = h i (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), ⁅e i, f i⁆ (Sum.inl k) (Sum.inr l) = h i (Sum.inl k) (Sum.inr l)
⊢ ⁅e i, f i⁆ = h i
have a₂ : ∀ (k : ι) (l : ↥b.support), ⁅e i, f i⁆ (Sum.inr k) (Sum.inl l) = h i (Sum.inr k) (Sum.inl l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [e, f, h]
  · have h₁ (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ k = i ∧ x = -i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero, sub_eq_add_neg] at contra
    have h₂ (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ k = i ∧ x = i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero] at contra
    simp [e, f, h, h₁, h₂, -indexNeg_neg, ← ite_and]
  · simp [e, f, h]
  · rcases eq_or_ne k i with rfl | hki
    · have hx (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ P.root i = P.root x - P.root i) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := i) ⟨x, ?_⟩
        rwa [eq_sub_iff_add_eq, ← two_smul ℕ, eq_comm] at contra
      simp only [e, f, h, P.ne_zero, P.ne_neg, Ring.lie_def, Fintype.sum_sum_type, Matrix.sub_apply,
        Matrix.mul_apply, Matrix.fromBlocks_apply₂₁, Matrix.of_apply, Matrix.fromBlocks_apply₂₂,
        left_eq_add, zero_mul, mul_zero, ite_mul, mul_ite, ← ite_and]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [hx, eq_comm]
    rcases eq_or_ne k (-i) with rfl | hki'
    · have hx (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ P.root (-i) = P.root i + P.root x) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := -i) ⟨x, ?_⟩
        replace contra : P.root x = -(P.root i + P.root i) := by
          simpa [neg_eq_iff_add_eq_zero, ← add_assoc, add_eq_zero_iff_eq_neg'] using contra
        simp [contra, two_smul]
      have aux (x : ι) : ¬ P.root (-i) = P.root x - P.root i := by
        simp [P.ne_zero x, eq_comm]
      simp only [e, f, h, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
        Matrix.fromBlocks_apply₂₁, Matrix.of_apply, hki, reduceIte, zero_mul, Finset.sum_const_zero,
        Matrix.fromBlocks_apply₂₂, mul_ite, ite_mul, mul_zero, ← ite_and, if_neg (hx _), add_zero,
        aux, zero_sub, Matrix.diagonal_apply]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [eq_comm, apply_ite ((-·) : R → R)]
    rcases eq_or_ne k l with rfl | hkl
    · exact lie_e_f_same_aux i k hki hki'
    · simp_all [h, e, f]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
a : ∀ (k l : ↥b.support), ⁅e i, f i⁆ (Sum.inl k) (Sum.inl l) = h i (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), ⁅e i, f i⁆ (Sum.inl k) (Sum.inr l) = h i (Sum.inl k) (Sum.inr l)
a₂ : ∀ (k : ι) (l : ↥b.support), ⁅e i, f i⁆ (Sum.inr k) (Sum.inl l) = h i (Sum.inr k) (Sum.inl l)
⊢ ⁅e i, f i⁆ = h i
have a₃ : ∀ (k l : ι), ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [e, f, h]
  · have h₁ (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ k = i ∧ x = -i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero, sub_eq_add_neg] at contra
    have h₂ (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ k = i ∧ x = i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero] at contra
    simp [e, f, h, h₁, h₂, -indexNeg_neg, ← ite_and]
  · simp [e, f, h]
  · rcases eq_or_ne k i with rfl | hki
    · have hx (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ P.root i = P.root x - P.root i) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := i) ⟨x, ?_⟩
        rwa [eq_sub_iff_add_eq, ← two_smul ℕ, eq_comm] at contra
      simp only [e, f, h, P.ne_zero, P.ne_neg, Ring.lie_def, Fintype.sum_sum_type, Matrix.sub_apply,
        Matrix.mul_apply, Matrix.fromBlocks_apply₂₁, Matrix.of_apply, Matrix.fromBlocks_apply₂₂,
        left_eq_add, zero_mul, mul_zero, ite_mul, mul_ite, ← ite_and]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [hx, eq_comm]
    rcases eq_or_ne k (-i) with rfl | hki'
    · have hx (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ P.root (-i) = P.root i + P.root x) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := -i) ⟨x, ?_⟩
        replace contra : P.root x = -(P.root i + P.root i) := by
          simpa [neg_eq_iff_add_eq_zero, ← add_assoc, add_eq_zero_iff_eq_neg'] using contra
        simp [contra, two_smul]
      have aux (x : ι) : ¬ P.root (-i) = P.root x - P.root i := by
        simp [P.ne_zero x, eq_comm]
      simp only [e, f, h, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
        Matrix.fromBlocks_apply₂₁, Matrix.of_apply, hki, reduceIte, zero_mul, Finset.sum_const_zero,
        Matrix.fromBlocks_apply₂₂, mul_ite, ite_mul, mul_zero, ← ite_and, if_neg (hx _), add_zero,
        aux, zero_sub, Matrix.diagonal_apply]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [eq_comm, apply_ite ((-·) : R → R)]
    rcases eq_or_ne k l with rfl | hkl
    · exact lie_e_f_same_aux i k hki hki'
    · simp_all [h, e, f]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i : ↥b.support
inst_10 : P.IsReduced
inst_11 : DecidableEq ι
⊢ ⁅e i, f i⁆ = h i
have rw : h i = h i
Tactic: rw [lie_e_f_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i : ↥b.support
inst_10 : P.IsReduced
inst_11 : DecidableEq ι
⊢ ⁅h i, e i⁆ = HSMul.hSMul (α := ℕ) 2 (e i)
have rw : b.cartanMatrix i i • e i = HSMul.hSMul (α := ℕ) 2 (e i)
Tactic: rw [lie_h_e]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i : ↥b.support
inst_10 : P.IsReduced
inst_11 : DecidableEq ι
⊢ ⁅h i, f i⁆ = -HSMul.hSMul (α := ℕ) 2 (f i)
have rw : -b.cartanMatrix i i • f i = -HSMul.hSMul (α := ℕ) 2 (f i)
Tactic: rw [lie_h_f]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j k : ↥b.support
l : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
have aux₁ : ∀ (x : ι),
  Membership.mem (γ := Finset ι) Finset.univ x →
    ¬((P.root : (a : ι) → M) x =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
        k = j ∧ x = (↑j : ι))
Tactic: have aux₁ : ∀ x ∈ Finset.univ, ¬ (P.root x = P.root i + P.root l ∧ k = j ∧ x = j) := by
    rintro x - ⟨hl, -, rfl⟩
    exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j k : ↥b.support
l : ι
this : InvolutiveNeg ι := P.indexNeg
aux₁ :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      ¬((P.root : (a : ι) → M) x =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
          k = j ∧ x = (↑j : ι))
hl :
  (P.root : (a : ι) → M) (-(↑i : ι)) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M)
⊢ False
have hl₁ : (P.root : (a : ι) → M) (↑i : ι) =
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) (↑j : ι) : M) ((P.root : (a : ι) → M) l : M)
Tactic: replace hl : P.root i = P.root j - P.root l := by simpa [neg_eq_iff_eq_neg] using hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j k : ↥b.support
l : ι
this : InvolutiveNeg ι := P.indexNeg
aux₁ :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      ¬((P.root : (a : ι) → M) x =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
          k = j ∧ x = (↑j : ι))
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
have aux₂ : ∀ (x : ι),
  Membership.mem (γ := Finset ι) Finset.univ x →
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
        k = i ∧ x = -(↑i : ι))
Tactic: have aux₂ : ∀ x ∈ Finset.univ, ¬ (P.root x = P.root l - P.root j ∧ k = i ∧ x = -i) := by
    rintro x - ⟨hl, -, rfl⟩
    replace hl : P.root i = P.root j - P.root l := by simpa [neg_eq_iff_eq_neg] using hl
    exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j k : ↥b.support
l : ι
letI letI₁ letI₂ : ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
have letI₃ : ∀
  (aux₁ :
    ∀ (x : ι),
      Membership.mem (γ := Finset ι) Finset.univ x →
        ¬((P.root : (a : ι) → M) x =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
            k = j ∧ x = (↑j : ι))),
  ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
Tactic: classical
  letI := P.indexNeg
  have aux₁ : ∀ x ∈ Finset.univ, ¬ (P.root x = P.root i + P.root l ∧ k = j ∧ x = j) := by
    rintro x - ⟨hl, -, rfl⟩
    exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩
  have aux₂ : ∀ x ∈ Finset.univ, ¬ (P.root x = P.root l - P.root j ∧ k = i ∧ x = -i) := by
    rintro x - ⟨hl, -, rfl⟩
    replace hl : P.root i = P.root j - P.root l := by simpa [neg_eq_iff_eq_neg] using hl
    exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩
  simp [e, f, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux₁, Finset.sum_ite_of_false aux₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j k : ↥b.support
l : ι
letI letI₁ letI₂ : ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
letI₃ :
  ∀
    (aux₁ :
      ∀ (x : ι),
        Membership.mem (γ := Finset ι) Finset.univ x →
          ¬((P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
              k = j ∧ x = (↑j : ι))),
    ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
have letI₄ : let this := P.indexNeg;
∀
  (aux₁ :
    ∀ (x : ι),
      Membership.mem (γ := Finset ι) Finset.univ x →
        ¬((P.root : (a : ι) → M) x =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
            k = j ∧ x = (↑j : ι)))
  (aux₂ :
    ∀ (x : ι),
      Membership.mem (γ := Finset ι) Finset.univ x →
        ¬((P.root : (a : ι) → M) x =
              HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
            k = i ∧ x = -(↑i : ι))),
  ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0
Tactic: classical
  letI := P.indexNeg
  have aux₁ : ∀ x ∈ Finset.univ, ¬ (P.root x = P.root i + P.root l ∧ k = j ∧ x = j) := by
    rintro x - ⟨hl, -, rfl⟩
    exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩
  have aux₂ : ∀ x ∈ Finset.univ, ¬ (P.root x = P.root l - P.root j ∧ k = i ∧ x = -i) := by
    rintro x - ⟨hl, -, rfl⟩
    replace hl : P.root i = P.root j - P.root l := by simpa [neg_eq_iff_eq_neg] using hl
    exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩
  simp [e, f, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux₁, Finset.sum_ite_of_false aux₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) = 0
have hij' : (↑i : ι) ≠ (↑j : ι)
Tactic: have hij' : (i : ι) ≠ (j : ι) := hij ∘ SetLike.coe_eq_coe.mp
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) = 0
have h : ∀ (k : ↥b.support), ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inl k) = 0 (Sum.inl k)
Tactic: ext (k | k)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
h : ∀ (k : ↥b.support), ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inl k) = 0 (Sum.inl k)
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) = 0
have h₁ : ∀ (k : ι), ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inr k) = 0 (Sum.inr k)
Tactic: ext (k | k)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inl k) = 0 (Sum.inl k)
have h : ⁅e i, f j⁆ (Sum.inl k) (Sum.inr (↑j : ι)) = 0 (Sum.inl k)
Tactic: rw [Matrix.transpose_apply, lie_e_f_ne_aux₀, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
h : ⁅e i, f j⁆ (Sum.inl k) (Sum.inr (↑j : ι)) = 0 (Sum.inl k)
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inl k) = 0 (Sum.inl k)
have h₁ : Eq.{u_2 + 1} (α := R) 0 (0 (Sum.inl k))
Tactic: rw [Matrix.transpose_apply, lie_e_f_ne_aux₀, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
h : ⁅e i, f j⁆ (Sum.inl k) (Sum.inr (↑j : ι)) = 0 (Sum.inl k)
h₁ : Eq.{u_2 + 1} (α := R) 0 (0 (Sum.inl k))
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inl k) = 0 (Sum.inl k)
have h₂ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [Matrix.transpose_apply, lie_e_f_ne_aux₀, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : (↑i : ι) ≠ (↑j : ι)
this_1 : InvolutiveNeg ι := P.indexNeg
k : ι
this :
  HSub.hSub (α := R) (if k = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                  ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
              (P.root : (a : ι) → M) k =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) x) : R)
            1
        else 0) =
    0
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inr k) = 0 (Sum.inr k)
have hij₁ : (↑j : ι) ≠ -(↑i : ι)
Tactic: have hij : (j : ι) ≠ -i := by simpa using b.root_ne_neg_of_ne j.property i.property hij'.symm