awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : IsAddTorsionFree 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)
h₁ :
  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.coxeterWeight i j = 4
have h₂ : ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
Tactic: rw [LinearIndependent.pair_symm_iff] at h
Cleared hypotheses: 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
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  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.coxeterWeight i j = 4
have h₂ : HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
Tactic: have h₂ := P.pairing_smul_root_eq_of_not_linearIndependent 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
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  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)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
⊢ P.coxeterWeight i j = 4
have suffices : HSMul.hSMul (β := M) (P.coxeterWeight i j) ((P.root : (a : ι) → M) i : M) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)
Tactic: suffices P.coxeterWeight i j • P.root i = (4 : R) • P.root i from
    smul_left_injective R (P.ne_zero i) 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  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)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (β := M) (P.pairing i j * P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
have rw : P.pairing i j • HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
  P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
Tactic: rw [mul_smul, 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
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  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)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
rw :
  P.pairing i j • HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul (β := M) (P.pairing i j * P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
have rw₁ : P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M) =
  P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
Tactic: rw [mul_smul, 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
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  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)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
⊢ P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)
have rw : HSMul.hSMul (β := M) (HMul.hMul (α := R) 2 2) ((P.root : (a : ι) → M) i : M) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)
Tactic: rw [smul_comm, h₂, ← mul_smul]
-- 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
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  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)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (β := M) (P.coxeterWeight i j) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)
have calc : HSMul.hSMul (β := M) (P.coxeterWeight i j) ((P.root : (a : ι) → M) i : M) =
  HSMul.hSMul (β := M) (P.pairing i j * P.pairing j i) ((P.root : (a : ι) → M) i : M)
Tactic: calc P.coxeterWeight i j • P.root i
      = (P.pairing i j * P.pairing j i) • P.root i := by rfl
    _ = P.pairing i j • (2 : R) • P.root j := by rw [mul_smul, h₁]
    _ = (4 : R) • P.root i := by rw [smul_comm, h₂, ← mul_smul]; 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
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  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)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
calc :
  HSMul.hSMul (β := M) (P.coxeterWeight i j) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M) (P.pairing i j * P.pairing j i) ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (β := M) (P.coxeterWeight i j) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)
have calc₁ : HSMul.hSMul (β := M) (P.pairing i j * P.pairing j i) ((P.root : (a : ι) → M) i : M) =
  P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
Tactic: calc P.coxeterWeight i j • P.root i
      = (P.pairing i j * P.pairing j i) • P.root i := by rfl
    _ = P.pairing i j • (2 : R) • P.root j := by rw [mul_smul, h₁]
    _ = (4 : R) • P.root i := by rw [smul_comm, h₂, ← mul_smul]; 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
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  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)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
calc :
  HSMul.hSMul (β := M) (P.coxeterWeight i j) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M) (P.pairing i j * P.pairing j i) ((P.root : (a : ι) → M) i : M)
calc₁ :
  HSMul.hSMul (β := M) (P.pairing i j * P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul (β := M) (P.coxeterWeight i j) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)
have calc₂ : P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)
Tactic: calc P.coxeterWeight i j • P.root i
      = (P.pairing i j * P.pairing j i) • P.root i := by rfl
    _ = P.pairing i j • (2 : R) • P.root j := by rw [mul_smul, h₁]
    _ = (4 : R) • P.root i := by rw [smul_comm, h₂, ← mul_smul]; 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
⊢ P.coxeterWeight 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.coxeterWeight i j = 4 ↔ ¬P.coxeterWeight i j ≠ 4
Tactic: rw [P.linearIndependent_iff_coxeterWeight_ne_four, 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
rw : P.coxeterWeight i j = 4 ↔ ¬P.coxeterWeight i j ≠ 4
⊢ P.coxeterWeight 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.coxeterWeight i j = 4 ↔ P.coxeterWeight i j = 4
Tactic: rw [P.linearIndependent_iff_coxeterWeight_ne_four, 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 : P.IsReduced
inst_10 : IsTorsionFree R N
⊢ P.flip.IsReduced
have refine : ∀ (i j : ι)
  (h :
    ¬LinearIndependent.{0, u_2, u_4} (ι := Fin (Nat.succ 0).succ) R (M := N)
        (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) j] : Fin (Nat.succ 0).succ → N)),
  Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) j : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)
