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
refine_1 :
  ∀
    (h :
      ∀ (i j : ι)
        (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)),
        Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
          Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M))
    (i j : ι) (hij : i ≠ j)
    (hLin :
      ¬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)),
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
refine_2 :
  ∀
    (h :
      ∀ (i j : ι),
        i ≠ j →
          ¬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) →
            Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M))
    (i j : ι)
    (hLin :
      ¬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)),
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ (∀ (i j : ι)
      (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)),
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
        Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)) ↔
    ∀ (i j : ι),
      i ≠ j →
        ¬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) →
          Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
refine ⟨fun h i j hij hLin ↦ ?_, fun h i j hLin  ↦ ?_⟩
-- 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
h :
  ∀ (i j : ι)
    (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)),
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
i j : ι
hij : i ≠ j
hLin :
  ¬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)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
specialize h i j hLin
-- 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 : ι
hij : i ≠ j
hLin :
  ¬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)
h :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
simp_all
-- 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
h :
  ∀ (i j : ι),
    i ≠ j →
      ¬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) →
        Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
i j : ι
hLin :
  ¬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)
refine_2 :
  ∀
    (hLin :
      ¬LinearIndependent.{0, u_2, u_3} R (M := M)
          (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)),
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) i : M) ∨
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) i : M)
refine_2₁ :
  ∀ (h' : i ≠ j),
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
rcases eq_or_ne i j with rfl | h'

Premises used: eq_or_ne, 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
h :
  ∀ (i j : ι),
    i ≠ j →
      ¬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) →
        Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
i : ι
hLin :
  ¬LinearIndependent.{0, u_2, u_3} R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
refine_2 refine_2₁ :
  ¬Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) i : M) →
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) i : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) i : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
tauto
-- 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
h :
  ∀ (i j : ι),
    i ≠ j →
      ¬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) →
        Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
i j : ι
hLin :
  ¬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)
h' : i ≠ j
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
Or.inr (h i j h' hLin)

Premises used: Or.inr
-- 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
h :
  ∀ (i j : ι),
    i ≠ j →
      ¬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) →
        Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
i j : ι
hLin :
  ¬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)
h' : i ≠ j
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
exact Or.inr (h i j h' hLin)

Premises used: Or.inr
-- 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 : P.IsReduced
h : i ≠ j
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : 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)),
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
have := IsReduced.eq_or_eq_neg (P := P) i j
-- 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 : P.IsReduced
h : i ≠ j
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
this :
  ∀
    (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)),
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∨
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ 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:
simp_all
-- 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 : Nontrivial R
inst_6 : P.IsReduced
⊢ 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) ↔
    i ≠ j ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
⟨fun h ↦ ?_, fun ⟨h, h'⟩ ↦ linearIndependent P h h'⟩

Premises used: _private.0.RootPairing.IsReduced.linearIndependent_iff.match_1, RootPairing.IsReduced.linearIndependent, RootPairing.root, LinearIndependent, Iff.intro, Matrix.vecEmpty, DFunLike.coe, Matrix.vecCons
-- 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 : Nontrivial R
inst_6 : P.IsReduced
refine :
  ∀
    (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)),
    i ≠ j ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ 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) ↔
    i ≠ j ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h, h'⟩ ↦ linearIndependent P 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 : Nontrivial R
inst_6 : P.IsReduced
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 : Nontrivial R
inst_6 : P.IsReduced
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
contrapose! :
  ∀ (h : ∀ (_ : i ≠ j), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)),
    ∃ (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
⊢ i ≠ j ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
contrapose! 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 : Nontrivial R
inst_6 : P.IsReduced
h : ∀ (_ : i ≠ j), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
inl :
  ∀ (h : ∀ (_ : i ≠ i), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) i : M)),
    ∃ (s : R) (t : R),
      HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M) =
          0 ∧
        ∀ (_ : s = 0), t ≠ 0
