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
⊢ ω b * ⁅h j, f i⁆ = ω b * (h j * f i - f i * h j)
have rw : ω b * (h j * f i - f i * h j) = ω b * (h j * f i - f i * h j)
Tactic: rw [Ring.lie_def]
-- 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
⊢ -(h j * e i - e i * h j) * ω b = -⁅h j, e i⁆ * ω b
have rw : -(h j * e i - e i * h j) * ω b = -(h j * e i - e i * h j) * ω b
Tactic: rw [Ring.lie_def]
-- 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
⊢ -⁅h j, e i⁆ * ω b = -(b.cartanMatrix i j • e i) * ω b
have rw : -(b.cartanMatrix i j • e i) * ω b = -(b.cartanMatrix i j • e i) * ω b
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 j : ↥b.support
⊢ ω b * (h j * f i - f i * h j) = -(h j * e i - e i * h j) * ω b
have calc_1 : -(h j * (e i * ω b)) - -(e i * (h j * ω b)) = e i * (h j * ω b) - h j * (e i * ω b)
Tactic: rw [mul_sub, ← mul_assoc, ← mul_assoc, ω_mul_h, ω_mul_f, mul_assoc, mul_assoc, ω_mul_f, ω_mul_h,
      neg_sub, neg_mul, neg_mul, mul_neg, sub_mul, mul_assoc, mul_assoc]
