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 j : ↥b.support
hij : i ≠ j
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ (↑j : ι)
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)
have a : ∀ (h₃ : -(↑i : ι) ≠ (↑j : ι)), ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-(↑i : ι))) = 0 (Sum.inr k) (Sum.inr (-(↑i : ι)))
Tactic: rcases eq_or_ne l (-i) with rfl | h₄
Cleared hypotheses: l, 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 l : ι
h₃ : l ≠ (↑j : ι)
a : ∀ (h₃ : -(↑i : ι) ≠ (↑j : ι)), ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-(↑i : ι))) = 0 (Sum.inr k) (Sum.inr (-(↑i : ι)))
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)
have a₁ : ∀ (h₄ : l ≠ -(↑i : ι)), ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)
Tactic: rcases eq_or_ne l (-i) 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 : ι
h₃ : -(↑i : ι) ≠ (↑j : ι)
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-(↑i : ι))) = 0 (Sum.inr k) (Sum.inr (-(↑i : ι)))
have a : ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (Sum.inr k) = 0 (Sum.inr k) (Sum.inr (-(↑i : ι)))
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 : ι
h₃ : -(↑i : ι) ≠ (↑j : ι)
a : ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (Sum.inr k) = 0 (Sum.inr k) (Sum.inr (-(↑i : ι)))
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-(↑i : ι))) = 0 (Sum.inr k) (Sum.inr (-(↑i : ι)))
have a₁ : Eq.{u_2 + 1} (α := R) (0 (Sum.inr k)) (0 (Sum.inr k) (Sum.inr (-(↑i : ι))))
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 : ι
h₃ : -(↑i : ι) ≠ (↑j : ι)
a : ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (Sum.inr k) = 0 (Sum.inr k) (Sum.inr (-(↑i : ι)))
a₁ : Eq.{u_2 + 1} (α := R) (0 (Sum.inr k)) (0 (Sum.inr k) (Sum.inr (-(↑i : ι))))
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-(↑i : ι))) = 0 (Sum.inr k) (Sum.inr (-(↑i : ι)))
have a₂ : Eq.{u_2 + 1} (α := R) 0 (0 (Sum.inr k) (Sum.inr (-(↑i : ι))))
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 : ι
h₃ : -(↑i : ι) ≠ (↑j : ι)
a : ⁅e i, f j⁆ᵀ (Sum.inr (-(↑i : ι))) (Sum.inr k) = 0 (Sum.inr k) (Sum.inr (-(↑i : ι)))
a₁ : Eq.{u_2 + 1} (α := R) (0 (Sum.inr k)) (0 (Sum.inr k) (Sum.inr (-(↑i : ι))))
a₂ : Eq.{u_2 + 1} (α := R) 0 (0 (Sum.inr k) (Sum.inr (-(↑i : ι))))
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-(↑i : ι))) = 0 (Sum.inr k) (Sum.inr (-(↑i : ι)))
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]
-- 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_1 : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ (↑j : ι)
h₄ : l ≠ -(↑i : ι)
this :
  Eq.{u_2 + 1} (α := R)
    (∑ x : ι,
      if
          (P.root : (a : ι) → M) x =
              HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
            (P.root : (a : ι) → M) k =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
            1 *
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) l) : R)
            1
      else 0)
    (∑ x : ι,
      if
          (P.root : (a : ι) → M) x =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : 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 *
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R)
            1
      else 0)
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)
have h₁ : ∀ (x : ↥b.support), Membership.mem (γ := Finset ↥b.support) Finset.univ x → ¬((x = i ∧ l = -(↑i : ι)) ∧ k = -(↑j : ι))
Tactic: have h₁ : ∀ x ∈ Finset.univ, ¬ ((x = i ∧ l = -i) ∧ k = -j) := by
        rintro - - ⟨⟨-, contra⟩, -⟩; contradiction
-- 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_1 : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ (↑j : ι)
h₄ : l ≠ -(↑i : ι)
this :
  Eq.{u_2 + 1} (α := R)
    (∑ x : ι,
      if
          (P.root : (a : ι) → M) x =
              HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
            (P.root : (a : ι) → M) k =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
            1 *
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) l) : R)
            1
      else 0)
    (∑ x : ι,
      if
          (P.root : (a : ι) → M) x =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : 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 *
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R)
            1
      else 0)
h₁ :
  ∀ (x : ↥b.support), Membership.mem (γ := Finset ↥b.support) Finset.univ x → ¬((x = i ∧ l = -(↑i : ι)) ∧ k = -(↑j : ι))
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)
have h₂ : ∀ (x : ↥b.support), Membership.mem (γ := Finset ↥b.support) Finset.univ x → ¬((x = j ∧ l = (↑j : ι)) ∧ k = (↑i : ι))
Tactic: have h₂ : ∀ x ∈ Finset.univ, ¬ ((x = j ∧ l = j) ∧ k = i) := by
        rintro - - ⟨⟨-, contra⟩, -⟩; contradiction
