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
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
let S := {I : LieIdeal R L | IsAtom I}

Goal state after:
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}
⊢ ∃ t ⊆ s, I = t.sup id
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: case fst
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x✝ : m.ToType
⊢ ((m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype fun x ↦ x ∈ m.toEnumFinset)) x✝).1 = (m.coeEmbedding x✝).1

pp: case snd
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x✝ : m.ToType
⊢ ((m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype fun x ↦ x ∈ m.toEnumFinset)) x✝).2 = (m.coeEmbedding x✝).2

Tactic:
<;>

Goal state after:
case fst
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x✝ : m.ToType
⊢ ((m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype fun x ↦ x ∈ m.toEnumFinset)) x✝).1 = (m.coeEmbedding x✝).1

case snd
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x✝ : m.ToType
⊢ ((m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype fun x ↦ x ∈ m.toEnumFinset)) x✝).2 = (m.coeEmbedding x✝).2
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: case isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
f : α → β
l : List α
a : α
s : List α
x✝ : { v // ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst }
v : ToType ⟦s⟧ ≃ (map f ⟦s⟧).ToType
hv : ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst
x : ToType ⟦a :: s⟧
h✝ : x.fst = a ∧ ↑x.snd = count a ⟦s⟧
⊢ ((cast ⋯).symm
        ((Option.map (⇑v) none).elim ⟨f a, ⟨count (f a) (map f ⟦s⟧), ⋯⟩⟩ fun x ↦ ⟨x.fst, Fin.castLE ⋯ x.snd⟩)).fst =
    f x.fst

pp: case isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
f : α → β
l : List α
a : α
s : List α
x✝ : { v // ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst }
v : ToType ⟦s⟧ ≃ (map f ⟦s⟧).ToType
hv : ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst
x : ToType ⟦a :: s⟧
h✝ : ¬(x.fst = a ∧ ↑x.snd = count a ⟦s⟧)
⊢ ((cast ⋯).symm
        ((Option.map (⇑v) (some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩)).elim ⟨f a, ⟨count (f a) (map f ⟦s⟧), ⋯⟩⟩ fun x ↦
          ⟨x.fst, Fin.castLE ⋯ x.snd⟩)).fst =
    f x.fst

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
f : α → β
l : List α
a : α
s : List α
x✝ : { v // ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst }
v : ToType ⟦s⟧ ≃ (map f ⟦s⟧).ToType
hv : ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst
x : ToType ⟦a :: s⟧
h✝ : x.fst = a ∧ ↑x.snd = count a ⟦s⟧
⊢ ((cast ⋯).symm
        ((Option.map (⇑v) none).elim ⟨f a, ⟨count (f a) (map f ⟦s⟧), ⋯⟩⟩ fun x ↦ ⟨x.fst, Fin.castLE ⋯ x.snd⟩)).fst =
    f x.fst

case isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
f : α → β
l : List α
a : α
s : List α
x✝ : { v // ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst }
v : ToType ⟦s⟧ ≃ (map f ⟦s⟧).ToType
hv : ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst
x : ToType ⟦a :: s⟧
h✝ : ¬(x.fst = a ∧ ↑x.snd = count a ⟦s⟧)
⊢ ((cast ⋯).symm
        ((Option.map (⇑v) (some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩)).elim ⟨f a, ⟨count (f a) (map f ⟦s⟧), ⋯⟩⟩ fun x ↦
          ⟨x.fst, Fin.castLE ⋯ x.snd⟩)).fst =
    f x.fst
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: case refine_2
K : Type v
inst✝ : Field K
f g : K[X]
h : ∀ {A : Type v} [inst : CommRing A] [IsDomain A] [inst_2 : Algebra K A] (a : A), (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0
x : K[X]
hx : x ∈ nonunits K[X]
x✝ : x ≠ 0
⊢ x ∣ f → ¬x ∣ g

Tactic:
· rintro ⟨_, rfl⟩ ⟨_, rfl⟩
    replace h := not_and_or.mpr <| h <| AdjoinRoot.root x.factor
    simp only [AdjoinRoot.aeval_eq, AdjoinRoot.mk_eq_zero,
      dvd_mul_of_dvd_left <| factor_dvd_of_not_isUnit hx, true_and, not_true] at h

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

Goal state before:
pp: case lie.hx.a.a
ι : 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
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
aux : yc + yl + yu = ⁅v, z⁆
⊢ ⁅yc, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hu

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 α β
⊢ -↑(chainBotCoeff α β) ≤ -↑n

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:
<;>

Goal state after:
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

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 α β)
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 :
  (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
        (trace R ↥(genWeightSpace M χ)) ((χ x • LinearMap.id) ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
      ((trace R ↥(genWeightSpace M χ)) (χ y • (toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ LinearMap.id) -
        (trace R ↥(genWeightSpace M χ)) ((χ x • LinearMap.id) ∘ₗ (χ y • LinearMap.id))) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)

Tactic:
LinearMap.smul_comp,

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 :
  (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
        (trace R ↥(genWeightSpace M χ)) (χ x • LinearMap.id ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
      ((trace R ↥(genWeightSpace M χ)) (χ y • (toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ LinearMap.id) -
        (trace R ↥(genWeightSpace M χ)) ((χ x • LinearMap.id) ∘ₗ (χ y • LinearMap.id))) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)
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 :
  (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
        χ x • finrank R ↥(genWeightSpace M χ) • χ y -
      (χ y • finrank R ↥(genWeightSpace M χ) • χ x -
        (trace R ↥(genWeightSpace M χ)) (χ y • (χ x • LinearMap.id) ∘ₗ LinearMap.id)) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)

Tactic:
LinearMap.smul_comp,

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 :
  (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
        χ x • finrank R ↥(genWeightSpace M χ) • χ y -
      (χ y • finrank R ↥(genWeightSpace M χ) • χ x -
        (trace R ↥(genWeightSpace M χ)) (χ y • χ x • LinearMap.id ∘ₗ LinearMap.id)) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)
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
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ IsReflexive R N

Tactic:
constructor
  rw [← trans_dualMap_symm_flip e]
  exact LinearEquiv.bijective _

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
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R N
⊢ map (↑e.flip.symm) p.dualAnnihilator = (map (↑e) p).dualCoannihilator

Tactic:
by
  have : IsReflexive R N := e.isReflexive_of_equiv_dual_of_isReflexive
  rw [← dualCoannihilator_map_linearEquiv_flip, ← LinearEquiv.coe_toLinearMap_flip,
    LinearEquiv.flip_flip]

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✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsTorsionFree R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
hfin : {χ | ↑(genWeightSpaceOf M χ z) ≠ ⊥}.Finite
⊢ ((traceForm R L M) x) y = ((∑ χ ∈ ⋯.toFinset, traceForm R L ↥(genWeightSpaceOf M χ z)) x) y

Tactic:
have h := LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpaceOf R L M z
  have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top h <| by
    simp [← LieSubmodule.iSup_toSubmodule]
  simp only [LinearMap.coe_sum, Finset.sum_apply, traceForm_apply_apply,
    LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
  exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl)

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✝³ : LieRing.IsNilpotent L
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : ∀ (x : L), ⁅x, z⁆ = 0
y u v : A ⊗[R] L
hu : ⁅u, 1 ⊗ₜ[R] z⁆ = 0
hv : ⁅v, 1 ⊗ₜ[R] z⁆ = 0
⊢ ⁅u + v, 1 ⊗ₜ[R] z⁆ = 0

Tactic:
simp [A, hu, hv]

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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : ⟨x, hx⟩ ∈ ↑(corootSpace ⇑α)
e : L
heα : e ∈ rootSpace H ⇑α
f : L
hfα : f ∈ rootSpace H (-⇑α)
⊢ ⁅e, f⁆ ∈ ↑(K ∙ ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))

Tactic:
lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα,

Goal state after:
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : ⟨x, hx⟩ ∈ ↑(corootSpace ⇑α)
e : L
heα : e ∈ rootSpace H ⇑α
f : L
hfα : f ∈ rootSpace H (-⇑α)
⊢ ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) ∈
    ↑(K ∙ ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))
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 : M
f : Dual R M
h : f x = 2
p : Submodule R M
hx : x ∈ p
⊢ p ∈ End.invtSubmodule ↑(reflection h)

Tactic:
suffices ∀ y ∈ p, reflection h y ∈ p from
    (End.mem_invtSubmodule _).mpr fun y hy ↦ by simpa using this y hy
  intro y hy
  simpa only [reflection_apply, p.sub_mem_iff_right hy] using p.smul_mem (f y) hx

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α : α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) = 0
this :
  (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ∈
    Weight.ker ⊓ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
⊢ α.IsZero

Tactic:
by
    rw [(disjoint_ker_weight_corootSpace α).eq_bot] at this
    simpa using this

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = ↑n.natAbs
⊢ T R ↑n.natAbs = T R n

pp: case inr
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = -↑n.natAbs
⊢ T R ↑n.natAbs = T R n

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = ↑n.natAbs
⊢ T R ↑n.natAbs = T R n

case inr
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = -↑n.natAbs
⊢ T R ↑n.natAbs = T R n
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case pos
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)
this : (↑n + 2) / 2 = ↑n / 2 + 1
h✝ : Even n
⊢ eval 0 (T R (↑n + 2)) = ↑(if Even (↑n + 2) then ↑((↑n + 2) / 2).negOnePow else 0)

pp: case neg
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)
this : (↑n + 2) / 2 = ↑n / 2 + 1
h✝ : ¬Even n
⊢ eval 0 (T R (↑n + 2)) = ↑(if Even (↑n + 2) then ↑((↑n + 2) / 2).negOnePow else 0)

Tactic:
<;>

Goal state after:
case pos
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)
this : (↑n + 2) / 2 = ↑n / 2 + 1
h✝ : Even n
⊢ eval 0 (T R (↑n + 2)) = ↑(if Even (↑n + 2) then ↑((↑n + 2) / 2).negOnePow else 0)

case neg
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)
this : (↑n + 2) / 2 = ↑n / 2 + 1
h✝ : ¬Even n
⊢ eval 0 (T R (↑n + 2)) = ↑(if Even (↑n + 2) then ↑((↑n + 2) / 2).negOnePow else 0)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case pos
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)
this : (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1
h✝ : Even n
⊢ eval 0 (T R (-↑n - 1)) = ↑(if Even (-↑n - 1) then ↑((-↑n - 1) / 2).negOnePow else 0)

pp: case neg
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)
this : (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1
h✝ : ¬Even n
⊢ eval 0 (T R (-↑n - 1)) = ↑(if Even (-↑n - 1) then ↑((-↑n - 1) / 2).negOnePow else 0)

Tactic:
<;>

Goal state after:
case pos
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)
this : (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1
h✝ : Even n
⊢ eval 0 (T R (-↑n - 1)) = ↑(if Even (-↑n - 1) then ↑((-↑n - 1) / 2).negOnePow else 0)

case neg
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)
this : (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1
h✝ : ¬Even n
⊢ eval 0 (T R (-↑n - 1)) = ↑(if Even (-↑n - 1) then ↑((-↑n - 1) / 2).negOnePow else 0)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval (-1) (U R n) = ↑↑n.negOnePow * (↑n + 1)

Tactic:
by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp; norm_num
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, neg_mul, ih2, Int.cast_ofNat, Int.negOnePow_add,
      Int.negOnePow_def 2]
    norm_cast
    norm_num
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.cast_neg, Int.cast_natCast, Int.negOnePow_neg, neg_mul, ih2, Int.cast_add, Int.cast_one,
      Int.cast_sub, sub_add_cancel, Int.negOnePow_sub, Int.negOnePow_add]
    norm_cast
    norm_num
    ring

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

