awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : InvolutiveNeg ι := P.indexNeg
hij_mem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
⊢ HSub.hSub (α := R) (if (↑i : ι) = (↑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) (↑i : ι) =
                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
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) (↑j : ι) : M) ∧
        (P.root : (a : ι) → M) (↑i : ι) =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M))
Tactic: have aux : ∀ x ∈ Finset.univ,
          ¬ (P.root x = P.root i + P.root j ∧ P.root i = P.root x - P.root j) := by
        rintro x - ⟨hx, -⟩; exact hij_mem ⟨x, hx⟩
-- 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: classical
  ext (k | k)
  · rw [Matrix.transpose_apply, lie_e_f_ne_aux₀, Pi.zero_apply]
  · suffices ((if k = i then ↑|b.cartanMatrix i j| else (0 : R)) -
        ∑ x, if P.root x = P.root i + P.root j ∧ P.root k = P.root x - P.root j then
          (P.chainTopCoeff j x : R) + 1 else 0) = 0 by
      have hij : (j : ι) ≠ -i := by simpa using b.root_ne_neg_of_ne j.property i.property hij'.symm
      have aux : ∀ x ∈ Finset.univ,
        x ≠ j → (if x = j ∧ k = i then ↑|b.cartanMatrix i x| else 0) = (0 : R) := by aesop
      simpa [e, f, P.ne_zero, hij, -indexNeg_neg, -Finset.univ_eq_attach, ← ite_and,
        Finset.sum_eq_single_of_mem j (Finset.mem_univ _) aux]
    rcases eq_or_ne k i with rfl | hk; swap
    · rw [if_neg (by tauto), Finset.sum_ite_of_false (by aesop)]; simp
    by_cases hij_mem : P.root i + P.root j ∈ range P.root
    · obtain ⟨m, hm⟩ := hij_mem
      rw [Finset.sum_eq_single_of_mem m (Finset.mem_univ _) (by rintro x - hx; simp [← hm, hx]),
        b.abs_cartanMatrix_apply, Base.cartanMatrix, Base.cartanMatrixIn_def]
      have aux₁ := b.chainTopCoeff_eq_of_ne hij.symm
      have aux₂ := chainTopCoeff_of_add (b.linearIndependent_pair_of_ne hij.symm) hm
      norm_cast
      aesop
    · have aux : ∀ x ∈ Finset.univ,
          ¬ (P.root x = P.root i + P.root j ∧ P.root i = P.root x - P.root j) := by
        rintro x - ⟨hx, -⟩; exact hij_mem ⟨x, hx⟩
      simp [Finset.sum_ite_of_false aux, b.cartanMatrix_apply_eq_zero_iff hij, hij_mem]
-- 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: classical
  ext (k | k)
  · rw [Matrix.transpose_apply, lie_e_f_ne_aux₀, Pi.zero_apply]
  · suffices ((if k = i then ↑|b.cartanMatrix i j| else (0 : R)) -
        ∑ x, if P.root x = P.root i + P.root j ∧ P.root k = P.root x - P.root j then
          (P.chainTopCoeff j x : R) + 1 else 0) = 0 by
      have hij : (j : ι) ≠ -i := by simpa using b.root_ne_neg_of_ne j.property i.property hij'.symm
      have aux : ∀ x ∈ Finset.univ,
        x ≠ j → (if x = j ∧ k = i then ↑|b.cartanMatrix i x| else 0) = (0 : R) := by aesop
      simpa [e, f, P.ne_zero, hij, -indexNeg_neg, -Finset.univ_eq_attach, ← ite_and,
        Finset.sum_eq_single_of_mem j (Finset.mem_univ _) aux]
    rcases eq_or_ne k i with rfl | hk; swap
    · rw [if_neg (by tauto), Finset.sum_ite_of_false (by aesop)]; simp
    by_cases hij_mem : P.root i + P.root j ∈ range P.root
    · obtain ⟨m, hm⟩ := hij_mem
      rw [Finset.sum_eq_single_of_mem m (Finset.mem_univ _) (by rintro x - hx; simp [← hm, hx]),
        b.abs_cartanMatrix_apply, Base.cartanMatrix, Base.cartanMatrixIn_def]
      have aux₁ := b.chainTopCoeff_eq_of_ne hij.symm
      have aux₂ := chainTopCoeff_of_add (b.linearIndependent_pair_of_ne hij.symm) hm
      norm_cast
      aesop
    · have aux : ∀ x ∈ Finset.univ,
          ¬ (P.root x = P.root i + P.root j ∧ P.root i = P.root x - P.root j) := by
        rintro x - ⟨hx, -⟩; exact hij_mem ⟨x, hx⟩
      simp [Finset.sum_ite_of_false aux, b.cartanMatrix_apply_eq_zero_iff hij, hij_mem]
