awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i j k : ι
z : ℤ
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))
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 zero : ∀ {i k : ι} (hi : b.IsPos i)
  (hk :
    (P.root : (a : ι) → M) k =
      HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
        (HSMul.hSMul (α := ℤ) (β := M) 0 ((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
Tactic: induction z generalizing i k with
  | zero => simp_all
  | succ w hw =>
    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
    replace hk : P.root k = P.root l + P.root j := by rw [hk, hl]; module
    exact (hw hi hl hij).add (b.isPos_of_mem_support hj) hk
  | pred w hw =>
    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
    replace hk : P.root k = P.root l - P.root j := by rw [hk, hl]; module
    exact (hw hi hl hij).sub hj hk
Cleared hypotheses: i, k, z, hi, hk, 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
i j k : ι
z : ℤ
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))
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)
zero :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) 0 ((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
⊢ b.IsPos k
have succ : ∀ (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
Tactic: induction z generalizing i k with
  | zero => simp_all
  | succ w hw =>
    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
    replace hk : P.root k = P.root l + P.root j := by rw [hk, hl]; module
    exact (hw hi hl hij).add (b.isPos_of_mem_support hj) hk
  | pred w hw =>
    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
    replace hk : P.root k = P.root l - P.root j := by rw [hk, hl]; module
    exact (hw hi hl hij).sub hj hk
Cleared hypotheses: i, k, z, hi, hk, 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
i j : ι
hi : b.IsPos i
hj : j ∈ b.support
hij : i ≠ j
⊢ (P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) i : ι) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (-P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
have rw : (P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
    (HSMul.hSMul (β := M) (-P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
Tactic: rw [root_reflectionPerm, neg_smul, reflection_apply_root' ℤ, sub_eq_add_neg]
-- 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
i j : ι
hi : b.IsPos i
hj : j ∈ b.support
hij : i ≠ j
rw :
  (P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (-P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
⊢ (P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) i : ι) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (-P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
have rw₁ : (P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
    (-HSMul.hSMul (β := M) (P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
Tactic: rw [root_reflectionPerm, neg_smul, reflection_apply_root' ℤ, sub_eq_add_neg]
-- 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
i j : ι
hi : b.IsPos i
hj : j ∈ b.support
hij : i ≠ j
rw :
  (P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (-P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
rw₁ :
  (P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (-HSMul.hSMul (β := M) (P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
⊢ (P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) i : ι) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (-P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
have rw₂ : HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
    (HSMul.hSMul (β := M) (P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M)) =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
    (-HSMul.hSMul (β := M) (P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
Tactic: rw [root_reflectionPerm, neg_smul, reflection_apply_root' ℤ, sub_eq_add_neg]
-- 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
i j : ι
hi : b.IsPos i
hj : j ∈ b.support
hij : i ≠ j
rw :
  (P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (-P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
rw₁ :
  (P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (-HSMul.hSMul (β := M) (P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
rw₂ :
  HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M)) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (-HSMul.hSMul (β := M) (P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
⊢ (P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) i : ι) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (-P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
have rw₃ : HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
    (-HSMul.hSMul (β := M) (P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M)) =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
    (-HSMul.hSMul (β := M) (P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
Tactic: rw [root_reflectionPerm, neg_smul, reflection_apply_root' ℤ, sub_eq_add_neg]
-- 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 : ι
hi : b.IsPos i
hj : j ∈ b.support
hij : i ≠ j
⊢ b.IsPos ((P.reflectionPerm j : (a : ι) → ι) i)
have this : (P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) i : ι) =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
    (HSMul.hSMul (β := M) (-P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
Tactic: have : P.root (P.reflectionPerm j i) = P.root i + (-P.pairingIn ℤ i j) • P.root j := by
    rw [root_reflectionPerm, neg_smul, reflection_apply_root' ℤ, sub_eq_add_neg]
-- 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
i : ι
h₀ : b.IsPos i
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
⊢ p i
have generalize : ∀ (N_1 : ℤ) (hN : b.height i = N_1), p i
Tactic: generalize hN : b.height i = N
-- 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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i
i : ι
h₀ : b.IsPos i
hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ p i
have succ : ∀ (j : ι) (hj : j ∈ b.support) (hj' : 0 < P.pairingIn ℤ j i), p i
Tactic: obtain ⟨j, hj, hj'⟩ := h₀.exists_mem_support_pos_pairingIn
-- 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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i
i : ι
h₀ : b.IsPos i
hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ j i
⊢ p i
have hj'₁ : 0 < P.pairingIn ℤ i j
Tactic: rw [P.zero_lt_pairingIn_iff'] at hj'
Cleared hypotheses: hj'
-- 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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i
i : ι
h₀ : b.IsPos i
hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
⊢ p i
have succ : ∀ (hj : i ∈ b.support) (hj' : 0 < P.pairingIn ℤ i i), p i
Tactic: rcases eq_or_ne i j with rfl | hij
Cleared hypotheses: j, hj, hj'
-- 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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i
i : ι
h₀ : b.IsPos i
hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
succ : ∀ (hj : i ∈ b.support) (hj' : 0 < P.pairingIn ℤ i i), p i
⊢ p i
have succ₁ : ∀ (hij : i ≠ j), p i
Tactic: rcases eq_or_ne i j with rfl | 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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i
i : ι
h₀ : b.IsPos i
hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
⊢ p i
have succ : ∀ (k : ι)
  (hk :
    (P.root : (a : ι) → M) k =
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)),
  p i
Tactic: obtain ⟨k, hk⟩ := P.root_sub_root_mem_of_pairingIn_pos hj' 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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i
i : ι
h₀ : b.IsPos i
hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ b.height k = (↑n : ℤ)
have rw : b.height i - 1 = (↑n : ℤ)
Tactic: rw [b.height_sub hk, height_one_of_mem_support hj]
-- 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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i
i : ι
h₀ : b.IsPos i
hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ p i
have succ : ∀ (hkn : b.height k = (↑n : ℤ)), p i
Tactic: have hkn : b.height k = n := by rw [b.height_sub hk, height_one_of_mem_support hj]; 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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i
i : ι
h₀ : b.IsPos i
hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hkn : b.height k = (↑n : ℤ)
⊢ b.IsPos k
have rw : 0 ≤ b.height k
Tactic: rw [isPos_iff']
-- 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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i
i : ι
h₀ : b.IsPos i
hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hkn : b.height k = (↑n : ℤ)
⊢ p i
have hkpos : b.IsPos k
Tactic: have hkpos : b.IsPos k := by rw [isPos_iff']; 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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i
i : ι
h₀ : b.IsPos i
hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hkn : b.height k = (↑n : ℤ)
hkpos : b.IsPos k
⊢ (P.root : (a : ι) → M) i = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M)
have rw : (P.root : (a : ι) → M) i =
  HAdd.hAdd (β := M) (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
    ((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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = -(↑n : ℤ)), p i
i : ι
h₀ : b.IsPos i
hN : b.height i = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ p i
have h₃ : 0 < b.height i
Tactic: rw [isPos_iff] at h₀
Cleared hypotheses: h₀, hN
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N_1 : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
P : RootPairing ι R M N_1
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
N : ℤ
hN : b.height i = N
⊢ p i
have zero : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = 0), p i
Tactic: induction N using Int.induction_on generalizing i with
  | zero => exact False.elim <| b.height_ne_zero i hN
  | succ n ih =>
    obtain ⟨j, hj, hj'⟩ := h₀.exists_mem_support_pos_pairingIn
    rw [P.zero_lt_pairingIn_iff'] at hj'
    rcases eq_or_ne i j with rfl | hij; · exact h₁ i hj
    obtain ⟨k, hk⟩ := P.root_sub_root_mem_of_pairingIn_pos hj' hij
    have hkn : b.height k = n := by rw [b.height_sub hk, height_one_of_mem_support hj]; lia
    have hkpos : b.IsPos k := by rw [isPos_iff']; lia
    exact h₂ k j i (by rw [hk]; module) (ih hkpos hkn) hj
  | pred n ih =>
    rw [isPos_iff] at h₀
    lia
Cleared hypotheses: i, h₀, N, hN