Goal state before:
pp: case pos
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)
this : (↑n + 2) / 2 = ↑n / 2 + 1
h✝ : Even n
⊢ eval 0 (U R (↑n + 2)) = ↑(if Even (↑n + 2) then ↑((↑n + 2) / 2).negOnePow else 0)

pp: case neg
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)
this : (↑n + 2) / 2 = ↑n / 2 + 1
h✝ : ¬Even n
⊢ eval 0 (U R (↑n + 2)) = ↑(if Even (↑n + 2) then ↑((↑n + 2) / 2).negOnePow else 0)

Tactic:
<;>

Goal state after:
case pos
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)
this : (↑n + 2) / 2 = ↑n / 2 + 1
h✝ : Even n
⊢ eval 0 (U R (↑n + 2)) = ↑(if Even (↑n + 2) then ↑((↑n + 2) / 2).negOnePow else 0)

case neg
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)
this : (↑n + 2) / 2 = ↑n / 2 + 1
h✝ : ¬Even n
⊢ eval 0 (U R (↑n + 2)) = ↑(if Even (↑n + 2) then ↑((↑n + 2) / 2).negOnePow else 0)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case pos
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)
this : (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1
h✝ : Even n
⊢ eval 0 (U R (-↑n - 1)) = ↑(if Even (-↑n - 1) then ↑((-↑n - 1) / 2).negOnePow else 0)

pp: case neg
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)
this : (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1
h✝ : ¬Even n
⊢ eval 0 (U R (-↑n - 1)) = ↑(if Even (-↑n - 1) then ↑((-↑n - 1) / 2).negOnePow else 0)

Tactic:
<;>

Goal state after:
case pos
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)
this : (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1
h✝ : Even n
⊢ eval 0 (U R (-↑n - 1)) = ↑(if Even (-↑n - 1) then ↑((-↑n - 1) / 2).negOnePow else 0)

case neg
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)
this : (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1
h✝ : ¬Even n
⊢ eval 0 (U R (-↑n - 1)) = ↑(if Even (-↑n - 1) then ↑((-↑n - 1) / 2).negOnePow else 0)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑(m + 1 + 1) ≠ -1
⊢ (U R ↑m).degree = ↑((-↑(m + 1 + 1) + 1).natAbs - 1)

Tactic:
· rw [degree_U_natCast R m]; norm_cast

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

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (2 * X * U R (↑n + 1)).degree

Tactic:
· norm_cast
      rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X,
        degree_U_natCast R n, degree_U_natCast R (n + 1)]
      norm_cast; omega

Goal state after: