mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ ↑(P.reflection i).dualMap ∘ₗ P.flip = P.flip ∘ₗ ↑(P.coreflection i)

Tactic:
by
  ext n m
  simp [map_sub, coreflection_apply, reflection_apply, mul_comm (P.toLinearMap m (P.coroot i))]

Goal state after:
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ (algebraMap A K) (num A x) / (algebraMap A K) ↑(den A x) = x

Tactic:
rw [← mk'_eq_div]

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ mk' K (num A x) (den A x) = x
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
⊢ ∀ (j : ℕ), j ≠ 0 → num A r ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j

Tactic:
intro j hj

Goal state after:
case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
⊢ ∀ (j : ℕ), j ≠ p.natDegree → ↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j

Tactic:
intro j hj

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ p.natDegree
⊢ ↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝ : Ring R
⊢ ∀ (α β : Type u_5) [inst : Fintype β] (e : α ≃ β),
    (∀ (M : α → Type u_6) [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : β → Type u_6) [inst_1 : (i : β) → AddCommGroup (M i)] [inst_2 : (i : β) → Module R (M i)],
        length R ((i : β) → M i) = ∑ i, length R (M i)

Tactic:
intro α

Goal state after:
case of_equiv
R : Type u_1
inst✝ : Ring R
α : Type u_5
⊢ ∀ (β : Type u_5) [inst : Fintype β] (e : α ≃ β),
    (∀ (M : α → Type u_6) [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : β → Type u_6) [inst_1 : (i : β) → AddCommGroup (M i)] [inst_2 : (i : β) → Module R (M i)],
        length R ((i : β) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝¹ : Ring R
α β : Type u_5
inst✝ : Fintype β
e : α ≃ β
⊢ (∀ (M : α → Type u_6) [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)],
      length R ((i : α) → M i) = ∑ i, length R (M i)) →
    ∀ (M : β → Type u_6) [inst : (i : β) → AddCommGroup (M i)] [inst_1 : (i : β) → Module R (M i)],
      length R ((i : β) → M i) = ∑ i, length R (M i)

Tactic:
IH

Goal state after:
case of_equiv
R : Type u_1
inst✝¹ : Ring R
α β : Type u_5
inst✝ : Fintype β
e : α ≃ β
IH :
  ∀ (M : α → Type u_6) [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)],
    length R ((i : α) → M i) = ∑ i, length R (M i)
⊢ ∀ (M : β → Type u_6) [inst : (i : β) → AddCommGroup (M i)] [inst_1 : (i : β) → Module R (M i)],
    length R ((i : β) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case h_option
R : Type u_1
inst✝¹ : Ring R
ι : Type u_5
inst✝ : Fintype ι
⊢ (∀ (M : ι → Type u_6) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
      length R ((i : ι) → M i) = ∑ i, length R (M i)) →
    ∀ (M : Option ι → Type u_6) [inst : (i : Option ι) → AddCommGroup (M i)] [inst_1 : (i : Option ι) → Module R (M i)],
      length R ((i : Option ι) → M i) = ∑ i, length R (M i)

Tactic:
IH

Goal state after:
case h_option
R : Type u_1
inst✝¹ : Ring R
ι : Type u_5
inst✝ : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
    length R ((i : ι) → M i) = ∑ i, length R (M i)
⊢ ∀ (M : Option ι → Type u_6) [inst : (i : Option ι) → AddCommGroup (M i)] [inst_1 : (i : Option ι) → Module R (M i)],
    length R ((i : Option ι) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case h_option
R : Type u_1
inst✝³ : Ring R
ι : Type u_5
inst✝² : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
    length R ((i : ι) → M i) = ∑ i, length R (M i)
M : Option ι → Type u_6
inst✝¹ : (i : Option ι) → AddCommGroup (M i)
inst✝ : (i : Option ι) → Module R (M i)
⊢ length R ((i : Option ι) → M i) = ∑ i, length R (M i)

Tactic:
(LinearEquiv.piOptionEquivProd _).length_eq,

Goal state after:
case h_option
R : Type u_1
inst✝³ : Ring R
ι : Type u_5
inst✝² : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
    length R ((i : ι) → M i) = ∑ i, length R (M i)
M : Option ι → Type u_6
inst✝¹ : (i : Option ι) → AddCommGroup (M i)
inst✝ : (i : Option ι) → Module R (M i)
⊢ length R (M none × ((i : ι) → M (some i))) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
⊢ v ↑u⁻¹ ≤ 1

Tactic:
rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
⊢ ∀ (a b : Ideal A), a ≤ b ∨ b ≤ a

Tactic:
intro α

Goal state after:
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α : Ideal A
⊢ ∀ (b : Ideal A), α ≤ b ∨ b ≤ α
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b : R
this : Ideal.span {a} ≤ Ideal.span {b} ∨ Ideal.span {b} ≤ Ideal.span {a}
⊢ a ∣ b ∨ b ∣ a

Tactic:
simp_rw [Ideal.span_singleton_le_span_singleton] at this

Goal state after:
R : Type u_1
inst✝ : CommRing R
H : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b : R
this : b ∣ a ∨ a ∣ b
⊢ a ∣ b ∨ b ∣ a
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Function.Surjective ⇑(mk I M)

Tactic:
intro x
  choose a ha using fun n ↦ Submodule.Quotient.mk_surjective _ (x.val n)
  refine ⟨⟨a, ?_⟩, ?_⟩
  · intro m n hmn
    rw [SModEq.def, ha m, ← mkQ_apply,
      ← factor_mk (Submodule.smul_mono_left (Ideal.pow_le_pow_right hmn)) (a n),
      mkQ_apply, ha n, x.property hmn]
  · ext n
    simp [ha n]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case h.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (n✝ + 1) - L ∈ I ^ (n✝ + 1)
⊢ x ^ (n✝ + 1) * y ^ (n✝ + 1) ∈ I ^ (n✝ + 1)

Tactic:
exact Ideal.mul_mem_right _ (I ^ _) (Ideal.pow_mem_pow hx _)

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ b ∈ fs, Associated x b) → ∃ n, Associated (x ^ n) fs.prod
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ b ∈ fa ::ₘ fs, Associated x b
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) fs.prod
⊢ Associated (x ^ 1 * x ^ n) (fa * fs.prod)

Tactic:
pow_one

Goal state after:
case h
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ b ∈ fs, Associated x b) → ∃ n, Associated (x ^ n) fs.prod
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ b ∈ fa ::ₘ fs, Associated x b
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) fs.prod
⊢ Associated (x * x ^ n) (fa * fs.prod)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
⊢ v₁ x = 1 ↔ v₂ x = 1

Tactic:
rw [← v₁.map_one, h.eq_iff, map_one]

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
hR : IsField R
this : Field R := hR.toField
⊢ finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Tactic:
simp only [finrank_cotangentSpace_eq_zero, zero_ne_one, false_iff]

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
hR : IsField R
this : Field R := hR.toField
⊢ ¬IsDiscreteValuationRing R
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
S✝ : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
S : Type u_6
inst✝² : CommRing S
inst✝¹ : Algebra S R
inst✝ : P.IsValuedIn S
⊢ P.flip.IsValuedIn S

Tactic:
by
  rw [isValuedIn_iff, forall_comm]
  exact P.exists_value

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
this : (algebraMap R S).IsIntegral
⊢ Module.Finite R S

Tactic:
have : Algebra.IsIntegral R S := Algebra.isIntegral_def.mpr this

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
this✝ : (algebraMap R S).IsIntegral
this : Algebra.IsIntegral R S
⊢ Module.Finite R S
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
⊢ h.orderMonoidIso = OrderMonoidIso.refl (ofClass v).ValueGroup₀

Tactic:
by
  ext x
  obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk
  · simp
  · simp [orderMonoidIso, valueGroup₀Fun_spec h]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ∀ x ∈ Finset.univ,
    (P.pairingIn S i x * P.pairingIn S i x) • P.coroot i = P.pairingIn S i x • P.pairing i x • P.coroot i

Tactic:
intro j hj

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
j : ι
hj : j ∈ Finset.univ
⊢ (P.pairingIn S i j * P.pairingIn S i j) • P.coroot i = P.pairingIn S i j • P.pairing i j • P.coroot i
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_2.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
h : ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j
i j : ι
hLin : ¬LinearIndependent R ![P.root i, P.root j]
h' : i ≠ j
⊢ P.root i = P.root j ∨ P.root i = -P.root j

Tactic:
exact Or.inr (h i j h' hLin)

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ (∀ (x : M₁ × M₂), 0 ≤ (Q₁.prod Q₂) x) ∧ (Q₁.prod Q₂).Anisotropic ↔
    ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic

Tactic:
nonneg_prod_iff

Goal state after:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x) ∧ (Q₁.prod Q₂).Anisotropic ↔
    ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
⊢ chainBotCoeff (⇑α) 0 + chainTopCoeff (⇑α) 0 = 2

Tactic:
chainTopCoeff_zero_right α hα,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
⊢ chainBotCoeff (⇑α) 0 + 1 = 2
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
hα : α.IsNonZero
h : ¬rootSpace H (2⁻¹ • ⇑α) = ⊥
W : Weight K (↥H) L := { toFun := 2⁻¹ • ⇑α, genWeightSpace_ne_bot' := h }
hW : 2 • ⇑W = ⇑α
e : ⇑W = 0
⊢ α.IsZero

Tactic:
apply_fun (2 • ·) at e; simpa [hW] using e

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case inr.inl
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑(↑n - ↑(chainTopCoeff (⇑α) β))
this : ↑n - ↑(chainTopCoeff (⇑α) β) ∈ Finset.Icc (-↑(chainBotCoeff (⇑α) 0)) ↑(chainTopCoeff (⇑α) 0)
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
chainTopCoeff_zero_right α hα,

Goal state after:
case inr.inl
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑(↑n - ↑(chainTopCoeff (⇑α) β))
this : ↑n - ↑(chainTopCoeff (⇑α) β) ∈ Finset.Icc (-↑(chainBotCoeff (⇑α) 0)) ↑1
⊢ k = -1 ∨ k = 0 ∨ k = 1
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ Function.Injective fun x ↦ Weight.toLinear K (↥H) L ↑x

Tactic:
intro α

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ β : Weight K (↥H) L
α : ↥LieSubalgebra.root
⊢ ∀ ⦃a₂ : ↥LieSubalgebra.root⦄,
    (fun x ↦ Weight.toLinear K (↥H) L ↑x) α = (fun x ↦ Weight.toLinear K (↥H) L ↑x) a₂ → α = a₂
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
⊢ 0 ∈ S

Tactic:
by simp [S_def]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i : ι
f : ι → ℤ
heq : P.root i = ∑ j ∈ b.support, f j • P.root j
⊢ ∀ j ∈ b.support, ⋯.choose j = f j

Tactic:
intro j hj

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i : ι
f : ι → ℤ
heq : P.root i = ∑ j ∈ b.support, f j • P.root j
j : ι
hj : j ∈ b.support
⊢ ⋯.choose j = f j
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this✝ : Fintype ι
B : P.InvariantForm
h : ∀ (i j : ι), (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)
i j : ι
this : P.pairing i j * (B.form (P.root j)) (P.root j) = P.pairing j i * (B.form (P.root j)) (P.root j)
⊢ P.pairing i j = P.pairing j i

Tactic:
mul_left_inj' (B.ne_zero j)

Goal state after:
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this✝ : Fintype ι
B : P.InvariantForm
h : ∀ (i j : ι), (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)
i j : ι
this : P.pairing i j = P.pairing j i
⊢ P.pairing i j = P.pairing j i
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i j k : ι
z : ℤ
hk : P.root k = P.root i + z • P.root j
⊢ b.height k = b.height i + z • b.height j

Tactic:
obtain ⟨f, -, -, hf⟩ := b.exists_root_eq_sum_int i
  obtain ⟨g, -, -, hg⟩ := b.exists_root_eq_sum_int j
  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]
  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]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : ∑ x, (u * ↑(a x) + v * ↑(b x)) • ↑x = ∑ x, Pi.single ri 1 x • ↑x
aux : P.root i = ∑ x, Pi.single ri 1 x • ↑x
⊢ LinearIndepOn ℚ id (⇑P.root '' s)

Tactic:
rw [← linearIndepOn_iff_image P.root.injective.injOn]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : ∑ x, (u * ↑(a x) + v * ↑(b x)) • ↑x = ∑ x, Pi.single ri 1 x • ↑x
aux : P.root i = ∑ x, Pi.single ri 1 x • ↑x
⊢ LinearIndepOn ℚ (⇑P.root) s