-- 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
this : InvolutiveNeg ι := P.indexNeg
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) = 0
have h : ∀ (k : ↥b.support), ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (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
this : InvolutiveNeg ι := P.indexNeg
h : ∀ (k : ↥b.support), ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (Sum.inl k) = 0 (Sum.inl k)
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) = 0
have h₁ : ∀ (k : ι), ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (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
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (Sum.inl k) = 0 (Sum.inl k)
have h : ⁅e i, f j⁆ (Sum.inl k) (Sum.inr (-(↑i : ι))) = 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
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
h : ⁅e i, f j⁆ (Sum.inl k) (Sum.inr (-(↑i : ι))) = 0 (Sum.inl k)
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (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
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
h : ⁅e i, f j⁆ (Sum.inl k) (Sum.inr (-(↑i : ι))) = 0 (Sum.inl k)
h₁ : Eq.{u_2 + 1} (α := R) 0 (0 (Sum.inl k))
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (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
this : InvolutiveNeg ι := P.indexNeg
k : ι
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (Sum.inr k) = 0 (Sum.inr k)
have aux : ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-(↑i : ι))) = (⁅e i, f j⁆ * ω b) (Sum.inr k) (Sum.inr (↑i : ι))
Tactic: have aux : ⁅e i, f j⁆ (.inr k) (.inr (-i)) = (⁅e i, f j⁆ * ω b) (.inr k) (.inr i) := by simp [ω]
-- 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
this : InvolutiveNeg ι := P.indexNeg
k : ι
aux : ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-(↑i : ι))) = (⁅e i, f j⁆ * ω b) (Sum.inr k) (Sum.inr (↑i : ι))
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (Sum.inr k) = 0 (Sum.inr k)
have h : Eq.{u_2 + 1} (α := R) (0 ⬝ᵥ fun (j : ↥b.support ⊕ ι) ↦ (-ω b)ᵀ j (Sum.inr k)) (0 (Sum.inr k))
Tactic: rw [Matrix.transpose_apply, aux, lie_e_f_mul_ω, ← (-ω b * ⁅e j, f i⁆).transpose_apply,
      Matrix.transpose_mul, Matrix.mul_apply', lie_e_f_ne_aux₁ hij.symm]
-- 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
this : InvolutiveNeg ι := P.indexNeg
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) = 0
have h : ∀ (k : ↥b.support), ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (Sum.inl k) = 0 (Sum.inl k)
Tactic: classical
  ext (k | k)
  · rw [Matrix.transpose_apply, lie_e_f_ne_aux₀, Pi.zero_apply]
  · have aux : ⁅e i, f j⁆ (.inr k) (.inr (-i)) = (⁅e i, f j⁆ * ω b) (.inr k) (.inr i) := by simp [ω]
    rw [Matrix.transpose_apply, aux, lie_e_f_mul_ω, ← (-ω b * ⁅e j, f i⁆).transpose_apply,
      Matrix.transpose_mul, Matrix.mul_apply', lie_e_f_ne_aux₁ hij.symm]
    simp
-- 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
this : InvolutiveNeg ι := P.indexNeg
h : ∀ (k : ↥b.support), ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (Sum.inl k) = 0 (Sum.inl k)
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) = 0
have h₁ : ∀ (k : ι), ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (Sum.inr k) = 0 (Sum.inr k)
Tactic: classical
  ext (k | k)
  · rw [Matrix.transpose_apply, lie_e_f_ne_aux₀, Pi.zero_apply]
  · have aux : ⁅e i, f j⁆ (.inr k) (.inr (-i)) = (⁅e i, f j⁆ * ω b) (.inr k) (.inr i) := by simp [ω]
    rw [Matrix.transpose_apply, aux, lie_e_f_mul_ω, ← (-ω b * ⁅e j, f i⁆).transpose_apply,
      Matrix.transpose_mul, Matrix.mul_apply', lie_e_f_ne_aux₁ hij.symm]
    simp
-- 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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
⊢ ⁅e i, f 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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
⊢ ⁅e i, f j⁆ = 0
have a : ∀ (k l : ↥b.support), ⁅e i, f j⁆ (Sum.inl k) (Sum.inl l) = 0 (Sum.inl k) (Sum.inl l)
Tactic: ext (k | k) (l | l)
-- 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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
a : ∀ (k l : ↥b.support), ⁅e i, f j⁆ (Sum.inl k) (Sum.inl l) = 0 (Sum.inl k) (Sum.inl l)
⊢ ⁅e i, f j⁆ = 0
have a₁ : ∀ (k : ↥b.support) (l : ι), ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0 (Sum.inl k) (Sum.inr l)
Tactic: ext (k | k) (l | l)
-- 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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
a : ∀ (k l : ↥b.support), ⁅e i, f j⁆ (Sum.inl k) (Sum.inl l) = 0 (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0 (Sum.inl k) (Sum.inr l)
⊢ ⁅e i, f j⁆ = 0
have a₂ : ∀ (k : ι) (l : ↥b.support), ⁅e i, f j⁆ (Sum.inr k) (Sum.inl l) = 0 (Sum.inr k) (Sum.inl l)
Tactic: ext (k | k) (l | l)
-- 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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
a : ∀ (k l : ↥b.support), ⁅e i, f j⁆ (Sum.inl k) (Sum.inl l) = 0 (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0 (Sum.inl k) (Sum.inr l)
a₂ : ∀ (k : ι) (l : ↥b.support), ⁅e i, f j⁆ (Sum.inr k) (Sum.inl l) = 0 (Sum.inr k) (Sum.inl l)
⊢ ⁅e i, f j⁆ = 0
have a₃ : ∀ (k l : ι), ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)
Tactic: ext (k | k) (l | l)
-- 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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k l : ↥b.support
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inl l) = 0 (Sum.inl k) (Sum.inl l)
have a : ∀ (hij : j ≠ i) [P.IsReduced] [P.IsIrreducible] (hij' : (↑i : ι) ≠ (↑j : ι)) (k l : ↥b.support),
  ⁅e i, f j⁆ (Sum.inl k) (Sum.inl l) = 0 (Sum.inl k) (Sum.inl l)
Tactic: rw [ne_comm] at hij
Cleared hypotheses: hij, inst_10, inst_11, hij', this, k, l
-- 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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ι
l : ↥b.support
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inl l) = 0 (Sum.inr k) (Sum.inl l)
have aux₁ : (P.root : (a : ι) → M) k ≠
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) (↑j : ι) : M)
Tactic: have aux₁ : P.root k ≠ P.root i - P.root j :=
      fun contra ↦ b.sub_notMem_range_root i.property j.property ⟨k, contra⟩
