mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Algebra.adjoin K
      (↑{(algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (AdjoinRoot.root f.factor)}.toFinset ∪
        ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor).roots.toFinset) =
    ⊤

Tactic:
Multiset.toFinset_singleton,

Goal state after:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Algebra.adjoin K
      (↑{(algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (AdjoinRoot.root f.factor)} ∪
        ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor).roots.toFinset) =
    ⊤
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
| map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f

Tactic:
rw [Splits.eq_prod_roots (Monics.splits_finsetProd h)]

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
| C (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).leadingCoeff *
    (Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ eval₂ (algebraMap k (AlgebraicClosure k)) ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi)) ↑fi.fst = 0

Tactic:
← eval_map,

Goal state after:
case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi)) (map (algebraMap k (AlgebraicClosure k)) ↑fi.fst) = 0
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
h : (ad R L) x = 0
⊢ x = 0

Tactic:
← LieHom.mem_ker,

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
h : x ∈ (ad R L).ker
⊢ x = 0
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
⊢ IsCompl I (killingCompl K L I)

Tactic:
by
  suffices Disjoint I I.killingCompl by
    rwa [← LieSubmodule.isCompl_toSubmodule, I.toSubmodule_killingCompl,
      LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint (LieModule.traceForm_isSymm K L L).isRefl,
      ← I.toSubmodule_killingCompl, LieSubmodule.disjoint_toSubmodule]
  suffices IsLieAbelian (I ⊓ I.killingCompl : LieIdeal K L) by
    rw [disjoint_iff]
    exact IsKilling.ideal_eq_bot_of_isLieAbelian _
  suffices ∀ (x y z : L) (hx : x ∈ killingCompl K L I) (hy : y ∈ I),
      LieModule.traceForm K L L ⁅x, y⁆ z = 0 by
    rw [LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieSubmodule.lie_eq_bot_iff]
    rintro x ⟨-, hx⟩ y ⟨hy, -⟩
    exact (IsKilling.killingForm_nondegenerate K L).1 _ fun z ↦ this x y z hx hy
  intro x y z hx hy
  rw [LieModule.traceForm_apply_lie_apply K L L x y z, LieModule.traceForm_comm K L L]
  exact I.mem_killingCompl.mp hx _ <| lie_mem_left K L I y z hy

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ) ↑l
hm : m ∈ p
h₁ : MapsTo ⇑g ↑p ↑p
⊢ g m = μ • m

Tactic:
have h₂ : MapsTo (g - algebraMap R (End R M) μ) p p :=
    mapsTo_genEigenspace_of_comm (hfg.sub_right <| Algebra.commute_algebraMap_right μ f) μ l

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ) ↑l
hm : m ∈ p
h₁ : MapsTo ⇑g ↑p ↑p
h₂ : MapsTo ⇑(g - (algebraMap R (End R M)) μ) ↑p ↑p
⊢ g m = μ • m
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 χ ≠ ⊥
⊢ ∃ a b, 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0

Tactic:
obtain ⟨p, hp₀, q, hq₀, hp, hq⟩ := exists₂_genWeightSpace_smul_add_eq_bot M α χ hα

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 b, 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0
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
⊢ genWeightSpace M ((↑(chainBotCoeff α β) + 1) • -α + ⇑β) = ⊥

Tactic:
chainBotCoeff,

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
⊢ genWeightSpace M ((↑(chainTopCoeff (-α) β) + 1) • -α + ⇑β) = ⊥
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: case hn
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
n : ℕ
hn : n ≤ chainBotCoeff α β
⊢ -↑(chainBotCoeff α β) ≤ -↑n

Tactic:
lia

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

Goal state before:
pp: case hn'
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
n : ℕ
hn : n ≤ chainBotCoeff α β
⊢ -↑n ≤ ↑(chainTopCoeff α β)

Tactic:
lia

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

Goal state before:
pp: case succ
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 : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
hx : x ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
⊢ ((traceForm R L M) x) y = 0

Tactic:
refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx

Goal state after:
case succ.refine_1
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 : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
hx : x ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
⊢ ∀ x ∈ {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}, ((traceForm R L M) x) y = 0

