awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
⊢ b.IsPos k
have hij₁ : 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: replace hij : LinearIndependent R ![P.root j, P.root i] := by
    refine IsReduced.linearIndependent P hij.symm fun contra ↦ ?_
    letI := P.indexNeg
    replace contra : i = -j := by rw [eq_comm, neg_eq_iff_eq_neg]; simpa using contra
    rw [contra, isPos_iff, height_reflectionPerm_self, height_one_of_mem_support hj] at hi
    lia
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M))
hij :
  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)
⊢ (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M))
have rw : HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
    (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M)) =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M))
Tactic: rw [hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M))
hij :
  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)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
have hk₁ : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M)))
Tactic: replace hk : P.root i + (w + 1) • P.root j ∈ range P.root := ⟨k, by rw [hk]; module⟩
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hij :
  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)
hk :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M)))
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
have simp : ∀ (hk : w + 1 ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i),
  w ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i
Tactic: simp only [natCast_zsmul, root_add_nsmul_mem_range_iff_le_chainTopCoeff hij] at hk ⊢
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M))
hij :
  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)
⊢ b.IsPos k
have succ : ∀ (l : ι)
  (hl :
    (P.root : (a : ι) → M) l =
      HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
        (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M))),
  b.IsPos k
Tactic: obtain ⟨l, hl⟩ : P.root i + (w : ℤ) • P.root j ∈ range P.root := by
      replace hk : P.root i + (w + 1) • P.root j ∈ range P.root := ⟨k, by rw [hk]; module⟩
      simp only [natCast_zsmul, root_add_nsmul_mem_range_iff_le_chainTopCoeff hij] at hk ⊢
      lia
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M))
hij :
  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)
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M))
⊢ (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M)
have rw : HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
    (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M)) =
  HAdd.hAdd (β := M)
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
    ((P.root : (a : ι) → M) j : M)
Tactic: rw [hk, hl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M))
hij :
  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)
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M))
⊢ b.IsPos k
have hk₁ : (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M)
Tactic: replace hk : P.root k = P.root l + P.root j := by rw [hk, hl]; module
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HSub.hSub (α := ℤ) (-(↑w : ℤ)) 1) ((P.root : (a : ι) → M) j : M))
hij :
  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)
⊢ (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M))
have rw : HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
    (HSMul.hSMul (β := M) (HSub.hSub (α := ℤ) (-(↑w : ℤ)) 1) ((P.root : (a : ι) → M) j : M)) =
  HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M))
Tactic: rw [hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HSub.hSub (α := ℤ) (-(↑w : ℤ)) 1) ((P.root : (a : ι) → M) j : M))
hij :
  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)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M)))
have hk₁ : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M)))
Tactic: replace hk : P.root i - (w + 1) • P.root j ∈ range P.root := ⟨k, by rw [hk]; module⟩
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hij :
  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)
hk :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M)))
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M)))
have rw : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) w ((P.root : (a : ι) → M) j : M)))
Tactic: rw [neg_smul, ← sub_eq_add_neg, natCast_zsmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hij :
  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)
hk :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M)))
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) w ((P.root : (a : ι) → M) j : M)))
have simp : ∀ (hk : w + 1 ≤ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i),
  w ≤ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i
Tactic: simp only [root_sub_nsmul_mem_range_iff_le_chainBotCoeff hij] at hk ⊢
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HSub.hSub (α := ℤ) (-(↑w : ℤ)) 1) ((P.root : (a : ι) → M) j : M))
hij :
  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)
⊢ b.IsPos k
have pred : ∀ (l : ι)
  (hl :
    (P.root : (a : ι) → M) l =
      HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
        (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M))),
  b.IsPos k
Tactic: obtain ⟨l, hl⟩ : P.root i + (-w : ℤ) • P.root j ∈ range P.root := by
      replace hk : P.root i - (w + 1) • P.root j ∈ range P.root := ⟨k, by rw [hk]; module⟩
      rw [neg_smul, ← sub_eq_add_neg, natCast_zsmul]
      simp only [root_sub_nsmul_mem_range_iff_le_chainBotCoeff hij] at hk ⊢
      lia
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HSub.hSub (α := ℤ) (-(↑w : ℤ)) 1) ((P.root : (a : ι) → M) j : M))
hij :
  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)
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M))
⊢ (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M)
have rw : HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
    (HSMul.hSMul (β := M) (HSub.hSub (α := ℤ) (-(↑w : ℤ)) 1) ((P.root : (a : ι) → M) j : M)) =
  HSub.hSub (β := M)
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M)))
    ((P.root : (a : ι) → M) j : M)
Tactic: rw [hk, hl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M)))
    (hij :
      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)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HSub.hSub (α := ℤ) (-(↑w : ℤ)) 1) ((P.root : (a : ι) → M) j : M))
hij :
  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)
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (α := ℤ) (β := M) (-(↑w : ℤ)) ((P.root : (a : ι) → M) j : M))
⊢ b.IsPos k
have hk₁ : (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M)
Tactic: replace hk : P.root k = P.root l - P.root j := by rw [hk, hl]; module
Cleared hypotheses: hk