awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (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
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)
⊢ 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)
have 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)
Tactic: rw [← P.pairing_one_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
    ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff,
    (algebraMap_injective S R).eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (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
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)
⊢ 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)
have 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)
Tactic: rw [← P.pairing_one_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
    ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff,
    (algebraMap_injective S R).eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (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
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 ↔
    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)
⊢ 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)
have 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
Tactic: rw [← P.pairing_one_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
    ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff,
    (algebraMap_injective S R).eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (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
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
⊢ 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)
have rw : P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔ P.pairing i j = -1 ∧ P.pairing j i = -4
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (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
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
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (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
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (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
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (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
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (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
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (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
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (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
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)
⊢ 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)
have 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)
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]