awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i_1 j_1 : ι
h_1 :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i_1, (P.root : (a : ι) → M) j_1] : Fin (Nat.succ 0).succ → 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)
⊢ (P.reflection i : (a : M) → M)
      ((P.root : (a : ι) → M) (chainBotIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M)
        ((↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) - P.pairingIn ℤ j i)
        ((P.root : (a : ι) → M) i : M))
have simp : HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (↑(P.pairingIn ℤ j i) : R) ((P.root : (a : ι) → M) i : M)) +
    HSMul.hSMul (β := M) (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)
      ((P.root : (a : ι) → M) i : M) =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
    (HSMul.hSMul (β := M)
      ((↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) - P.pairingIn ℤ j i)
      ((P.root : (a : ι) → M) i : M))
Tactic: simp [reflection_apply_root, ← P.algebraMap_pairingIn ℤ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i_1 j_1 : ι
h_1 :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i_1, (P.root : (a : ι) → M) j_1] : Fin (Nat.succ 0).succ → 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)
⊢ HSub.hSub (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) ≤
    P.pairingIn ℤ j i
have h₁ : (P.reflection i : (a : M) → M)
    ((P.root : (a : ι) → M) (chainBotIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : M) =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
    (HSMul.hSMul (β := M)
      ((↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) - P.pairingIn ℤ j i)
      ((P.root : (a : ι) → M) i : M))
Tactic: have h₁ : P.reflection i (P.root <| P.chainBotIdx i j) =
      P.root j + (P.chainBotCoeff i j - P.pairingIn ℤ j i) • P.root i := by
    simp [reflection_apply_root, ← P.algebraMap_pairingIn ℤ]
    module
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i_1 j_1 : ι
h_1 :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i_1, (P.root : (a : ι) → M) j_1] : Fin (Nat.succ 0).succ → 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)
h₁ :
  (P.reflection i : (a : M) → M)
      ((P.root : (a : ι) → M) (chainBotIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M)
        ((↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) - P.pairingIn ℤ j i)
        ((P.root : (a : ι) → M) i : M))
⊢ Membership.mem (α := M) (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    ((P.reflection i : (a : M) → M)
        ((P.root : (a : ι) → M) (chainBotIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : M) :
      M)
have rw : Membership.mem.{u_3, u_3} (α := M) (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  ((P.root : (a : ι) → M)
      ((P.reflectionPerm i : (a : ι) → ι) (chainBotIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) :
        ι) :
    M)
Tactic: rw [← root_reflectionPerm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i_1 j_1 : ι
h_1 :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i_1, (P.root : (a : ι) → M) j_1] : Fin (Nat.succ 0).succ → 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)
h₁ :
  (P.reflection i : (a : M) → M)
      ((P.root : (a : ι) → M) (chainBotIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M)
        ((↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) - P.pairingIn ℤ j i)
        ((P.root : (a : ι) → M) i : M))
⊢ HSub.hSub (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) ≤
    P.pairingIn ℤ j i
have h₂ : Membership.mem (α := M) (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  ((P.reflection i : (a : M) → M)
      ((P.root : (a : ι) → M) (chainBotIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : M) :
    M)
Tactic: have h₂ : P.reflection i (P.root <| P.chainBotIdx i j) ∈ range P.root := by
    rw [← root_reflectionPerm]
    exact mem_range_self _
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i_1 j_1 : ι
h_1 :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i_1, (P.root : (a : ι) → M) j_1] : Fin (Nat.succ 0).succ → 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)
h₁ :
  (P.reflection i : (a : M) → M)
      ((P.root : (a : ι) → M) (chainBotIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M)
        ((↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) - P.pairingIn ℤ j i)
        ((P.root : (a : ι) → M) i : M))
h₂ :
  Membership.mem (α := M) (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    ((P.reflection i : (a : M) → M)
        ((P.root : (a : ι) → M) (chainBotIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : M) :
      M)
⊢ HSub.hSub (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) ≤
    P.pairingIn ℤ j i
have h₃ : -(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) ≤
    (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) - P.pairingIn ℤ j i ∧
  (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) - P.pairingIn ℤ j i ≤
    (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
Tactic: rw [h₁, root_add_zsmul_mem_range_iff h, mem_Icc] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
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)
⊢ HSub.hSub (α := ℤ) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
    -P.pairingIn ℤ j i
have rw : HSub.hSub (α := ℤ) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
    (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
  -HSub.hSub (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
Tactic: rw [← chainBotCoeff_sub_chainTopCoeff h, neg_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
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)
rw :
  HSub.hSub (α := ℤ) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
    -HSub.hSub (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
        (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
    -P.pairingIn ℤ j i
have rw₁ : HSub.hSub (α := ℤ) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
    (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
  HSub.hSub (α := ℤ) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
    (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
Tactic: rw [← chainBotCoeff_sub_chainTopCoeff h, neg_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
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) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
        Fin (Nat.succ 0).succ → M)
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) ↔
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i,
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
          (HSMul.hSMul (β := M) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)
            ((P.root : (a : ι) → M) i : M))] :
      Fin (Nat.succ 0).succ → M)
Tactic: rw [P.root_chainTopIdx, add_comm (P.root j), ← natCast_zsmul,
      LinearIndependent.pair_add_smul_right_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
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) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)
              ((P.root : (a : ι) → M) i : M))] :
        Fin (Nat.succ 0).succ → 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) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
        Fin (Nat.succ 0).succ → M)
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) ↔
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i,
        HAdd.hAdd (β := M)
          (HSMul.hSMul (β := M) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)
            ((P.root : (a : ι) → M) i : M))
          ((P.root : (a : ι) → M) j : M)] :
      Fin (Nat.succ 0).succ → M)
