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
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hl :
  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)
hc : P.coxeterWeight i j = 4
refine_2 :
  HMul.hMul (β := R) (P.pairing j i)
      ((((P.flip : (a : N) → M →ₗ[R] R) ((P.coroot : (a : ι) → N) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R) =
    4
refine_2₁ : P.pairing j i * P.pairing i j = 4
refine_2₂ : P.pairing j i * P.pairing i j = P.coxeterWeight i j
refine_2₃ : P.pairing i j * P.pairing j i = P.coxeterWeight i j
refine_2₄ refine_2₅ : P.pairing i j * P.pairing j i = P.pairing i j * P.pairing j i
⊢ HMul.hMul (α := R) (β := R)
      ((((P.flip : (a : N) → M →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
      ((((P.flip : (a : N) → M →ₗ[R] R) ((P.coroot : (a : ι) → N) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R) =
    4

Tactic:
rw [coroot_root_eq_pairing, coroot_root_eq_pairing, ← hc, mul_comm, coxeterWeight]

Premises used: RootPairing.coxeterWeight, RootPairing.coroot_root_eq_pairing, mul_comm
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hl :
  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)
hc : P.coxeterWeight i j = 4
⊢ ∀ (s t : R),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0

Tactic:
rw [LinearIndependent.pair_iff] at hl

Premises used: LinearIndependent.pair_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 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hl :
  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)
hc : P.coxeterWeight i j = 4
hl₁ :
  ∀ (s t : R),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
⊢ P.coxeterWeight i j = 4

Tactic:
rw [LinearIndependent.pair_iff] at hl

Premises used: LinearIndependent.pair_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 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hl :
  ∀ (s t : R),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
hc : P.coxeterWeight i j = 4
⊢ 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) =
      0 →
    P.pairing j i = 0 ∧ Eq.{u_2 + 1} (α := R) (-2) 0

Tactic:
specialize hl (P.pairing j i) (-2)

Premises used: RootPairing.pairing, OfNat.ofNat, Neg.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 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hc : P.coxeterWeight i j = 4
hl :
  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) =
      0 →
    P.pairing j i = 0 ∧ Eq.{u_2 + 1} (α := R) (-2) 0
⊢ ¬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) =
      0

Tactic:
simp only [neg_smul, neg_eq_zero, two_ne_zero (α := R), and_false, imp_false] at hl

Premises used: neg_smul, imp_false, neg_eq_zero, two_ne_zero, and_false
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hc : P.coxeterWeight i j = 4
hl :
  ¬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) =
      0
refine_3 :
  ¬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) =
      0
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.flip : (a : N) → M →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
      ((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 [ne_eq, coroot_root_eq_pairing, ← sub_eq_zero, sub_eq_add_neg]

Premises used: sub_eq_zero, sub_eq_add_neg, ne_eq, RootPairing.coroot_root_eq_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 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hc : P.coxeterWeight i j = 4
hl :
  ¬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) =
      0
⊢ ¬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) =
      0

Tactic:
hl
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hc : P.coxeterWeight i j = 4
hl :
  ¬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) =
      0
⊢ ¬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) =
      0

Tactic:
exact hl
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
h :
  ¬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)
⊢ ¬∀ (s t : R),
      HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) =
          0 →
        s = 0 ∧ t = 0

Tactic:
rw [LinearIndependent.pair_iff] at h

Premises used: LinearIndependent.pair_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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
h :
  ¬∀ (s t : R),
      HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) =
          0 →
        s = 0 ∧ t = 0
⊢ ∃ (s : R) (t : R),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 ∧
      ∀ (_ : s = 0), t ≠ 0

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
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
h :
  ∃ (s : R) (t : R),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 ∧
      ∀ (_ : s = 0), t ≠ 0
obtain :
  ∀ (s t : R)
    (h₁ :
      HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0)
    (h₂ : ∀ (_ : s = 0), t ≠ 0),
    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 (β := 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:
obtain ⟨s, t, h₁, h₂⟩ := 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0
h₂ : ∀ (_ : s = 0), t ≠ 0
inl :
  ∀
    (h₁ :
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 0 ((P.root : (a : ι) → M) i : M) +
          HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) =
        0)
    (h₂ : ∀ (_ : Eq.{u_2 + 1} (α := R) 0 0), t ≠ 0), Ne.{u_2 + 1} (α := R) 0 0
inr : ∀ (hs : s ≠ 0), s ≠ 0
⊢ s ≠ 0

Tactic:
rcases eq_or_ne s 0 with rfl | hs

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
t : R
h₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 0 ((P.root : (a : ι) → M) i : M) +
      HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) =
    0
h₂ : ∀ (_ : Eq.{u_2 + 1} (α := R) 0 0), t ≠ 0
⊢ HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0

Tactic:
simpa using 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
t : R
h₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 0 ((P.root : (a : ι) → M) i : M) +
      HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) =
    0
