awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
x : ι
hx :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M)
h₂ : chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0
h_lin_ind_x :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) x] : Fin (Nat.succ 0).succ → M)
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k =
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x + 1

Tactic:
have hx' : P.chainBotCoeff i k = P.chainBotCoeff i x + 1 :=
      chainBotCoeff_of_add h_lin_ind_x (add_comm (P.root i) _ ▸ hx)
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
x : ι
hx :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M)
h₂ : chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0
h_lin_ind_x :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) x] : Fin (Nat.succ 0).succ → M)
hx' :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k =
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x + 1
⊢ (∑ x : ι,
      if
          (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) (↑i : ι) k) : R)
            1
      else 0) =
    HSub.hSub (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)

Tactic:
simp [hx, hx', h₂]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
h₁ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) a : M)
y : ι
hy :
  (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) y : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
inr :
  (-∑ x : ι,
        if
            (P.root : (a : ι) → M) k =
              HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
              1 *
            HAdd.hAdd (α := R)
              (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R) 1
        else 0) =
    HSub.hSub (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)
⊢ HSub.hSub (α := R)
      (∑ x : ι,
        if
            (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) (↑i : ι) k) : R) 1
        else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) k =
              HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
              1 *
            HAdd.hAdd (α := R)
              (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R) 1
        else 0) =
    HSub.hSub (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)

Tactic:
simp_rw [if_neg (h₁ _), Finset.sum_const_zero, zero_sub]

Premises used: Finset.sum_const_zero, if_neg, zero_sub
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
h₁ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) a : M)
y : ι
hy :
  (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) y : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
x : ι
hx :
  (P.root : (a : ι) → M) x =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M)

Tactic:
simp [hx]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
h₁ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) a : M)
y : ι
hy :
  (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) y : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0

Tactic:
replace h₁ : P.chainBotCoeff i k = 0 :=
      P.chainBotCoeff_eq_zero_iff.mpr <| Or.inr fun ⟨x, hx⟩ ↦ h₁ x <| by simp [hx]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
y : ι
hy :
  (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) y : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
h₁ : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0
rw :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι),
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)] :
      Fin (Nat.succ 0).succ → M)
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) y] : Fin (Nat.succ 0).succ → M)

Tactic:
rw [← add_eq_of_eq_sub hy, add_comm]

Premises used: add_comm, add_eq_of_eq_sub
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
y : ι
hy :
  (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) y : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
h₁ : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι),
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)] :
      Fin (Nat.succ 0).succ → M)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
y : ι
hy :
  (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) y : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
h₁ : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) y] : Fin (Nat.succ 0).succ → M)

Tactic:
have h_lin_ind_y : LinearIndependent R ![P.root i, P.root y] := by
      rw [← add_eq_of_eq_sub hy, add_comm]; simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
y : ι
hy :
  (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) y : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
h₁ : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0
h_lin_ind_y :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) y] : Fin (Nat.succ 0).succ → M)
⊢ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k =
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) y + 1

Tactic:
have hy' : P.chainTopCoeff i k = P.chainTopCoeff i y + 1 := chainTopCoeff_of_sub h_lin_ind_y hy
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
y : ι
hy :
  (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) y : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
h₁ : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0
h_lin_ind_y :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) y] : Fin (Nat.succ 0).succ → M)
hy' :
  chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k =
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) y + 1
⊢ (-∑ x : ι,
        if
            (P.root : (a : ι) → M) k =
              HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
              1 *
            HAdd.hAdd (α := R)
              (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R) 1
        else 0) =
    HSub.hSub (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)

Tactic:
simp [hy, hy', h₁]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
h₁ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) a : M)
h₂ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) a : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
this :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0 ∧
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0
⊢ HSub.hSub (α := R)
      (∑ x : ι,
        if
            (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) (↑i : ι) k) : R) 1
        else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) k =
              HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
              1 *
            HAdd.hAdd (α := R)
              (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R) 1
        else 0) =
    HSub.hSub (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)

Tactic:
simp [h₁, h₂, this]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
h₁ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) a : M)
h₂ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) a : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
inr :
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0 ∧
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k = 0
⊢ HSub.hSub (α := R)
      (∑ x : ι,
        if
            (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) (↑i : ι) k) : R) 1
        else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) k =
              HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
              1 *
            HAdd.hAdd (α := R)
              (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R) 1
        else 0) =
    HSub.hSub (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)

Tactic:
suffices P.chainBotCoeff i k = 0 ∧ P.chainTopCoeff i k = 0 by simp [h₁, h₂, this]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
h₁ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) a : M)
h₂ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) a : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
x : ι
hx :
  (P.root : (a : ι) → M) x =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M)

Tactic:
simp [hx]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
h_lin_ind :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
h₁ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) a : M)
h₂ :
  ∀ (a : ι),
    ¬(P.root : (a : ι) → M) k =
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) a : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
x : ι
hx :
  (P.root : (a : ι) → M) x =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M)

Tactic:
simp [hx]