awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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))
⊢ 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:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)

Tactic:
replace hk : P.root k = P.root l - P.root j := by rw [hk, hl]; module
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)
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))
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M)
⊢ b.IsPos k

Tactic:
(hw hi hl hij).sub hj hk

Premises used: RootPairing.Base.IsPos.sub
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)
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))
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) j : M)
⊢ b.IsPos k

Tactic:
exact (hw hi hl hij).sub hj hk

Premises used: RootPairing.Base.IsPos.sub
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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))
rw₃ 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))
⊢ (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:
rw [root_reflectionPerm, neg_smul, reflection_apply_root' ℤ, sub_eq_add_neg]

Premises used: neg_smul, RootPairing.reflection_apply_root', sub_eq_add_neg, Int, RootPairing.root_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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))

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]
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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))
⊢ b.IsPos ((P.reflectionPerm j : (a : ι) → ι) i)

Tactic:
hi.add_zsmul hij hj this

Premises used: RootPairing.Base.IsPos.add_zsmul
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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))
⊢ b.IsPos ((P.reflectionPerm j : (a : ι) → ι) i)

Tactic:
exact hi.add_zsmul hij hj this

Premises used: RootPairing.Base.IsPos.add_zsmul
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
generalize : ∀ (N_1 : ℤ) (hN : b.height i = N_1), p i
⊢ p i

Tactic:
generalize hN : b.height i = N

Premises used: RootPairing.Base.height
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
h₀ : b.IsPos i
hN : b.height i = 0
⊢ p i

Tactic:
False.elim <| b.height_ne_zero i hN

Premises used: False.elim, RootPairing.Base.height_ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
h₀ : b.IsPos i
hN : b.height i = 0
⊢ p i

Tactic:
exact False.elim <| b.height_ne_zero i hN

Premises used: False.elim, RootPairing.Base.height_ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
succ : ∀ (j : ι) (hj : j ∈ b.support) (hj' : 0 < P.pairingIn ℤ j i), p i
⊢ p i

Tactic:
obtain ⟨j, hj, hj'⟩ := h₀.exists_mem_support_pos_pairingIn

Premises used: RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
⊢ 0 < P.pairingIn ℤ i j

Tactic:
rw [P.zero_lt_pairingIn_iff'] at hj'

Premises used: RootPairing.zero_lt_pairingIn_iff'
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
succ₁ : ∀ (hij : i ≠ j), p i
⊢ p i

Tactic:
rcases eq_or_ne i j with rfl | hij

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
hj : i ∈ b.support
hj' : 0 < P.pairingIn ℤ i i
⊢ p i

Tactic:
h₁ i hj
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
hj : i ∈ b.support
hj' : 0 < P.pairingIn ℤ i i
⊢ p i

Tactic:
exact h₁ i hj
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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
⊢ p i

Tactic:
obtain ⟨k, hk⟩ := P.root_sub_root_mem_of_pairingIn_pos hj' hij

Premises used: RootPairing.root_sub_root_mem_of_pairingIn_pos
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)
rw : b.height i - 1 = (↑n : ℤ)
⊢ b.height k = (↑n : ℤ)

Tactic:
rw [b.height_sub hk, height_one_of_mem_support hj]

Premises used: RootPairing.Base.height_one_of_mem_support, RootPairing.Base.height_sub
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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 i - 1 = (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)
succ : ∀ (hkn : b.height k = (↑n : ℤ)), p i
⊢ p i

Tactic:
have hkn : b.height k = n := by rw [b.height_sub hk, height_one_of_mem_support hj]; lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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 : ℤ)
rw : 0 ≤ b.height k
⊢ b.IsPos k

Tactic:
rw [isPos_iff']

Premises used: RootPairing.Base.isPos_iff'
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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 : ℤ)
⊢ 0 ≤ b.height k

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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

Tactic:
have hkpos : b.IsPos k := by rw [isPos_iff']; lia