awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
rw :
  ¬Eq.{u_5 + 1} («α» := K)
      ((((P.toLinearMap : (a : M) → N →ₗ[K] K)
                (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)) :
              N →ₗ[K] K) :
            (a : N) → K)
          ((P.coroot : (a : ι) → N) i : N) :
        K)
      (0 : K)
⊢ P.pairing i k ≠ 0

Tactic:
rw [ne_eq, P.pairing_eq_zero_iff, ← root_coroot_eq_pairing, hk]

Premises used: RootPairing.root_coroot_eq_pairing, RootPairing.pairing_eq_zero_iff, ne_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
⊢ ¬Eq.{u_5 + 1} («α» := K)
      ((((P.toLinearMap : (a : M) → N →ₗ[K] K)
                (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)) :
              N →ₗ[K] K) :
            (a : N) → K)
          ((P.coroot : (a : ι) → N) i : N) :
        K)
      (0 : K)

Tactic:
simpa [P.pairing_eq_zero_iff.mp hij₀] using two_ne_zero

Premises used: RootPairing.pairing_eq_zero_iff, two_ne_zero, Iff.mp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
⊢ P.pairing i k ≠ 0

Tactic:
have hik : P.pairing i k ≠ 0 := by
      rw [ne_eq, P.pairing_eq_zero_iff, ← root_coroot_eq_pairing, hk]
      simpa [P.pairing_eq_zero_iff.mp hij₀] using two_ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
hik : P.pairing i k ≠ 0
inl : Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)

Tactic:
suffices P.root k ∈ q from (q.add_mem_iff_right hi).mp <| hk ▸ this
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
hik : P.pairing i k ≠ 0
⊢ HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairing i k) ((P.root : (a : ι) → M) k : M)) ∈
    q

Tactic:
simpa [reflection_apply_root] using hq k hi

Premises used: RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
hik : P.pairing i k ≠ 0
⊢ HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairing i k) ((P.root : (a : ι) → M) k : M)) ∈
    q

Tactic:
replace hq : P.root i - P.pairing i k • P.root k ∈ q := by
      simpa [reflection_apply_root] using hq k hi
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
hik : P.pairing i k ≠ 0
hq :
  HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairing i k) ((P.root : (a : ι) → M) k : M)) ∈
    q
inl :
  ∀ (hq : HSMul.hSMul (β := M) (P.pairing i k) ((P.root : (a : ι) → M) k : M) ∈ q),
    Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)
inl₁ inl₂ inl₃ inl₄ :
  ∀ (hq : Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)),
    Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)

Tactic:
rwa [q.sub_mem_iff_right hi, q.smul_mem_iff hik] at hq

Premises used: Submodule.smul_mem_iff, Submodule.sub_mem_iff_right
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j ≠ 0
⊢ HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) ∈
    q

Tactic:
simpa [reflection_apply_root] using hq j hi

Premises used: RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j ≠ 0
⊢ HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) ∈
    q

Tactic:
replace hq : P.root i - P.pairing i j • P.root j ∈ q := by
      simpa [reflection_apply_root] using hq j hi
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j ≠ 0
hq :
  HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) ∈
    q
inr :
  ∀ (hq : HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) ∈ q),
    Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
inr₁ inr₂ inr₃ inr₄ :
  ∀ (hq : Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)),
    Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)

Tactic:
rwa [q.sub_mem_iff_right hi, q.smul_mem_iff hij₀] at hq

Premises used: Submodule.smul_mem_iff, Submodule.sub_mem_iff_right
-- 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
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
i j : ι
h : P.pairingIn ℤ i j ≠ 0
⊢ Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)

Tactic:
have h₁ := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i j
-- 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
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
i j : ι
h : P.pairingIn ℤ i j ≠ 0
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
⊢ HMul.hMul («α» := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ j i) : 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) =
    HMul.hMul («α» := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i j) : 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:
simpa only [algebraMap_pairingIn] using B.pairing_mul_eq_pairing_mul_swap i j

Premises used: RootPairing.InvariantForm.pairing_mul_eq_pairing_mul_swap, RootPairing.algebraMap_pairingIn
-- 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
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
i j : ι
h : P.pairingIn ℤ i j ≠ 0
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
⊢ HMul.hMul («α» := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ j i) : 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) =
    HMul.hMul («α» := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i j) : 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:
have h₂ : algebraMap ℤ R (P.pairingIn ℤ j i) * B.form (α i) (α i) =
            algebraMap ℤ R (P.pairingIn ℤ i j) * B.form (α j) (α j) := by
    simpa only [algebraMap_pairingIn] using B.pairing_mul_eq_pairing_mul_swap i j
-- 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
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
i j : ι
h : P.pairingIn ℤ i j ≠ 0
h₁ :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
h₂ :
  HMul.hMul («α» := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ j i) : 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) =
    HMul.hMul («α» := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i j) : 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) 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)

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
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
inst_10 : P.IsIrreducible
i j j' : ι
h₁ :
  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₂ :
  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) j' : M) :
      R)
    (0 : R)
this : P.pairingIn ℤ i j' ≠ 0
⊢ 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)

Tactic:
simp only [← h₁, B.apply_eq_or_aux i j' this]

Premises used: RootPairing.InvariantForm.apply_eq_or_aux
-- 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
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
inst_10 : P.IsIrreducible
i j j' : ι
h₁ :
  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₂ :
  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) j' : M) :
      R)
    (0 : R)
suffices : P.pairingIn ℤ i j' ≠ 0
⊢ 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)

Tactic:
suffices P.pairingIn ℤ i j' ≠ 0 by simp only [← h₁, B.apply_eq_or_aux i j' this]