awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 j_1 : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i j : ι
h : ¬(i ≠ j ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M))
hij : i ≠ j
⊢ ∀ (_ : i ≠ j), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
push Not at h

Premises used: Not
-- 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_1 j_1 : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i j : ι
hij : i ≠ j
h : ∀ (_ : i ≠ j), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)

Tactic:
simp [P.root_eq_neg_iff.mp (h hij)]

Premises used: RootPairing.root_eq_neg_iff, Iff.mp
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
h : i = j
⊢ P.pairing i j = 2 ∧ P.pairing j i = 2

Tactic:
simp [h]
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
refine : P.pairing i j = 2 ∧ P.pairing j i = 2 → ∀ (h₁ : P.pairing i j = 2) (h₂ : P.pairing j i = 2), i = j
⊢ P.pairing i j = 2 ∧ P.pairing j i = 2 ↔ i = j

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun h ↦ by simp [h]⟩
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
h : P.pairing i j = 2 ∧ P.pairing j i = 2
h₁ : P.pairing i j = 2
h₂ : P.pairing j i = 2
rw : HMul.hMul (α := R) 2 2 = 4
⊢ ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]

Premises used: RootPairing.coxeterWeight, RootPairing.coxeterWeight_eq_four_iff_not_linearIndependent
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
h : P.pairing i j = 2 ∧ P.pairing j i = 2
h₁ : P.pairing i j = 2
h₂ : P.pairing j i = 2
⊢ HMul.hMul (α := R) 2 2 = 4

Tactic:
norm_num
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
h : P.pairing i j = 2 ∧ P.pairing j i = 2
h₁ : P.pairing i j = 2
h₂ : P.pairing j i = 2
⊢ ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
have : ¬ LinearIndependent R ![P.root i, P.root j] := by
    rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]; norm_num
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
h : P.pairing i j = 2 ∧ P.pairing j i = 2
h₁ : P.pairing i j = 2
h₂ : P.pairing j i = 2
this :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)

Tactic:
replace this := P.pairing_smul_root_eq_of_not_linearIndependent this
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
h : P.pairing i j = 2 ∧ P.pairing j i = 2
h₁ : P.pairing i j = 2
h₂ : P.pairing j i = 2
this :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ i = j

Tactic:
P.root.injective <| smul_right_injective M two_ne_zero (h₂ ▸ this)

Premises used: smul_right_injective, two_ne_zero, RootPairing.root, Function.Embedding.injective
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
h : P.pairing i j = 2 ∧ P.pairing j i = 2
h₁ : P.pairing i j = 2
h₂ : P.pairing j i = 2
this :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ i = j

Tactic:
exact P.root.injective <| smul_right_injective M two_ne_zero (h₂ ▸ this)

Premises used: smul_right_injective, two_ne_zero, RootPairing.root, Function.Embedding.injective
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
simp :
  -P.pairing i j = 2 ∧ -P.pairing j i = 2 ↔
    Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ P.pairing i j = -2 ∧ P.pairing j i = -2 ↔
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
simp only [← neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
⊢ -P.pairing i j = 2 ∧ -P.pairing j i = 2 ↔
    Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)

Tactic:
simpa [eq_comm (a := -P.root i), eq_comm (b := j)] using
    P.pairing_two_two_iff (P.reflectionPerm i i) j

Premises used: RootPairing.pairing_two_two_iff, eq_comm, RootPairing.reflectionPerm, DFunLike.coe
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
⊢ IsAddTorsionFree M

Tactic:
have : IsAddTorsionFree M := .of_isTorsionFree R M
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this : IsAddTorsionFree M
⊢ IsAddTorsionFree N

Tactic:
have : IsAddTorsionFree N := .of_isTorsionFree R N
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this : IsAddTorsionFree N
⊢ P.pairing i j = 1 ∧ P.pairing 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:
⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun h ↦ ?_⟩

Premises used: RootPairing.root, Iff.intro, _private.0.RootPairing.pairing_one_four_iff'.match_1, HSMul.hSMul, OfNat.ofNat, Eq, DFunLike.coe
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this : IsAddTorsionFree N
refine_1 :
  P.pairing i j = 1 ∧ P.pairing j i = 4 →
    ∀ (h₁ : P.pairing i j = 1) (h₂ : P.pairing 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)
