-- 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
inst_10 : P.IsIrreducible
this_1 : Fintype ι
B : P.InvariantForm
i j : ι
li : 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)
lj : 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)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
this :
  Eq.{u_2 + 1} («α» := 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)
      ((((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) =
        HMul.hMul («α» := R) (β := R) (2 : 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) =
          HMul.hMul («α» := R) (β := R) (3 : 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) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) =
            HMul.hMul («α» := R) (β := R) (2 : 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) ∨
          (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) =
            HMul.hMul («α» := R) (β := R) (3 : 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)
inl :
  ∀
    (this :
      Eq.{u_2 + 1} («α» := 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)
        ((((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)),
    (li = 2 * lj ∨ lj = 2 * li) ∨ li = 3 * lj ∨ lj = 3 * li
⊢ (li = 2 * lj ∨ lj = 2 * li) ∨ li = 3 * lj ∨ lj = 3 * li
have inr : ∀
  (this :
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) =
      HMul.hMul («α» := R) (β := R) (2 : 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)),
  (li = 2 * lj ∨ lj = 2 * li) ∨ li = 3 * lj ∨ lj = 3 * li
Tactic: tauto
Cleared hypotheses: this