awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
inst_10 : P.IsIrreducible
h :
  Ne.{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)
k : ι
this : Nonempty ι
obtain :
  ∀ (i' j' : ι)
    (h' :
      ∀ (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)),
    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)
⊢ 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:
obtain ⟨i', j', h'⟩ := B.exists_apply_eq_or

Premises used: RootPairing.InvariantForm.exists_apply_eq_or
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
inst_10 : P.IsIrreducible
h :
  Ne.{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)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  ∀ (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)
hi :
  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) i') : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i' : M) :
      R)
hj :
  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)
⊢ 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:
specialize h' k
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
inst_10 : P.IsIrreducible
h :
  Ne.{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)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  ∀ (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)
hi :
  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) i') : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i' : M) :
      R)
hj :
  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) j') : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j' : 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) 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:
specialize h' k
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
inst_10 : P.IsIrreducible
h :
  Ne.{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)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  ∀ (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)
hi :
  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)
hj :
  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)
⊢ 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:
specialize h' k
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
inst_10 : P.IsIrreducible
h :
  Ne.{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)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  ∀ (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)
hi :
  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)
hj :
  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) j') : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j' : 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) 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:
specialize h' k
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
inst_10 : P.IsIrreducible
h :
  Ne.{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)
k : ι
this : Nonempty ι
i' j' : ι
hi :
  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) i') : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i' : M) :
      R)
hj :
  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)
h' :
  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)
⊢ 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:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
inst_10 : P.IsIrreducible
h :
  Ne.{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)
k : ι
this : Nonempty ι
i' j' : ι
hi :
  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) i') : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i' : M) :
      R)
hj :
  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) j') : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j' : M) :
      R)
h' :
  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)
⊢ 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:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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
i j : ι
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
inst_10 : P.IsIrreducible
h :
  Ne.{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)
k : ι
this : Nonempty ι
i' j' : ι
hi :
  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)
hj :
  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)
h' :
  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)
⊢ 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:
aesop