Tactic: rw [P.root_chainTopIdx, add_comm (P.root j), ← natCast_zsmul,
      LinearIndependent.pair_add_smul_right_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
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) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)
              ((P.root : (a : ι) → M) i : M))] :
        Fin (Nat.succ 0).succ → M)
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) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          HAdd.hAdd (β := M)
            (HSMul.hSMul (β := M) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)
              ((P.root : (a : ι) → M) i : M))
            ((P.root : (a : ι) → M) j : M)] :
        Fin (Nat.succ 0).succ → 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) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
        Fin (Nat.succ 0).succ → M)
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) ↔
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i,
        HAdd.hAdd (β := M)
          (HSMul.hSMul (α := ℤ) (β := M)
            (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
            ((P.root : (a : ι) → M) i : M))
          ((P.root : (a : ι) → M) j : M)] :
      Fin (Nat.succ 0).succ → M)
Tactic: rw [P.root_chainTopIdx, add_comm (P.root j), ← natCast_zsmul,
      LinearIndependent.pair_add_smul_right_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
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) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)
              ((P.root : (a : ι) → M) i : M))] :
        Fin (Nat.succ 0).succ → M)
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) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          HAdd.hAdd (β := M)
            (HSMul.hSMul (β := M) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)
              ((P.root : (a : ι) → M) i : M))
            ((P.root : (a : ι) → M) j : M)] :
        Fin (Nat.succ 0).succ → M)
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) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          HAdd.hAdd (β := M)
            (HSMul.hSMul (α := ℤ) (β := M)
              (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
              ((P.root : (a : ι) → M) i : M))
            ((P.root : (a : ι) → M) j : M)] :
        Fin (Nat.succ 0).succ → 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) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
        Fin (Nat.succ 0).succ → M)
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) ↔
  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 [P.root_chainTopIdx, add_comm (P.root j), ← natCast_zsmul,
      LinearIndependent.pair_add_smul_right_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
        (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
        chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ∧
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
        (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
      0
have aux : 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) ↔
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i,
        (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
      Fin (Nat.succ 0).succ → M)
Tactic: have aux : LinearIndependent R ![P.root i, P.root j] ↔
      LinearIndependent R ![P.root i, P.root (P.chainTopIdx i j)] := by
    rw [P.root_chainTopIdx, add_comm (P.root j), ← natCast_zsmul,
      LinearIndependent.pair_add_smul_right_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
aux :
  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) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
        Fin (Nat.succ 0).succ → M)
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
        (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
        chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ∧
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
        (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
      0
have pos : ∀
  (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)),
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
        (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
        chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ∧
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
        (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
      0
Tactic: by_cases h : LinearIndependent R ![P.root i, P.root j]