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
i j k : ι
z : ℤ
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))
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
simp_rw :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ x ∈ b.support, HSMul.hSMul (β := M) (f x + (z • g) x) ((P.root : (a : ι) → M) x : M) : M)
simp_rw₁ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ x ∈ b.support, HSMul.hSMul (β := M) (f x + z • g x) ((P.root : (a : ι) → M) x : M) : M)
simp_rw₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ x ∈ b.support,
        (HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M) +
          HSMul.hSMul (β := M) (z • g x) ((P.root : (a : ι) → M) x : M)) :
      M)
simp_rw₃ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ x ∈ b.support,
        (HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M) +
          z • HSMul.hSMul (β := M) (g x) ((P.root : (a : ι) → M) x : M)) :
      M)
simp_rw₄ :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (∑ x ∈ b.support, HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M))
      (∑ x ∈ b.support, z • HSMul.hSMul (β := M) (g x) ((P.root : (a : ι) → M) x : M))
simp_rw₅ :
  (P.root : (a : ι) → M) k =
    ∑ x ∈ b.support, HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M) +
      HSMul.hSMul (β := M) z (∑ x ∈ b.support, HSMul.hSMul (β := M) (g x) ((P.root : (a : ι) → M) x : M))
simp_rw₆ :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) z (∑ x ∈ b.support, HSMul.hSMul (β := M) (g x) ((P.root : (a : ι) → M) x : M)))
simp_rw₇ :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ l ∈ b.support, HSMul.hSMul (β := M) ((f + z • g) l) ((P.root : (a : ι) → M) l : M) : M)

Tactic:
simp_rw [Pi.add_apply, Pi.smul_apply, add_smul, smul_assoc, Finset.sum_add_distrib,
      ← Finset.smul_sum, ← hf, ← hg, hk]

Premises used: smul_assoc, Finset.sum_add_distrib, Pi.add_apply, add_smul, Finset.smul_sum, Pi.smul_apply
-- 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
i j k : ι
z : ℤ
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))
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ l ∈ b.support, HSMul.hSMul (β := M) ((f + z • g) l) ((P.root : (a : ι) → M) l : M) : M)

Tactic:
have hfg : P.root k = ∑ l ∈ b.support, (f + z • g) l • P.root l := by
    simp_rw [Pi.add_apply, Pi.smul_apply, add_smul, smul_assoc, Finset.sum_add_distrib,
      ← Finset.smul_sum, ← hf, ← hg, hk]
-- 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
i j k : ι
z : ℤ
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))
f : ι → ℤ
hf :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
hfg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ l ∈ b.support, HSMul.hSMul (β := M) ((f + z • g) l) ((P.root : (a : ι) → M) l : M) : M)
simp_rw : b.height k = ∑ j ∈ b.support, f j + z • b.height j
simp_rw₁ : b.height k = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
simp_rw₂ : ∑ j ∈ b.support, (f + z • g) j = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
simp_rw₃ : ∑ x ∈ b.support, (f x + (z • g) x) = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
simp_rw₄ : ∑ x ∈ b.support, (f x + z • g x) = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
simp_rw₅ :
  HAdd.hAdd (α := ℤ) (∑ x ∈ b.support, f x) (∑ x ∈ b.support, z • g x) =
    ∑ x ∈ b.support, f x + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
⊢ b.height k = b.height i + z • b.height j

Tactic:
simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, Pi.add_apply, Pi.smul_apply,
    Finset.sum_add_distrib, Finset.smul_sum]

Premises used: RootPairing.Base.height_eq_sum, Finset.sum_add_distrib, Pi.add_apply, Finset.smul_sum, Pi.smul_apply
-- 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
i : ι
⊢ b.IsPos i ↔ 0 < b.height i

Tactic:
Iff.rfl

Premises used: Iff.rfl, RootPairing.Base.IsPos
-- 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
i : ι
⊢ b.height i ≠ 0

Tactic:
have := b.height_ne_zero i
-- 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
i : ι
this : b.height i ≠ 0
⊢ 0 < b.height i ↔ 0 ≤ b.height i

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
i : ι
rw : 0 < b.height i ∨ 0 < -b.height i
⊢ b.IsPos i ∨ b.IsPos (-i)

Tactic:
rw [isPos_iff, isPos_iff, height_reflectionPerm_self]

Premises used: RootPairing.Base.height_reflectionPerm_self, 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
i : ι
this : b.height i ≠ 0
⊢ 0 < b.height i ∨ 0 < -b.height i

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
i : ι
rw : 0 < -b.height i ↔ ¬0 < b.height i
⊢ b.IsPos (-i) ↔ ¬b.IsPos i

Tactic:
rw [isPos_iff, isPos_iff, height_reflectionPerm_self]

Premises used: RootPairing.Base.height_reflectionPerm_self, 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
i : ι
this : b.height i ≠ 0
⊢ 0 < -b.height i ↔ ¬0 < b.height i

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
i : ι
h : i ∈ b.support
rw : LT.lt (α := ℤ) 0 1
⊢ b.IsPos i

Tactic:
rw [isPos_iff, height_one_of_mem_support h]

Premises used: RootPairing.Base.height_one_of_mem_support, 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
i : ι
h : i ∈ b.support
⊢ LT.lt (α := ℤ) 0 1

Tactic:
Int.one_pos

Premises used: Int.one_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
i : ι
h : i ∈ b.support
⊢ LT.lt (α := ℤ) 0 1