-- 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 : ι
h₃ : l ≠ (↑j : ι)
h₄ : l ≠ -(↑i : ι)
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)
have a : Eq.{u_2 + 1} (α := R)
  (∑ x : ι,
    if
        (P.root : (a : ι) → M) x =
            HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
          (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
      HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R) 1 *
        HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) l) : R) 1
    else 0)
  (∑ x : ι,
    if
        (P.root : (a : ι) → M) x =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : 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 *
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) 1
    else 0)
Tactic: suffices
      (∑ x, if P.root x = P.root l - P.root j ∧ P.root k = P.root i + P.root x then
          ((P.chainBotCoeff i x : R) + 1) * (P.chainTopCoeff j l + 1) else 0) =
      (∑ x, if P.root x = P.root i + P.root l ∧ P.root k = P.root x - P.root j then
          ((P.chainTopCoeff j x : R) + 1) * (P.chainBotCoeff i l + 1) else 0) by
      have h₁ : ∀ x ∈ Finset.univ, ¬ ((x = i ∧ l = -i) ∧ k = -j) := by
        rintro - - ⟨⟨-, contra⟩, -⟩; contradiction
      have h₂ : ∀ x ∈ Finset.univ, ¬ ((x = j ∧ l = j) ∧ k = i) := by
        rintro - - ⟨⟨-, contra⟩, -⟩; contradiction
      rw [← sub_eq_zero] at this
      simpa [e, f, ← ite_and, Finset.sum_ite_of_false h₁, Finset.sum_ite_of_false h₂, -indexNeg_neg,
        -Finset.univ_eq_attach]
-- 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 : ι
h₃ : l ≠ (↑j : ι)
h₄ : l ≠ -(↑i : ι)
h₅ :
  HSub.hSub (β := M) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
x : ι
hx :
  (P.root : (a : ι) → M) x =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M)
hx' :
  (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M)
⊢ (P.root : (a : ι) → M) k =
    HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M)
have rw : HSub.hSub (β := M) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M))
    ((P.root : (a : ι) → M) (↑j : ι) : M) =
  HSub.hSub (β := M) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
    ((P.root : (a : ι) → M) (↑j : ι) : M)
Tactic: rw [hx', hx]
-- 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 : ι
h₃ : l ≠ (↑j : ι)
h₄ : l ≠ -(↑i : ι)
h₅ :
  HSub.hSub (β := M) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x : ι,
      if
          (P.root : (a : ι) → M) x =
              HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
            (P.root : (a : ι) → M) k =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
            1 *
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) l) : R)
            1
      else 0)
    (∑ x : ι,
      if
          (P.root : (a : ι) → M) x =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : 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 *
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R)
            1
      else 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) ∧
        (P.root : (a : ι) → M) k =
          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 l ∧ P.root k = P.root x - P.root j) := by
        rintro x - ⟨hx, hx'⟩; exact h₅ ⟨k, by rw [hx', hx]; abel⟩
-- 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 : ι
h₃ : l ≠ (↑j : ι)
h₄ : l ≠ -(↑i : ι)
h₅ :
  HSub.hSub (β := M) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
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) ∧
          (P.root : (a : ι) → M) k =
            HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M))
x : ι
hx :
  (P.root : (a : ι) → M) x =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M)
hx' :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M)
⊢ (P.root : (a : ι) → M) k =
    HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M)
have rw : HAdd.hAdd (α := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M)) =
  HSub.hSub (β := M) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
    ((P.root : (a : ι) → M) (↑j : ι) : M)
Tactic: rw [hx', hx]
-- 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 : ι
h₃ : l ≠ (↑j : ι)
h₄ : l ≠ -(↑i : ι)
h₅ :
  HSub.hSub (β := M) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
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) ∧
          (P.root : (a : ι) → M) k =
            HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M))
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x : ι,
      if
          (P.root : (a : ι) → M) x =
              HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
            (P.root : (a : ι) → M) k =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
            1 *
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) l) : R)
            1
      else 0)
    (∑ x : ι,
      if
          (P.root : (a : ι) → M) x =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : 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 *
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R)
            1
      else 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) ∧
        (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))
Tactic: have aux₄ : ∀ x ∈ Finset.univ,
          ¬ (P.root x = P.root l - P.root j ∧ P.root k = P.root i + P.root x) := by
        rintro x - ⟨hx, hx'⟩; exact h₅ ⟨k, by rw [hx', hx]; abel⟩
-- 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 : ι
h₃ : l ≠ (↑j : ι)
h₄ : l ≠ -(↑i : ι)
h₅ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M))
h₆ :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
⊢ HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
have rwa : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) (↑i : ι) : M)
Tactic: rwa [b.root_sub_mem_iff_root_add_mem i j l hij' i.property j.property h₃ _ h₅]