inr :
  ∀ (h' : i ≠ j),
    ∃ (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
⊢ ∃ (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:
rcases eq_or_ne i j with rfl | h'

Premises used: eq_or_ne, 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 : ι
inst_5 : Nontrivial R
inst_6 : P.IsReduced
h : ∀ (_ : i ≠ i), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 1 ((P.root : (a : ι) → M) i : M) +
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (-1) ((P.root : (a : ι) → M) i : M) =
      0 ∧
    ∀ (_ : Eq.{u_2 + 1} (α := R) 1 0), Ne.{u_2 + 1} (α := R) (-1) 0

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 : ι
inst_5 : Nontrivial R
inst_6 : P.IsReduced
h : ∀ (_ : i ≠ i), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) i : M)
⊢ ∃ (s : R) (t : R),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M) = 0 ∧
      ∀ (_ : s = 0), t ≠ 0

Tactic:
exact ⟨1, -1, by 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 : Nontrivial R
inst_6 : P.IsReduced
h : ∀ (_ : i ≠ j), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
h' : i ≠ j
inr :
  ∃ (s : R) (t : R),
    HSMul.hSMul (β := M) s (-(P.root : (a : ι) → M) j : 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:
rw [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 : Nontrivial R
inst_6 : P.IsReduced
h : ∀ (_ : i ≠ j), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
h' : i ≠ j
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 1 (-(P.root : (a : ι) → M) j : M) +
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 1 ((P.root : (a : ι) → M) j : M) =
      0 ∧
    ∀ (_ : Eq.{u_2 + 1} (α := R) 1 0), Ne.{u_2 + 1} (α := R) 1 0

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 : Nontrivial R
inst_6 : P.IsReduced
h : ∀ (_ : i ≠ j), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
h' : i ≠ j
⊢ ∃ (s : R) (t : R),
    HSMul.hSMul (β := M) s (-(P.root : (a : ι) → M) j : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 ∧
      ∀ (_ : s = 0), t ≠ 0

Tactic:
exact ⟨1, 1, by 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
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i : ι
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) 1 (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M)) +
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (-(↑n : R)) ((P.root : (a : ι) → M) i : M) =
    0

Tactic:
simp [Nat.cast_smul_eq_nsmul]

Premises used: Nat.cast_smul_eq_nsmul
-- 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
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i : ι
⊢ ¬(Eq.{u_2 + 1} (α := R) 1 0 ∧ Eq.{u_2 + 1} (α := R) (-(↑n : R)) 0)

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
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i : ι
⊢ ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R
      ![HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M), (P.root : (a : ι) → M) i]

Tactic:
simpa only [LinearIndependent.pair_iff, not_forall] using
      ⟨1, -(n : R), by simp [Nat.cast_smul_eq_nsmul], by simp⟩

Premises used: LinearIndependent.pair_iff, Classical.not_forall
-- 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
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i : ι
⊢ ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R
      ![HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M), (P.root : (a : ι) → M) i]

Tactic:
have : ¬ LinearIndependent R ![n • P.root i, P.root i] := by
    simpa only [LinearIndependent.pair_iff, not_forall] using
      ⟨1, -(n : R), by simp [Nat.cast_smul_eq_nsmul], by 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
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i : ι
this :
  ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R
      ![HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M), (P.root : (a : ι) → M) i]
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M)
⊢ j = i ∨ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
simpa only [← hj, IsReduced.linearIndependent_iff, not_and_or, not_not] using this

Premises used: Classical.not_not, RootPairing.IsReduced.linearIndependent_iff, not_and_or
-- 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
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i : ι
this :
  ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R
      ![HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M), (P.root : (a : ι) → M) i]
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M)
⊢ j = i ∨ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
replace this : j = i ∨ P.root j = -P.root i := by
    simpa only [← hj, IsReduced.linearIndependent_iff, not_and_or, not_not] using 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
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M)
this : j = i ∨ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)
inl : ∀ (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M)), False
inr : ∀ (this : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)), False
⊢ False

Tactic:
rcases this with rfl | this

Premises used: 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
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul (α := ℤ) (β := M) 1 ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul (α := ℤ) (β := M) (↑n : ℤ) ((P.root : (a : ι) → M) j : M)

Tactic:
simpa
-- 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
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul (α := ℤ) (β := M) 1 ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul (α := ℤ) (β := M) (↑n : ℤ) ((P.root : (a : ι) → M) j : M)

Tactic:
replace hj : (1 : ℤ) • P.root j = (n : ℤ) • P.root j := by simpa