-- 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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k l : ι
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)
have a : ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (↑j : ι)) = 0 (Sum.inr k) (Sum.inr (↑j : ι))
Tactic: rcases eq_or_ne l j with rfl | h₃
Cleared hypotheses: l
-- 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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k l : ι
a : ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (↑j : ι)) = 0 (Sum.inr k) (Sum.inr (↑j : ι))
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)
have a₁ : ∀ (h₃ : l ≠ (↑j : ι)), ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)
Tactic: rcases eq_or_ne l j with rfl | h₃
-- 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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ι
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (↑j : ι)) = 0 (Sum.inr k) (Sum.inr (↑j : ι))
have a : ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inr k) = 0 (Sum.inr k) (Sum.inr (↑j : ι))
Tactic: rw [← ⁅e i, f j⁆.transpose_apply, lie_e_f_ne_aux₁ hij, Pi.zero_apply, Matrix.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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ι
a : ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inr k) = 0 (Sum.inr k) (Sum.inr (↑j : ι))
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (↑j : ι)) = 0 (Sum.inr k) (Sum.inr (↑j : ι))
have a₁ : Eq.{u_2 + 1} (α := R) (0 (Sum.inr k)) (0 (Sum.inr k) (Sum.inr (↑j : ι)))
Tactic: rw [← ⁅e i, f j⁆.transpose_apply, lie_e_f_ne_aux₁ hij, Pi.zero_apply, Matrix.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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ι
a : ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inr k) = 0 (Sum.inr k) (Sum.inr (↑j : ι))
a₁ : Eq.{u_2 + 1} (α := R) (0 (Sum.inr k)) (0 (Sum.inr k) (Sum.inr (↑j : ι)))
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (↑j : ι)) = 0 (Sum.inr k) (Sum.inr (↑j : ι))
have a₂ : Eq.{u_2 + 1} (α := R) 0 (0 (Sum.inr k) (Sum.inr (↑j : ι)))
Tactic: rw [← ⁅e i, f j⁆.transpose_apply, lie_e_f_ne_aux₁ hij, Pi.zero_apply, Matrix.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
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k : ι
a : ⁅e i, f j⁆ᵀ (Sum.inr (↑j : ι)) (Sum.inr k) = 0 (Sum.inr k) (Sum.inr (↑j : ι))
a₁ : Eq.{u_2 + 1} (α := R) (0 (Sum.inr k)) (0 (Sum.inr k) (Sum.inr (↑j : ι)))
a₂ : Eq.{u_2 + 1} (α := R) 0 (0 (Sum.inr k) (Sum.inr (↑j : ι)))
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (↑j : ι)) = 0 (Sum.inr k) (Sum.inr (↑j : ι))
have a₃ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [← ⁅e i, f j⁆.transpose_apply, lie_e_f_ne_aux₁ hij, Pi.zero_apply, Matrix.zero_apply]