refine_2 :
  ∀ (h : (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)),
    P.pairing i j = 1 ∧ P.pairing j i = 4
⊢ P.pairing i j = 1 ∧ P.pairing 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:
refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun h ↦ ?_⟩
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this : IsAddTorsionFree N
h : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
rw : HMul.hMul (α := R) 1 4 = 4
⊢ ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]

Premises used: RootPairing.coxeterWeight, RootPairing.coxeterWeight_eq_four_iff_not_linearIndependent
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this : IsAddTorsionFree N
h : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
⊢ HMul.hMul (α := R) 1 4 = 4

Tactic:
simp
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this : IsAddTorsionFree N
h : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
⊢ ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
have : ¬ LinearIndependent R ![P.root i, P.root j] := by
      rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]; simp
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this_2 : IsAddTorsionFree N
h : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)

Tactic:
replace this := P.pairing_smul_root_eq_of_not_linearIndependent this
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this_2 : IsAddTorsionFree N
h : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ 4 = HMul.hMul (α := R) 2 2

Tactic:
norm_num
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this_2 : IsAddTorsionFree N
h : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)

Tactic:
rw [h₂, show (4 : R) = 2 * 2 by norm_num, mul_smul] at this

Premises used: SemigroupAction.mul_smul
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this_2 : IsAddTorsionFree N
h : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)

Tactic:
smul_right_injective M two_ne_zero this.symm

Premises used: smul_right_injective, two_ne_zero, Eq.symm
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this_2 : IsAddTorsionFree N
h : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)

Tactic:
exact smul_right_injective M two_ne_zero this.symm

Premises used: smul_right_injective, two_ne_zero, Eq.symm
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this : IsAddTorsionFree N
h : (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
⊢ (P.coroot : (a : ι) → N) i = HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)

Tactic:
rw [← coroot_eq_smul_coroot_iff] at h

Premises used: RootPairing.coroot_eq_smul_coroot_iff
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this : IsAddTorsionFree N
h : (P.coroot : (a : ι) → N) i = HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)
refine_2 :
  Eq.{u_2 + 1} (α := R) ((P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R) (1 : R) ∧
    Eq.{u_2 + 1} (α := R)
      ((P.root' j : (a : N) → R) (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) : R)
      (4 : R)
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4

Tactic:
rw [pairing, pairing, h]

Premises used: RootPairing.pairing
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this : IsAddTorsionFree N
h : (P.coroot : (a : ι) → N) i = HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)
refine_2 : P.pairing i j = 1
⊢ Eq.{u_2 + 1} (α := R) ((P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R) (1 : R) ∧
    Eq.{u_2 + 1} (α := R)
      ((P.root' j : (a : N) → R) (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) : R)
      (4 : R)

Tactic:
norm_num
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this : IsAddTorsionFree N
h : (P.coroot : (a : ι) → N) i = HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)
refine_2 : HSMul.hSMul (α := R) 2 (P.pairing i j) = HSMul.hSMul (α := R) (β := R) 2 1
⊢ P.pairing i j = 1

Tactic:
suffices (2 : R) • P.pairing i j = (2 : R) • 1 from h2 this
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
this_1 : IsAddTorsionFree M
this : IsAddTorsionFree N
h : (P.coroot : (a : ι) → N) i = HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)
⊢ (P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) = HSMul.hSMul (α := R) (β := R) 2 1

Tactic:
simp
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
h2 : IsSMulRegular (R := R) R 2
⊢ P.pairing i j = -1 ∧ P.pairing 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:
simpa [neg_smul, ← neg_eq_iff_eq_neg] using P.pairing_one_four_iff' i (P.reflectionPerm j j) h2

Premises used: neg_smul, RootPairing.pairing_one_four_iff', neg_eq_iff_eq_neg, RootPairing.reflectionPerm, DFunLike.coe
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
⊢ P.pairing i j = 1 ∧ P.pairing 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:
P.pairing_one_four_iff' i j <| smul_right_injective R two_ne_zero

Premises used: RootPairing.pairing_one_four_iff', smul_right_injective, two_ne_zero
-- 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : IsTorsionFree R N
⊢ P.pairing i j = -1 ∧ P.pairing 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:
P.pairing_neg_one_neg_four_iff' i j <| smul_right_injective R two_ne_zero

Premises used: smul_right_injective, two_ne_zero, RootPairing.pairing_neg_one_neg_four_iff'