awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
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)
have 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)
Tactic: simp only [← neg_eq_iff_eq_neg]
-- 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 : 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)
have this : IsAddTorsionFree M
Tactic: have : IsAddTorsionFree M := .of_isTorsionFree R M
-- 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 : 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
⊢ 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)
have this₁ : IsAddTorsionFree N
Tactic: have : IsAddTorsionFree N := .of_isTorsionFree R N
-- 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 : 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)
have 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)
Tactic: refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun 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 : 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)
⊢ 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)
have 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
Tactic: refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun 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 : 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)
have rw : HMul.hMul (α := R) 1 4 = 4
Tactic: rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, 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 : 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
⊢ (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
have 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)
Tactic: have : ¬ LinearIndependent R ![P.root i, P.root j] := by
      rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]; 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
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)
⊢ (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
have 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)
Tactic: replace this := P.pairing_smul_root_eq_of_not_linearIndependent this
Cleared hypotheses: this
-- 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 : 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)
⊢ (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
have 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)
Tactic: rw [h₂, show (4 : R) = 2 * 2 by norm_num, mul_smul] at this
Cleared hypotheses: this
-- 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 : 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.pairing i j = 1 ∧ P.pairing j i = 4
have h₁ : (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
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 : 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.pairing i j = 1 ∧ P.pairing j i = 4
have 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)
Tactic: rw [pairing, pairing, 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 : 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)
⊢ 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)
have refine_2 : P.pairing i j = 1
Tactic: norm_num
-- 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 : 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.pairing i j = 1
have refine_2 : HSMul.hSMul (α := R) 2 (P.pairing i j) = HSMul.hSMul (α := R) (β := R) 2 1
Tactic: suffices (2 : R) • P.pairing i j = (2 : R) • 1 from h2 this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
⊢ 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) ↔
    P.coxeterWeightIn S i j ≠ 4
have rw : P.coxeterWeight i j ≠ 4 ↔ P.coxeterWeightIn S i j ≠ 4
Tactic: rw [linearIndependent_iff_coxeterWeight_ne_four, ← P.algebraMap_coxeterWeightIn S,
    ← map_ofNat (algebraMap S R), (algebraMap_injective S R).ne_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
rw : P.coxeterWeight i j ≠ 4 ↔ P.coxeterWeightIn S i j ≠ 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) ↔
    P.coxeterWeightIn S i j ≠ 4
have rw₁ : Ne.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.coxeterWeightIn S i j) : R) (4 : R) ↔
  P.coxeterWeightIn S i j ≠ 4
Tactic: rw [linearIndependent_iff_coxeterWeight_ne_four, ← P.algebraMap_coxeterWeightIn S,
    ← map_ofNat (algebraMap S R), (algebraMap_injective S R).ne_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
rw : P.coxeterWeight i j ≠ 4 ↔ P.coxeterWeightIn S i j ≠ 4
rw₁ :
  Ne.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.coxeterWeightIn S i j) : R) (4 : R) ↔
    P.coxeterWeightIn S i j ≠ 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) ↔
    P.coxeterWeightIn S i j ≠ 4
have rw₂ : Ne.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.coxeterWeightIn S i j) : R)
    ((algebraMap S R : (a : S) → R) 4 : R) ↔
  P.coxeterWeightIn S i j ≠ 4
Tactic: rw [linearIndependent_iff_coxeterWeight_ne_four, ← P.algebraMap_coxeterWeightIn S,
    ← map_ofNat (algebraMap S R), (algebraMap_injective S R).ne_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
rw : P.coxeterWeight i j ≠ 4 ↔ P.coxeterWeightIn S i j ≠ 4
rw₁ :
  Ne.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.coxeterWeightIn S i j) : R) (4 : R) ↔
    P.coxeterWeightIn S i j ≠ 4
rw₂ :
  Ne.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.coxeterWeightIn S i j) : R)
      ((algebraMap S R : (a : S) → R) 4 : R) ↔
    P.coxeterWeightIn S i j ≠ 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) ↔
    P.coxeterWeightIn S i j ≠ 4
have rw₃ : P.coxeterWeightIn S i j ≠ 4 ↔ P.coxeterWeightIn S i j ≠ 4
Tactic: rw [linearIndependent_iff_coxeterWeight_ne_four, ← P.algebraMap_coxeterWeightIn S,
    ← map_ofNat (algebraMap S R), (algebraMap_injective S R).ne_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
⊢ P.coxeterWeightIn S i j = 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)
have rw : P.coxeterWeightIn S i j = 4 ↔ ¬P.coxeterWeightIn S i j ≠ 4
Tactic: rw [P.linearIndependent_iff_coxeterWeightIn_ne_four S, not_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
rw : P.coxeterWeightIn S i j = 4 ↔ ¬P.coxeterWeightIn S i j ≠ 4
⊢ P.coxeterWeightIn S i j = 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)
have rw₁ : P.coxeterWeightIn S i j = 4 ↔ P.coxeterWeightIn S i j = 4
Tactic: rw [P.linearIndependent_iff_coxeterWeightIn_ne_four S, not_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : P.IsReduced
h : i ≠ j
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ P.coxeterWeightIn S i j ≠ 4
have rw : 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 [ne_eq, coxeterWeightIn_eq_four_iff_not_linearIndependent, not_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : IsTorsionFree R N
⊢ P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
have rw : P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔ P.pairing i j = 1 ∧ P.pairing j i = 4
Tactic: rw [← P.pairing_one_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
    ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff,
    (algebraMap_injective S R).eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : IsTorsionFree R N
rw : P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔ P.pairing i j = 1 ∧ P.pairing j i = 4
⊢ P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
have rw₁ : P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R) (1 : R) ∧ P.pairing j i = 4
Tactic: rw [← P.pairing_one_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
    ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff,
    (algebraMap_injective S R).eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : IsTorsionFree R N
rw : P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔ P.pairing i j = 1 ∧ P.pairing j i = 4
rw₁ :
  P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R) (1 : R) ∧ P.pairing j i = 4
⊢ P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
have rw₂ : P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R) (1 : R) ∧
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R) (4 : R)
Tactic: rw [← P.pairing_one_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
    ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff,
    (algebraMap_injective S R).eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Reduced (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : CommRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : P.IsValuedIn S
inst_13 : IsTorsionFree R N
rw : P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔ P.pairing i j = 1 ∧ P.pairing j i = 4
rw₁ :
  P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R) (1 : R) ∧ P.pairing j i = 4
rw₂ :
  P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R) (1 : R) ∧
      Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R) (4 : R)
⊢ P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
    (P.root : (a : ι) → M) j = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
have rw₃ : P.pairingIn S i j = 1 ∧ P.pairingIn S j i = 4 ↔
  Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
      ((algebraMap S R : (a : S) → R) 1 : R) ∧
    Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R) (4 : R)
Tactic: rw [← P.pairing_one_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
    ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff,
    (algebraMap_injective S R).eq_iff]