-- 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
⊢ -(b.cartanMatrix i j • e i) * ω b = ω b * -b.cartanMatrix i j • f i
have calc_2 : -(b.cartanMatrix i j • e i) * ω b = -b.cartanMatrix i j • (e i * ω b)
Tactic: rw [Matrix.mul_smul, ω_mul_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 j : ↥b.support
⊢ ⁅h j, f i⁆ = -b.cartanMatrix i j • f i
have suffices : ω b * ⁅h j, f i⁆ = ω b * -b.cartanMatrix i j • f i
Tactic: classical
  suffices ω b * ⁅h j, f i⁆ = ω b * (-b.cartanMatrix i j • f i) by
    replace this := congr_arg (ω b * ·) this
    simpa [← mul_assoc, ω_mul_ω] using this
  calc ω b * ⁅h j, f i⁆ = ω b * (h j * f i - f i * h j) := by rw [Ring.lie_def]
                      _ = -(h j * e i - e i * h j) * ω b := ?_
                      _ = -⁅h j, e i⁆ * ω b := by rw [Ring.lie_def]
                      _ = -(b.cartanMatrix i j • e i) * ω b := by rw [lie_h_e]
                      _ = ω b * (-b.cartanMatrix i j • f i) := ?_
  · rw [mul_sub, ← mul_assoc, ← mul_assoc, ω_mul_h, ω_mul_f, mul_assoc, mul_assoc, ω_mul_f, ω_mul_h,
      neg_sub, neg_mul, neg_mul, mul_neg, sub_mul, mul_assoc, mul_assoc]
    abel
  · rw [Matrix.mul_smul, ω_mul_f]
    simp [mul_assoc]
-- 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
suffices suffices₁ suffices₂ : ω b * ⁅h j, f i⁆ = ω b * -b.cartanMatrix i j • f i
⊢ ⁅h j, f i⁆ = -b.cartanMatrix i j • f i
have calc_1 : ω b * (h j * f i - f i * h j) = -(h j * e i - e i * h j) * ω b
Tactic: classical
  suffices ω b * ⁅h j, f i⁆ = ω b * (-b.cartanMatrix i j • f i) by
    replace this := congr_arg (ω b * ·) this
    simpa [← mul_assoc, ω_mul_ω] using this
  calc ω b * ⁅h j, f i⁆ = ω b * (h j * f i - f i * h j) := by rw [Ring.lie_def]
                      _ = -(h j * e i - e i * h j) * ω b := ?_
                      _ = -⁅h j, e i⁆ * ω b := by rw [Ring.lie_def]
                      _ = -(b.cartanMatrix i j • e i) * ω b := by rw [lie_h_e]
                      _ = ω b * (-b.cartanMatrix i j • f i) := ?_
  · rw [mul_sub, ← mul_assoc, ← mul_assoc, ω_mul_h, ω_mul_f, mul_assoc, mul_assoc, ω_mul_f, ω_mul_h,
      neg_sub, neg_mul, neg_mul, mul_neg, sub_mul, mul_assoc, mul_assoc]
    abel
  · rw [Matrix.mul_smul, ω_mul_f]
    simp [mul_assoc]
-- 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
suffices suffices₁ suffices₂ : ω b * ⁅h j, f i⁆ = ω b * -b.cartanMatrix i j • f i
calc_1 : ω b * (h j * f i - f i * h j) = -(h j * e i - e i * h j) * ω b
⊢ ⁅h j, f i⁆ = -b.cartanMatrix i j • f i
have calc_2 : -(b.cartanMatrix i j • e i) * ω b = ω b * -b.cartanMatrix i j • f i
Tactic: classical
  suffices ω b * ⁅h j, f i⁆ = ω b * (-b.cartanMatrix i j • f i) by
    replace this := congr_arg (ω b * ·) this
    simpa [← mul_assoc, ω_mul_ω] using this
  calc ω b * ⁅h j, f i⁆ = ω b * (h j * f i - f i * h j) := by rw [Ring.lie_def]
                      _ = -(h j * e i - e i * h j) * ω b := ?_
                      _ = -⁅h j, e i⁆ * ω b := by rw [Ring.lie_def]
                      _ = -(b.cartanMatrix i j • e i) * ω b := by rw [lie_h_e]
                      _ = ω b * (-b.cartanMatrix i j • f i) := ?_
  · rw [mul_sub, ← mul_assoc, ← mul_assoc, ω_mul_h, ω_mul_f, mul_assoc, mul_assoc, ω_mul_f, ω_mul_h,
      neg_sub, neg_mul, neg_mul, mul_neg, sub_mul, mul_assoc, mul_assoc]
    abel
  · rw [Matrix.mul_smul, ω_mul_f]
    simp [mul_assoc]
-- 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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
⊢ 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)
have rw : k ≠ (↑i : ι) ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) (↑i : ι) : M)
Tactic: rw [LinearIndependent.pair_symm_iff, IsReduced.linearIndependent_iff]
-- 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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
⊢ k ≠ (↑i : ι) ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) (↑i : ι) : M)
have refine : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) (↑i : ι) : M)
Tactic: refine ⟨hki, ?_⟩
-- 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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
⊢ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) (↑i : ι) : M)
have rwa : ¬Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) (↑i : ι) : M)
Tactic: rwa [ne_eq, root_eq_neg_iff]
-- 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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
rwa : ¬Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) (↑i : ι) : M)
⊢ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) (↑i : ι) : M)
have rwa₁ : ¬k = (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
Tactic: rwa [ne_eq, root_eq_neg_iff]
-- 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 : ↥b.support
inst_10 : P.IsReduced
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k)
have 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)
Tactic: have h_lin_ind : LinearIndependent R ![P.root i, P.root k] := by
    rw [LinearIndependent.pair_symm_iff, IsReduced.linearIndependent_iff]
    refine ⟨hki, ?_⟩
    rwa [ne_eq, root_eq_neg_iff]
-- 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
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)
this :
  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)
x : ι
⊢ (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)
have rw : HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) =
    (P.root : (a : ι) → M) k ↔
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M)
Tactic: rw [eq_sub_iff_add_eq', eq_comm]
-- 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
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)
this :
  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)
x : ι
rw :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) =
      (P.root : (a : ι) → M) k ↔
    (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) 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)
have rw₁ : (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 =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M)
Tactic: rw [eq_sub_iff_add_eq', eq_comm]
-- 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 : ↥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)
this :
  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)
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k)
have aux : ∀ (x : ι),
  (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: have aux (x : ι) : P.root x = P.root k - P.root i ↔ P.root k = P.root i + P.root x := by
      rw [eq_sub_iff_add_eq', eq_comm]
-- 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
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)
this :
  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)
aux :
  ∀ (x : ι),
    (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)
x : ι
⊢ (P.root : (a : ι) → M) x =
      HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M) ↔
    (P.root : (a : ι) → M) k =
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
have rw : (P.root : (a : ι) → M) x =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M) ↔
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M) =
    (P.root : (a : ι) → M) x
Tactic: rw [eq_sub_iff_add_eq', eq_comm]