-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
inst_10 : P.IsIrreducible
inst_11 : Nonempty ι
i : ι
pos :
  ∀
    (h :
      ∀ (j : ι),
        Eq.{u_2 + 1} («α» := R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) i : M) :
            R)),
    ∃ (i : ι) (j : ι),
      ∀ (k : ι),
        Eq.{u_2 + 1} («α» := R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) k : M) :
              R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) i : M) :
              R) ∨
          Eq.{u_2 + 1} («α» := R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) k : M) :
              R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) j : M) :
              R)
⊢ ∃ (i : ι) (j : ι),
    ∀ (k : ι),
      Eq.{u_2 + 1} («α» := R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) k : M) :
            R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) i : M) :
            R) ∨
        Eq.{u_2 + 1} («α» := R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) k : M) :
            R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R)
have neg : ∀
  (h :
    ∃ (j : ι),
      Ne.{u_2 + 1} («α» := R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)),
  ∃ (i : ι) (j : ι),
    ∀ (k : ι),
      Eq.{u_2 + 1} («α» := R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) k : M) :
            R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) i : M) :
            R) ∨
        Eq.{u_2 + 1} («α» := R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) k : M) :
            R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R)
Tactic: by_cases! h : (∀ j, B.form (α j) (α j) = B.form (α i) (α i))