awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular.{u_1} (R := R) 2
x y : (↑{x : M | B.IsReflective x} : Type u_2)
z : M
⊢ HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R) (2 : R)
        ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
      ((IsReflective.coroot B ⋯ : (a : M) → R) z : R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑y : M) : R) (↑x : M)) :
        R)
have h : Eq.{u_1 + 1} (α := R)
  ((fun (x_1 : R) ↦
      HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) x_1)
    (HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R) (2 : R)
        ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
      ((IsReflective.coroot B sorry : (a : M) → R) z : R)))
  ((fun (x_1 : R) ↦
      HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) x_1)
    (HMul.hMul (α := R) (β := R) (2 : R)
      ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((IsReflective.coroot B sorry : (a : M) → R) (↑y : M) : R) (↑x : M)) :
        R)))
Tactic: refine x.2.1.1 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular.{u_1} (R := R) 2
x y : (↑{x : M | B.IsReflective x} : Type u_2)
z : M
⊢ Eq.{u_1 + 1} (α := R)
    ((fun (x_1 : R) ↦
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) x_1)
      (HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) (2 : R)
          ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)))
    ((fun (x_1 : R) ↦
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R) x_1)
      (HMul.hMul (α := R) (β := R) (2 : R)
        ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑y : M) : R) (↑x : M)) :
          R)))
have h : HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
    (HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R) (2 : R)
        ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
      ((IsReflective.coroot B sorry : (a : M) → R) z : R)) =
  HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
    (2 *
      HMul.hMul (α := R) (β := R) ((IsReflective.coroot B sorry : (a : M) → R) (↑y : M) : R)
        ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
Tactic: simp only [mem_setOf_eq, map_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.OfBilinear (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular.{u_1} (R := R) 2
x y : (↑{x : M | B.IsReflective x} : Type u_2)
z : M
⊢ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
      (HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) (2 : R)
          ((((B : (a : M) → M →ₗ[R] R) (↑y : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
        ((IsReflective.coroot B ⋯ : (a : M) → R) z : R)) =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
      (2 *
        HMul.hMul (α := R) (β := R) ((IsReflective.coroot B ⋯ : (a : M) → R) (↑y : M) : R)
          ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R))
have h : HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R) *
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) z : R) =
  HMul.hMul (β := R)
    (2 *
      HMul.hMul (α := R) (β := R) (2 : R)
        ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑y : M) : R))
    ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) z : R)
Tactic: rw [← mul_assoc _ _ (B z x), ← mul_assoc _ _ (B z x), mul_left_comm,
      apply_self_mul_coroot_apply B x.2, mul_left_comm (B x x), apply_self_mul_coroot_apply B x.2,
      ← hSB.eq x y, RingHom.id_apply, ← hSB.eq x z, RingHom.id_apply]
-- 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
⊢ P.IsReduced ↔
    ∀ (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)
have rw : (∀ (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: rw [isReduced_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
⊢ (∀ (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)
have 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)
Tactic: refine ⟨fun h i j hij hLin ↦ ?_, fun h i j hLin  ↦ ?_⟩
-- 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
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)
⊢ (∀ (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)
have 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)
Tactic: refine ⟨fun h i j hij hLin ↦ ?_, fun h i j hLin  ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (hypothesis)
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)
have 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)
Tactic: specialize h i j hLin
Cleared hypotheses: h
-- 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
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)
have 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)
Tactic: rcases eq_or_ne i j with rfl | h'
Cleared hypotheses: j, hLin
-- 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
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)
⊢ 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)
have 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)
Tactic: rcases eq_or_ne i j with rfl | h'
-- 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
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)
⊢ 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)
have 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)
Tactic: tauto
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (hypothesis)
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)
⊢ 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)
have 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)
Tactic: have := IsReduced.eq_or_eq_neg (P := P) i j
-- 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
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)
have 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)
Tactic: refine ⟨fun h ↦ ?_, fun ⟨h, h'⟩ ↦ linearIndependent P h h'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (hypothesis)
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)
⊢ i ≠ j ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
have 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
Tactic: rw [LinearIndependent.pair_iff] at h
Cleared hypotheses: h
-- 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
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
⊢ i ≠ j ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
have 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
Tactic: contrapose! h
Cleared hypotheses: h
-- 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
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)
⊢ ∃ (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
have 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
Tactic: rcases eq_or_ne i j with rfl | h'
Cleared hypotheses: j, h
-- 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
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
⊢ ∃ (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
have 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
Tactic: rcases eq_or_ne i j with rfl | h'
-- 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
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) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 ∧
      ∀ (_ : s = 0), t ≠ 0
have 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
Tactic: rw [h h']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (hypothesis)
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 (β := M) n ((P.root : (a : ι) → M) i : M) ∉ range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
have this : ¬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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (hypothesis)
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)
⊢ False
have this₁ : 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
Cleared hypotheses: this