-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra_1 : P.IsG2
n : ι
h₃ :
  (P.root : (a : ι) → M) n =
    HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M)
x y : ℤ
h₀ :
  HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
contra : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : 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) j : M)
have rwa : ∀
  (h₂ :
    HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) =
      -(P.root : (a : ι) → M) i)
  (this : Module.IsReflexive R M) (this : IsAddTorsionFree M) (contra : P.IsG2) (n : ι)
  (h₃ :
    (P.root : (a : ι) → M) n =
      HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
        ((P.root : (a : ι) → M) j : M))
  (x y : ℤ)
  (h₀ :
    HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) j : M) =
      (P.root : (a : ι) → M) k)
  (hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
  (hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M))
  (hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M))
  (hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M))
  (hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M))
  (contra : Eq.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : 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) j : M)
Tactic: rwa [contra, sub_eq_iff_eq_add] at h₂
Cleared hypotheses: h₂, this_1, this, contra_1, n, h₃, x, y, h₀, s, A, hki, hki', hli, hli', hmi, contra