-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma exists₂_genWeightSpace_smul_add_eq_bot :
    ∃ᵉ (p < (0 : ℤ)) (q > (0 : ℤ)),
      genWeightSpace M (p • χ₁ + χ₂) = ⊥ ∧
      genWeightSpace M (q • χ₁ + χ₂) = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
⊢ ∃ p < 0, ∃ q > 0, genWeightSpace M (p • χ₁ + χ₂) = ⊥ ∧ genWeightSpace M (q • χ₁ + χ₂) = ⊥

Tactic:
obtain ⟨q, hq₀, hq⟩ := exists_genWeightSpace_smul_add_eq_bot M χ₁ χ₂ hχ₁

Result:
case intro.intro
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
⊢ ∃ p < 0, ∃ q > 0, genWeightSpace M (p • χ₁ + χ₂) = ⊥ ∧ genWeightSpace M (q • χ₁ + χ₂) = ⊥

Proof state:
case intro.intro.intro.intro.refine_1
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ genWeightSpace M (-↑p • χ₁ + χ₂) = ⊥

Tactic:
rw [neg_smul, ← smul_neg, natCast_zsmul]

Result:
case intro.intro.intro.intro.refine_1
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ genWeightSpace M (p • -χ₁ + χ₂) = ⊥

Proof state:
case intro.intro
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
⊢ ∃ p < 0, ∃ q > 0, genWeightSpace M (p • χ₁ + χ₂) = ⊥ ∧ genWeightSpace M (q • χ₁ + χ₂) = ⊥

Tactic:
obtain ⟨p, hp₀, hp⟩ := exists_genWeightSpace_smul_add_eq_bot M (-χ₁) χ₂ (neg_ne_zero.mpr hχ₁)

Result:
case intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ ∃ p < 0, ∃ q > 0, genWeightSpace M (p • χ₁ + χ₂) = ⊥ ∧ genWeightSpace M (q • χ₁ + χ₂) = ⊥

Proof state:
case intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ ∃ p < 0, ∃ q > 0, genWeightSpace M (p • χ₁ + χ₂) = ⊥ ∧ genWeightSpace M (q • χ₁ + χ₂) = ⊥

Tactic:
refine ⟨-(p : ℤ), by simpa, q, by simpa, ?_, ?_⟩

Result:
case intro.intro.intro.intro.refine_1
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ genWeightSpace M (-↑p • χ₁ + χ₂) = ⊥

case intro.intro.intro.intro.refine_2
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ genWeightSpace M (↑q • χ₁ + χ₂) = ⊥

Proof state:
case intro.intro.intro.intro.refine_2
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ genWeightSpace M (q • χ₁ + χ₂) = ⊥

Tactic:
exact hq

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ genWeightSpace M (↑q • χ₁ + χ₂) = ⊥

Tactic:
rw [natCast_zsmul]

Result:
case intro.intro.intro.intro.refine_2
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ genWeightSpace M (q • χ₁ + χ₂) = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ -↑p < 0

Tactic:
simpa

Result:
no goals