Tactic:
exact Int.one_pos

Premises used: Int.one_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
i j k : ι
hi : b.IsPos i
hj : b.IsPos j
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ 0 < b.height i

Tactic:
rw [isPos_iff] at hi hj ⊢

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
i j k : ι
hi : b.IsPos i
hj : b.IsPos j
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi₁ : 0 < b.height i
⊢ 0 < b.height j

Tactic:
rw [isPos_iff] at hi hj ⊢

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
i j k : ι
hi : b.IsPos i
hj : b.IsPos j
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi₁ : 0 < b.height i
hj₁ : 0 < b.height j
⊢ (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)

Tactic:
rw [isPos_iff] at hi hj ⊢

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
i j k : ι
hi : 0 < b.height i
hj : 0 < b.height j
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
rw : 0 < b.height i + b.height j
⊢ 0 < b.height k

Tactic:
rw [b.height_add hk]

Premises used: RootPairing.Base.height_add
-- 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
i j k : ι
hi : 0 < b.height i
hj : 0 < b.height j
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ 0 < b.height i + b.height j

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
i j k : ι
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ 0 < b.height i

Tactic:
rw [isPos_iff] at hi

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
i j k : ι
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi₁ : 0 < b.height i
⊢ j ∈ b.support

Tactic:
rw [isPos_iff] at hi

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
i j k : ι
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi₁ : 0 < b.height i
hj₁ : j ∈ b.support
⊢ (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)

Tactic:
rw [isPos_iff] at hi

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
i j k : ι
hi : 0 < b.height i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
rw : 0 ≤ b.height i - 1
⊢ b.IsPos k

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

Premises used: RootPairing.Base.height_one_of_mem_support, RootPairing.Base.height_sub, 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
i j k : ι
hi : 0 < b.height i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ 0 ≤ b.height i - 1

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 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
by_contra! : ∀ (contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0), False
⊢ ∃ j ∈ b.support, 0 < P.pairingIn ℤ j i

Tactic:
by_contra! contra
-- 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 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
this : P.pairingIn ℤ i i ≤ 0
⊢ False

Tactic:
simp_all
-- 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 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
suffices : P.pairingIn ℤ i i ≤ 0
⊢ False

Tactic:
suffices P.pairingIn ℤ i i ≤ 0 by simp_all
-- 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 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
obtain :
  ∀ (f : ι → ℤ) (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf₁ : 0 < f ∨ f < 0)
    (hf₂ :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)),
    P.pairingIn ℤ i i ≤ 0
⊢ P.pairingIn ℤ i i ≤ 0

Tactic:
obtain ⟨f, hf₀, hf₁, hf₂⟩ := b.exists_root_eq_sum_int i

Premises used: RootPairing.Base.exists_root_eq_sum_int
-- 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 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₁ : 0 < f ∨ f < 0
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
⊢ 0 < f

Tactic:
hf₁.resolve_right ?_

Premises used: Or.resolve_right
-- 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 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₁ : 0 < f ∨ f < 0
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
refine : ¬f < 0
⊢ 0 < f

Tactic:
refine hf₁.resolve_right ?_

Premises used: Or.resolve_right
-- 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 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₁ : 0 < f ∨ f < 0
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
rw :
  ∀ (contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0) (f : ι → ℤ)
    (h₀ : LT.lt (α := ℤ) 0 (∑ j ∈ b.support, f j)) (hf₀ : Function.support f ⊆ (↑b.support : Set ι))
    (hf₁ : 0 < f ∨ f < 0)
    (hf₂ :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)),
    ¬f < 0
⊢ ¬f < 0

Tactic:
rw [isPos_iff, height_eq_sum hf₂] at h₀

Premises used: RootPairing.Base.height_eq_sum, 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 : P.IsCrystallographic
i : ι
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
h₀ : LT.lt (α := ℤ) 0 (∑ j ∈ b.support, f j)
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₁ : 0 < f ∨ f < 0
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
contrapose! : ∀ (h₀ : f < 0), LE.le (α := ℤ) (∑ j ∈ b.support, f j) 0
⊢ ¬f < 0

Tactic:
contrapose! h₀
-- 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 : P.IsCrystallographic
i : ι
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₁ : 0 < f ∨ f < 0
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
h₀ : f < 0
⊢ LE.le (α := ℤ) (∑ j ∈ b.support, f j) 0

Tactic:
Finset.sum_nonpos fun i _ ↦ h₀.le i

Premises used: LT.lt.le, Finset.sum_nonpos
-- 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 : P.IsCrystallographic
i : ι
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₁ : 0 < f ∨ f < 0
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
h₀ : f < 0
⊢ LE.le (α := ℤ) (∑ j ∈ b.support, f j) 0

Tactic:
exact Finset.sum_nonpos fun i _ ↦ h₀.le i

Premises used: LT.lt.le, Finset.sum_nonpos
-- 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 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₁ : 0 < f ∨ f < 0
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
⊢ 0 < f

Tactic:
replace hf₁ : 0 < f := by
    refine hf₁.resolve_right ?_
    rw [isPos_iff, height_eq_sum hf₂] at h₀
    contrapose! h₀
    exact Finset.sum_nonpos fun i _ ↦ h₀.le i
-- 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 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
⊢ P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i

Tactic:
have : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i :=
    algebraMap_injective ℤ R <| by
      simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]