case succ.refine_2
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 : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
hx : x ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
⊢ ((traceForm R L M) 0) y = 0

case succ.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 : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
hx : x ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
z w : L
x✝¹ : z ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
x✝ : w ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
hz : ((traceForm R L M) z) y = 0
hw : ((traceForm R L M) w) y = 0
⊢ ((traceForm R L M) (z + w)) y = 0

case succ.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 : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
hx : x ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
t : R
z : L
x✝ : z ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
hz : ((traceForm R L M) z) y = 0
⊢ ((traceForm R L M) (t • z)) y = 0
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case hx
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
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ⁅e, f⁆ ∈ H

Tactic:
simpa using mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α (-α) heα hfα

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

Goal state before:
pp: K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
⊢ ((traceForm K L M) x) y = ∑ χ, finrank K ↥(genWeightSpace M ⇑χ) • (χ x * χ y)

Tactic:
classical
  have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
    (LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpace' K L M)
    (LieSubmodule.iSup_toSubmodule_eq_top.mpr <| iSup_genWeightSpace_eq_top' K L M)
  simp_rw [traceForm_apply_apply, LinearMap.trace_eq_sum_trace_restrict hds hxy,
    ← traceForm_genWeightSpace_eq K L M _ x y]
  rfl

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
z : M
t : R
ht : t = f y * g x - 2
m : ℕ
S_eval_t_sub_two :
  ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    Polynomial.eval t (S R k) ^ 2 + Polynomial.eval t (S R (k + 1)) ^ 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1
k : ℤ := ↑m / 2
ih :
  ((reflection hf * reflection hg) ^ m) z =
    z +
        (Polynomial.eval t (S R ((↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) * (Polynomial.eval t (S R k) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
e : ℤ := ↑m % 2
⊢ e = 0 ∨ e = 1

Tactic:
lia

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
⊢ iSup ![H.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤

Tactic:
by
  suffices H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper = ⊤ by simpa
  refine eq_top_iff.mpr fun x hx ↦ ?_
  replace hx : x ∈ lieSpan R L (range b.e ∪ range b.f) := by simp [b.span_ef]
  induction hx using lieSpan_induction with
  | mem u hu =>
    rcases (mem_union _ _ _).mpr hu with hu | hu
    · exact LieSubmodule.mem_sup_right <| subset_lieSpan hu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu
  | zero => simp
  | add u v _ _ hu hv => exact add_mem hu hv
  | smul t u _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    obtain ⟨yc, hyc, yl, hyl, yu, hyu, rfl⟩ :
        ∃ᵉ (yc ∈ H) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
          yc + yl + yu = u := by simpa [LieSubmodule.mem_sup] using! hu
    obtain ⟨zc, hzc, zl, hzl, zu, hzu, rfl⟩ :
        ∃ᵉ (zc ∈ H) (zl ∈ lieSpan R L (range b.f)) (zu ∈ lieSpan R L (range b.e)),
          zc + zl + zu = v := by simpa [LieSubmodule.mem_sup] using! hv
    simp only [lie_add, add_lie, ← add_assoc]
    repeat apply add_mem
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_left <| lie_mem _ hyc hzc
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨zc, hzc⟩) hyl
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨zc, hzc⟩) hyu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨yc, hyc⟩) hzl
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| lie_mem _ hyl hzl
    · exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hyu hzl
    · exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hzu
    · rw [← lie_skew, neg_mem_iff]
      exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hzu hyl
    · exact LieSubmodule.mem_sup_right <| lie_mem _ hyu hzu

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 0 (T R (↑n + 1)) = ↑(if Even (↑n + 1) then ↑((↑n + 1) / 2).negOnePow else 0)
ih2 : eval 0 (T R ↑n) = ↑(if Even ↑n then ↑(↑n / 2).negOnePow else 0)
⊢ (↑n + 2) / 2 = ↑n / 2 + 1

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 0 (T R (-↑n)) = ↑(if Even (-↑n) then ↑(-↑n / 2).negOnePow else 0)
ih2 : eval 0 (T R (-↑n + 1)) = ↑(if Even (-↑n + 1) then ↑((-↑n + 1) / 2).negOnePow else 0)
⊢ (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval 0 (T R n) = ↑(if Even n then ↑(n / 2).negOnePow else 0)

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have : ((n : ℤ) + 2) / 2 = (n : ℤ) / 2 + 1 := by lia
    by_cases Even n <;> simp_all [Int.negOnePow_add]
  | neg_add_one n ih1 ih2 =>
    have : (-(n : ℤ) + 1) / 2 = (-(n : ℤ) - 1) / 2 + 1 := by lia
    by_cases Even n <;> simp_all [T_sub_one, ← Int.not_even_iff_odd, Int.negOnePow_add]

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
hyp : coroot α = coroot β
⊢ α = β

Tactic:
if hα : α.IsZero then
    have hβ : β.IsZero := by
      rw [← coroot_eq_zero_iff] at hα ⊢
      rwa [← hyp]
    ext
    simp [hα.eq, hβ.eq]
  else
    have hβ : β.IsNonZero := by
      contrapose hα
      simp only [← coroot_eq_zero_iff] at hα ⊢
      rwa [hyp]
    have : α.ker = β.ker := by
      rw [← orthogonal_span_coroot_eq_ker α, hyp, orthogonal_span_coroot_eq_ker]
    suffices (α : H →ₗ[K] K) = β by ext x; simpa using LinearMap.congr_fun this x
    apply Module.Dual.eq_of_ker_eq_of_apply_eq (coroot α) this
    · rw [Weight.toLinear_apply, root_apply_coroot hα, hyp, Weight.toLinear_apply,
        root_apply_coroot hβ]
    · simp [root_apply_coroot hα]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
this : U R 2 = 2 * X * (2 * X) - 1
⊢ U R 2 = 4 * X ^ 2 - 1

Tactic:
linear_combination this

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 0 (U R (↑n + 1)) = ↑(if Even (↑n + 1) then ↑((↑n + 1) / 2).negOnePow else 0)
ih2 : eval 0 (U R ↑n) = ↑(if Even ↑n then ↑(↑n / 2).negOnePow else 0)
⊢ (↑n + 2) / 2 = ↑n / 2 + 1

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 0 (U R (-↑n)) = ↑(if Even (-↑n) then ↑(-↑n / 2).negOnePow else 0)
ih2 : eval 0 (U R (-↑n + 1)) = ↑(if Even (-↑n + 1) then ↑((-↑n + 1) / 2).negOnePow else 0)
⊢ (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1

Tactic:
lia

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
this : ¬1 < finrank K ↥(rootSpace H ⇑α)
h₀ : finrank K ↥(rootSpace H ⇑α) ≠ 0
⊢ finrank K ↥(rootSpace H ⇑α) = 1

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n

Tactic:
have h₁ := U_eq_X_mul_U_add_T R n
  have h₂ := U_eq_X_mul_U_add_T R (n + 1)
  have h₃ := U_add_two R n
  linear_combination (norm := ring_nf) h₃ - h₂ + (X : R[X]) * h₁

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
this : S R 2 = X * X - 1
⊢ S R 2 = X ^ 2 - 1

Tactic:
linear_combination this

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
z : M
t : R
ht : t = f y * g x - 2
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
ht' : t = g x * f y - 2
a b : ℤ
hab : a + b = -3
⊢ a / 2 = -(b / 2) - 2

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)

Tactic:
by
  have := congr_arg (·.comp (Polynomial.C ⅟2 * X)) (S_comp_two_mul_X R n)
  simp_rw [comp_assoc, mul_comp, ofNat_comp, X_comp, ← mul_assoc, ← C_eq_natCast, ← C_mul,
    Nat.cast_ofNat, mul_invOf_self', map_one, one_mul, comp_X] at this
  assumption

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
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
n : ι → ℕ
hn : n ≠ 0
hg : -⇑(∑ i, n i • b.baseSupp i) ∈ sU
contra : ∑ i, n i • b.baseSupp i = 0
⊢ ∑ i, (Nat.cast ∘ n) i • b.baseSupp i = 0

Tactic:
simpa [Nat.cast_smul_eq_nsmul]

Goal state after: