mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
⊢ ∃ J ∈ s, ¬J ≤ I

Tactic:
by_contra! H
    exact hI.ne (le_antisymm hI.le (s.sup_le H))

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h : ¬(x.fst = v ∧ ↑x.snd = count v m)
hv : x.fst = v
⊢ ↑x.snd < count x.fst m

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h : ¬(x.fst = v ∧ ↑x.snd = count v m)
hv : ¬x.fst = v
⊢ ↑x.snd < count x.fst m

Tactic:
· simp only [hv, true_and] at h ⊢
      apply lt_of_le_of_ne (Nat.le_of_lt_add_one _) h
      convert! x.2.2 using 1
      simp [hv]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h : ¬(x.fst = v ∧ ↑x.snd = count v m)
hv : ¬x.fst = v
⊢ ↑x.snd < count x.fst m
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
hf : f ∈ s
⊢ (∏ x ∈ s, map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑x).Splits

Tactic:
by simpa [Polynomial.map_prod] using SplittingField.splits (∏ f ∈ s, f.1)

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : AddCommMonoid M₂
inst✝¹ : Algebra R A
inst✝ : Module R M₂
⊢ BilinForm.baseChange A 0 = 0

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: case mpr
K : Type u_3
V : Type u_4
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
⊢ (∀ (μ : K), f.HasEigenvalue μ → μ = 0) → f = 0

Tactic:
intro h
    suffices f.eigenspace 0 = ⊤ by rwa [eigenspace_zero, LinearMap.ker_eq_top] at this
    rw [← hf.iSup_eigenspace_eq_top]
    refine le_antisymm (le_iSup _ 0) (iSup_le fun μ ↦ ?_)
    rcases eq_or_ne μ 0 with rfl | hμ
    · exact le_refl _
    · have : f.eigenspace μ = ⊥ := not_not.mp (hasEigenvalue_iff.not.mp fun he ↦ hμ (h μ he))
      simp [this]

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

Goal state before:
pp: 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
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k ↦ ↑(genWeightSpace M (k • α + χ))
h₁ : iSupIndep fun i ↦ N ↑i
h₂ : ∀ (i : ℤ), MapsTo ⇑((toEnd R (↥H) M) x) ↑(N i) ↑(N i)
h₃ : ↑(genWeightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, N i
⊢ (a • α + ↑b • χ) x = 0

Tactic:
← trace_toEnd_genWeightSpaceChain_eq_zero M α χ p q hp hq hx,

Goal state after:
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
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k ↦ ↑(genWeightSpace M (k • α + χ))
h₁ : iSupIndep fun i ↦ N ↑i
h₂ : ∀ (i : ℤ), MapsTo ⇑((toEnd R (↥H) M) x) ↑(N i) ↑(N i)
h₃ : ↑(genWeightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, N i
⊢ (a • α + ↑b • χ) x =
    (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) x)
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: 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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ Nat.find ⋯ ≠ 0

Tactic:
intro e

Goal state after:
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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
e : Nat.find ⋯ = 0
⊢ False
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : IsReduced R
inst✝ : IsNilpotent L M
⊢ traceForm R L M = 0

Tactic:
ext x y
  simp only [traceForm_apply_apply, LinearMap.zero_apply, ← isNilpotent_iff_eq_zero]
  apply LinearMap.isNilpotent_trace_of_isNilpotent
  exact isNilpotent_toEnd_of_isNilpotent₂ R L M x y

Goal state after:
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this : traceForm R L ↥(shiftedGenWeightSpace R L M χ) = 0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)

Tactic:
replace this := LinearMap.congr_fun (LinearMap.congr_fun this x) y

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this : ((traceForm R L ↥(shiftedGenWeightSpace R L M χ)) x) y = (0 x) y
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: 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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ chainTop (-α) β = chainBot α β

Tactic:
ext; simp

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

Goal state before:
pp: 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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ chainBot (-α) β = chainTop α β

Tactic:
ext; simp

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

Goal state before:
pp: 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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
β : Weight R L M
⊢ chainTop 0 β = β

Tactic:
ext; simp

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

Goal state before:
pp: 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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
β : Weight R L M
⊢ chainBot 0 β = β

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] Dual R M
p : Submodule R M
⊢ (map (↑e).flip p).dualCoannihilator = map (↑e.symm) p.dualAnnihilator

Tactic:
ext; simp

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

Goal state before:
pp: case neg
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ genWeightSpace L (-⇑α) ≠ ⊥

Tactic:
intro e

Goal state after:
case neg
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ α : Weight K (↥H) L
hα : ¬α.IsZero
e : genWeightSpace L (-⇑α) = ⊥
⊢ False
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ α : Weight K (↥H) L
⊢ { toFun := -⇑{ toFun := -⇑α, genWeightSpace_ne_bot' := ⋯ }, genWeightSpace_ne_bot' := ⋯ } = α

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case refine_3
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
u v : L
x✝¹ : u ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
x✝ : v ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
hu : (trace R M) (φ u) = 0
hv : (trace R M) (φ v) = 0
⊢ (trace R M) (φ (u + v)) = 0

pp: case refine_4
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
t : R
u : L
x✝ : u ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
hu : (trace R M) (φ u) = 0
⊢ (trace R M) (φ (t • u)) = 0

Tactic:
· simp [hu, hv]

Goal state after:
case refine_4
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
t : R
u : L
x✝ : u ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
hu : (trace R M) (φ u) = 0
⊢ (trace R M) (φ (t • u)) = 0
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
⊢ corootSpace 0 = ⊥

Tactic:
by
  refine eq_bot_iff.mpr fun x hx ↦ ?_
  suffices {x | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} = {0} by simpa [mem_corootSpace, this] using hx
  refine eq_singleton_iff_unique_mem.mpr ⟨⟨0, H.zero_mem, 0, H.zero_mem, zero_lie 0⟩, ?_⟩
  rintro - ⟨y, hy, z, hz, rfl⟩
  suffices ⁅(⟨y, hy⟩ : H), (⟨z, hz⟩ : H)⁆ = 0 by
    simpa only [Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero] using this
  simp [trivial_lie_zero]

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e
⊢ ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))

Tactic:
set α' := (cartanEquivDual H).symm α
  rw [← sub_eq_zero, ← Submodule.mem_bot (R := K), ← ker_killingForm_eq_bot]
  apply mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg (α := (0 : H → K))
  · simp only [rootSpace_zero_eq, LieSubalgebra.mem_toLieSubmodule]
    refine sub_mem ?_ (H.smul_mem _ α'.property)
    simpa using mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α (-α) heα hfα
  · intro z hz
    replace hz : z ∈ H := by simpa using hz
    have he : ⁅z, e⁆ = α ⟨z, hz⟩ • e := aux ⟨z, hz⟩
    have hαz : killingForm K L α' (⟨z, hz⟩ : H) = α ⟨z, hz⟩ :=
      LinearMap.BilinForm.apply_toDual_symm_apply (hB := traceForm_cartan_nondegenerate K L H) _ _
    simp [traceForm_comm K L L ⁅e, f⁆, ← traceForm_apply_lie_apply, he, mul_comm _ (α ⟨z, hz⟩), hαz]

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
n : ↑{n | n ≠ 0}
⊢ ∑ i, ↑n i • ⇑(b.baseSupp i) = ⇑(∑ i, ↑n i • b.baseSupp i)

Tactic:
ext; simp

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
⊢ ∃ c, he.choose = c • e

Tactic:
obtain ⟨c, hc⟩ := (finrank_eq_one_iff_of_nonzero' ⟨e, hte⟩ (by simpa using t.e_ne_zero)).mp
      (finrank_rootSpace_eq_one α hα) ⟨_, he.choose_spec.choose_spec.2.1⟩
    exact ⟨c, by simpa using hc.symm⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ S R (-1) = 0

Tactic:
simpa using S_sub_one R 0

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (S R (-↑n)) = ↑(-↑n) + 1
ih2 : eval 2 (S R (-↑n + 1)) = ↑(-↑n + 1) + 1
⊢ eval 2 (S R (-↑n - 1)) = ↑(-↑n - 1) + 1

Tactic:
simp only [S_sub_one, eval_sub, eval_mul, eval_X,
      ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
      sub_add_cancel]

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (S R (-↑n)) = ↑(-↑n) + 1
ih2 : eval 2 (S R (-↑n + 1)) = ↑(-↑n + 1) + 1
⊢ 2 * (-↑n + 1) - (-↑n + 1 + 1) = -↑n
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.reflectionPerm i))^[2] = id

Tactic:
ext; simp

Goal state after:
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 j : ι
x : M
⊢ x -
      ((P.toLinearMap x) (P.coroot i) - P.pairing j i * (P.toLinearMap x) (P.coroot j)) •
        (P.root i - P.pairing i j • P.root j) =
    x - (P.toLinearMap x) (P.coroot j) • P.root j -
        ((P.toLinearMap x) (P.coroot i) - (P.toLinearMap x) (P.coroot j) * P.pairing j i) • P.root i -
      ((P.toLinearMap x) (P.coroot j) - (P.toLinearMap x) (P.coroot j) * 2 -
          ((P.toLinearMap x) (P.coroot i) - (P.toLinearMap x) (P.coroot j) * P.pairing j i) * P.pairing i j) •
        P.root j

Tactic:
module

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ U R (Int.subNatNat n 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Ico 0 n)

Tactic:
convert! U_mem_span_T R (n - 1) using 2 <;> grind

Goal state after:
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✝ j i : ι
⊢ P.root i + 2 • (P.root i - 2 • P.root i) - (2 • P.root i + 2 • 2 • (P.root i - 2 • P.root i)) = P.root i

Tactic:
module

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℤ
t : R
ht : t = f y * g x - 2
⊢ (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • (x - g x • y) +
      (Polynomial.eval t (S R (m - 1)) * -g x) • (y - 2 • y) =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x + (Polynomial.eval t (S R m) * -g x) • y

Tactic:
module

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case e'_5
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
hUV : Disjoint sU sV
key : iSupIndep fun χ ↦ LieModule.genWeightSpace L χ
⊢ U ⊔ V = ⨆ i ∈ sU ∪ sV, LieModule.genWeightSpace L i

Tactic:
iSup_union,

Goal state after:
case e'_5
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
hUV : Disjoint sU sV
key : iSupIndep fun χ ↦ LieModule.genWeightSpace L χ
⊢ U ⊔ V = (⨆ x ∈ sU, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ sV, LieModule.genWeightSpace L x