h₂ : ∀ (_ : Eq.{u_2 + 1} (α := R) 0 0), t ≠ 0
⊢ Ne.{u_2 + 1} (α := R) 0 0

Tactic:
exact False.elim <| h₂ rfl <| (smul_eq_zero_iff_left <| P.ne_zero j).mp <| by simpa using h₁

Premises used: RootPairing.ne_zero, False.elim, smul_eq_zero_iff_left, Iff.mp, rfl
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0
h₂ : ∀ (_ : s = 0), t ≠ 0
hs : s ≠ 0
⊢ s ≠ 0

Tactic:
assumption
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0
h₂ : ∀ (_ : s = 0), t ≠ 0
⊢ s ≠ 0

Tactic:
replace h₂ : s ≠ 0 := by
    rcases eq_or_ne s 0 with rfl | hs
    · exact False.elim <| h₂ rfl <| (smul_eq_zero_iff_left <| P.ne_zero j).mp <| by simpa using h₁
    · assumption
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0
h₂ : s ≠ 0
inl :
  ∀
    (h₁ :
      HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) +
          HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 0 ((P.root : (a : ι) → M) j : M) =
        0),
    Ne.{u_2 + 1} (α := R) 0 0
inr : ∀ (ht : t ≠ 0), t ≠ 0
⊢ t ≠ 0

Tactic:
rcases eq_or_ne t 0 with rfl | ht

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s : R
h₂ : s ≠ 0
h₁ :
  HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) +
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 0 ((P.root : (a : ι) → M) j : M) =
    0
⊢ HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) = 0

Tactic:
simpa using 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s : R
h₂ : s ≠ 0
h₁ :
  HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) +
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 0 ((P.root : (a : ι) → M) j : M) =
    0
⊢ Ne.{u_2 + 1} (α := R) 0 0

Tactic:
exact False.elim <| h₂ <| (smul_eq_zero_iff_left <| P.ne_zero i).mp <| by simpa using h₁

Premises used: RootPairing.ne_zero, False.elim, smul_eq_zero_iff_left, 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0
h₂ : s ≠ 0
ht : t ≠ 0
⊢ t ≠ 0

Tactic:
assumption
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0
h₂ : s ≠ 0
⊢ t ≠ 0

Tactic:
have h₃ : t ≠ 0 := by
    rcases eq_or_ne t 0 with rfl | ht
    · exact False.elim <| h₂ <| (smul_eq_zero_iff_left <| P.ne_zero i).mp <| by simpa using h₁
    · assumption
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0
h₂ : s ≠ 0
h₃ : t ≠ 0
rwa :
  ∀
    (h₁ :
      HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) = -HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M))
    (h₂ : s ≠ 0) (h₃ : t ≠ 0),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (h₁ :
      HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M))
    (h₂ : s ≠ 0) (h₃ : t ≠ 0),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M)

Tactic:
rwa [← eq_neg_iff_add_eq_zero, ← neg_smul] at h₁

Premises used: neg_smul, eq_neg_iff_add_eq_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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0
h₂ : s ≠ 0
h₃ : t ≠ 0
⊢ HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M)

Tactic:
replace h₁ : s • P.root i = -t • P.root j := by rwa [← eq_neg_iff_add_eq_zero, ← neg_smul] at 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M)
⊢ s * 2 = -(t * P.pairing j i)

Tactic:
simpa using congr_arg (P.coroot' i) h₁

Premises used: RootPairing.coroot', congr_arg, 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M)
⊢ s * 2 = -(t * P.pairing j i)

Tactic:
have h₄ : s * 2 = -(t * P.pairing j i) := by simpa using congr_arg (P.coroot' i) 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M)
h₄ : s * 2 = -(t * P.pairing j i)
rw rw₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M))
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M))

Tactic:
rw [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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₁ : HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M)
h₄ : s * 2 = -(t * P.pairing j i)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M))

Tactic:
replace h₁ : (2 : R) • (s • P.root i) = (2 : R) • (-t • P.root j) := by rw [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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₄ : s * 2 = -(t * P.pairing j i)
h₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (HSMul.hSMul (β := M) (-t) ((P.root : (a : ι) → M) j : M))
⊢ -t • HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    -t • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)

Tactic:
rw [smul_smul, mul_comm, h₄, smul_comm, ← neg_mul, ← smul_smul] at h₁

Premises used: smul_smul, mul_comm, neg_mul, SMulCommClass.smul_comm
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₄ : s * 2 = -(t * P.pairing j i)
h₁ :
  -t • HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    -t • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : 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:
smul_right_injective M (neg_ne_zero.mpr h₃) h₁

Premises used: Iff.mpr, smul_right_injective, neg_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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
s t : R
h₂ : s ≠ 0
h₃ : t ≠ 0
h₄ : s * 2 = -(t * P.pairing j i)
h₁ :
  -t • HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    -t • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : 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:
exact smul_right_injective M (neg_ne_zero.mpr h₃) h₁

Premises used: Iff.mpr, smul_right_injective, neg_ne_zero