-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
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
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : IsTorsionFree R N
rw : P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔ P.pairing i j = -1 ∧ P.pairing j i = -4
rw₁ :
  P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R) (-1 : R) ∧ P.pairing j i = -4
rw₂ :
  P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R) (-1 : R) ∧
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R) (-4 : R)
rw₃ :
  P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
        (-(algebraMap S R : (a : S) → R) 1 : R) ∧
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R) (-4 : R)
rw₄ :
  P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
        (-(algebraMap S R : (a : S) → R) 1 : R) ∧
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R)
        (-(algebraMap S R : (a : S) → R) 4 : R)
rw₅ :
  P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
        ((algebraMap S R : (a : S) → R) (-1) : R) ∧
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R)
        (-(algebraMap S R : (a : S) → R) 4 : R)
rw₆ :
  P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
        ((algebraMap S R : (a : S) → R) (-1) : R) ∧
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R)
        ((algebraMap S R : (a : S) → R) (-4) : R)
rw₇ :
  P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔
    P.pairingIn S i j = -1 ∧
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R)
        ((algebraMap S R : (a : S) → R) (-4) : R)
rw₈ rw₉ : P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔ P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4
⊢ P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔
    (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (-2) ((P.root : (a : ι) → M) i : M)

Tactic:
rw [← P.pairing_neg_one_neg_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
    ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), ← map_neg, ← map_neg,
    (algebraMap_injective S R).eq_iff, (algebraMap_injective S R).eq_iff]

Premises used: Algebra.algebraMap, Function.Injective.eq_iff, map_ofNat, RootPairing.pairing_neg_one_neg_four_iff, RootPairing.algebraMap_pairingIn, map_neg, map_one, FaithfulSMul.algebraMap_injective