Tactic: refine ⟨fun i 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
S : Type u_5
i_1 j_1 : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i j : ι
h :
  ¬LinearIndependent.{0, u_2, u_4} (ι := Fin (Nat.succ 0).succ) R (M := N)
      (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) j] : Fin (Nat.succ 0).succ → N)
⊢ Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) j : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)
have inl : ∀
  (h :
    ¬LinearIndependent.{0, u_2, u_4} R (M := N)
        (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) i] : Fin (Nat.succ 0).succ → N)),
  Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) i : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) i : N)
Tactic: rcases eq_or_ne i j with rfl | hij
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
S : Type u_5
i_1 j_1 : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i j : ι
h :
  ¬LinearIndependent.{0, u_2, u_4} (ι := Fin (Nat.succ 0).succ) R (M := N)
      (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) j] : Fin (Nat.succ 0).succ → N)
inl :
  ∀
    (h :
      ¬LinearIndependent.{0, u_2, u_4} R (M := N)
          (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) i] : Fin (Nat.succ 0).succ → N)),
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) i : N) ∨
      Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) i : N)
⊢ Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) j : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)
have inr : ∀ (hij : i ≠ j),
  Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) j : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)
Tactic: rcases eq_or_ne i j with rfl | hij
-- 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_1 j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i : ι
h :
  ¬LinearIndependent.{0, u_2, u_4} R (M := N)
      (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) i] : Fin (Nat.succ 0).succ → N)
⊢ Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) i : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) i : N)
have inl : ¬Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) i : N) →
  Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) i : N)
Tactic: tauto
-- 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_1 j_1 : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i j : ι
h :
  ¬LinearIndependent.{0, u_2, u_4} (ι := Fin (Nat.succ 0).succ) R (M := N)
      (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) j] : Fin (Nat.succ 0).succ → N)
hij : i ≠ j
⊢ Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) j : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)
have inr : Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)
Tactic: right
-- 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
S : Type u_5
i_1 j_1 : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i j : ι
h :
  ¬LinearIndependent.{0, u_2, u_4} (ι := Fin (Nat.succ 0).succ) R (M := N)
      (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) j] : Fin (Nat.succ 0).succ → N)
hij : i ≠ j
⊢ Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)
have h₁ : ¬(i ≠ j ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M))
Tactic: rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight_flip,
    coxeterWeight_eq_four_iff_not_linearIndependent, IsReduced.linearIndependent_iff] at h
Cleared hypotheses: h, hij
-- 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
S : Type u_5
i_1 j_1 : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i j : ι
h : ¬(i ≠ j ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M))
hij : i ≠ j
⊢ Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)
have h₁ : ∀ (_ : i ≠ j), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
Tactic: push Not 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
⊢ P.pairing i j = 2 ∧ P.pairing j i = 2 ↔ i = j
have refine : P.pairing i j = 2 ∧ P.pairing j i = 2 → ∀ (h₁ : P.pairing i j = 2) (h₂ : P.pairing j i = 2), i = j
Tactic: refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun h ↦ by simp [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
h : P.pairing i j = 2 ∧ P.pairing j i = 2
h₁ : P.pairing i j = 2
h₂ : P.pairing j i = 2
⊢ ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
have rw : HMul.hMul (α := R) 2 2 = 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
h : P.pairing i j = 2 ∧ P.pairing j i = 2
h₁ : P.pairing i j = 2
h₂ : P.pairing j i = 2
⊢ i = j
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₂]; norm_num
-- 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
h : P.pairing i j = 2 ∧ P.pairing j i = 2
h₁ : P.pairing i j = 2
h₂ : P.pairing j i = 2
this :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ i = j
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