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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
y z : L
hy : y ∈ (↑H.toLieSubmodule.normalizer).carrier
hz : z ∈ (↑H.toLieSubmodule.normalizer).carrier
x : ↥H
⊢ ⁅⁅↑x, y⁆, z⁆ + ⁅y, ⁅↑x, z⁆⁆ ∈ H

Tactic:
← lie_skew y,

Goal state after:
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
y z : L
hy : y ∈ (↑H.toLieSubmodule.normalizer).carrier
hz : z ∈ (↑H.toLieSubmodule.normalizer).carrier
x : ↥H
⊢ ⁅⁅↑x, y⁆, z⁆ + -⁅⁅↑x, z⁆, y⁆ ∈ H
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
x : L
h : 1 ⊗ₜ[R] x = 0
hx : x ∈ derivedSeries R L k
⊢ x = 0

Tactic:
Module.FaithfullyFlat.one_tmul_eq_zero_iff

Goal state after:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
x : L
h : x = 0
hx : x ∈ derivedSeries R L k
⊢ x = 0
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_1
R✝ : Type u_1
A✝ : Type u_2
L✝ : Type u_3
M : Type u_4
inst✝¹⁷ : CommRing R✝
inst✝¹⁶ : CommRing A✝
inst✝¹⁵ : Algebra R✝ A✝
inst✝¹⁴ : LieRing L✝
inst✝¹³ : LieAlgebra R✝ L✝
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R✝ M
inst✝¹⁰ : LieRingModule L✝ M
inst✝⁹ : LieModule R✝ L✝ M
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
⊢ ∀ (x : A) (y_1 : L),
    (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x ⊗ₜ[R] y_1)) y) =
      ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x ⊗ₜ[R] y_1)))
        ((TensorProduct.map f.toLinearMap ↑g) y)

Tactic:
intro _ _

Goal state after:
case refine_1
R✝ : Type u_1
A✝ : Type u_2
L✝ : Type u_3
M : Type u_4
inst✝¹⁷ : CommRing R✝
inst✝¹⁶ : CommRing A✝
inst✝¹⁵ : Algebra R✝ A✝
inst✝¹⁴ : LieRing L✝
inst✝¹³ : LieAlgebra R✝ L✝
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R✝ M
inst✝¹⁰ : LieRingModule L✝ M
inst✝⁹ : LieModule R✝ L✝ M
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝ ⊗ₜ[R] y✝)) y) =
    ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝ ⊗ₜ[R] y✝)))
      ((TensorProduct.map f.toLinearMap ↑g) y)
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2
R✝ : Type u_1
A✝ : Type u_2
L✝ : Type u_3
M : Type u_4
inst✝¹⁷ : CommRing R✝
inst✝¹⁶ : CommRing A✝
inst✝¹⁵ : Algebra R✝ A✝
inst✝¹⁴ : LieRing L✝
inst✝¹³ : LieAlgebra R✝ L✝
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R✝ M
inst✝¹⁰ : LieRingModule L✝ M
inst✝⁹ : LieModule R✝ L✝ M
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L),
    (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x) y) =
        ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x))
          ((TensorProduct.map f.toLinearMap ↑g) y) →
      (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y_1) y) =
          ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y_1))
            ((TensorProduct.map f.toLinearMap ↑g) y) →
        (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x + y_1)) y) =
          ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x + y_1)))
            ((TensorProduct.map f.toLinearMap ↑g) y)

Tactic:
intro _ _

Goal state after:
case refine_2
R✝ : Type u_1
A✝ : Type u_2
L✝ : Type u_3
M : Type u_4
inst✝¹⁷ : CommRing R✝
inst✝¹⁶ : CommRing A✝
inst✝¹⁵ : Algebra R✝ A✝
inst✝¹⁴ : LieRing L✝
inst✝¹³ : LieAlgebra R✝ L✝
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R✝ M
inst✝¹⁰ : LieRingModule L✝ M
inst✝⁹ : LieModule R✝ L✝ M
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y x✝ y✝ : A ⊗[R] L
⊢ (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x✝) y) =
      ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x✝))
        ((TensorProduct.map f.toLinearMap ↑g) y) →
    (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y✝) y) =
        ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y✝))
          ((TensorProduct.map f.toLinearMap ↑g) y) →
      (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝ + y✝)) y) =
        ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝ + y✝)))
          ((TensorProduct.map f.toLinearMap ↑g) y)
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: case refine_2
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
N : LieSubmodule R L M
z : M
hz : z ∈ (fun a ↦ ⁅x, a⁆) '' ↑↑N ∪ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}
⊢ z ∈ {x | ∃ x_1, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
· rcases hz with (⟨m, hm, rfl⟩ | ⟨y, -, m, hm, rfl⟩)
    exacts [⟨x, m, hm, rfl⟩, ⟨y, m, hm, rfl⟩]

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

Goal state before:
pp: case mpr
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
h : ∀ m ∈ lowerCentralSeries R L M 1, m = 0
x : L
m : M
⊢ ⁅x, m⁆ ∈ lowerCentralSeries R L M 1

Tactic:
apply LieSubmodule.subset_lieSpan

Goal state after:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
h : ∀ m ∈ lowerCentralSeries R L M 1, m = 0
x : L
m : M
⊢ ⁅x, m⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
⊢ IsNilpotent L ↥N ↔ ∃ k, LieSubmodule.lcs k N = ⊥

Tactic:
isNilpotent_iff R L N

Goal state after:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
⊢ (∃ k, lowerCentralSeries R L (↥N) k = ⊥) ↔ ∃ k, LieSubmodule.lcs k N = ⊥
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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✝ : IsNoetherian R M
⊢ IsNilpotent L M ↔ ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)

Tactic:
← isNilpotent_range_toEnd_iff (R := R),

Goal state after:
R : Type u₁
L : Type u₂
M : Type u₄
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✝ : IsNoetherian R M
⊢ IsNilpotent (↥(toEnd R L M).range) M ↔ ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
a✝ : Algebra.EssFiniteType F E
x : ↥(Algebra.EssFiniteType.subalgebra F E)
s : ↥(Algebra.EssFiniteType.submonoid F E)
x✝ : IsLocalization.mk' E x s ∈ ⊤
⊢ IsLocalization.mk' E x s ∈ adjoin F ↑(Algebra.EssFiniteType.finset F E)

Tactic:
have hs : s.1.1 ≠ 0 := (IsLocalization.map_units E s).ne_zero

Goal state after:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
a✝ : Algebra.EssFiniteType F E
x : ↥(Algebra.EssFiniteType.subalgebra F E)
s : ↥(Algebra.EssFiniteType.submonoid F E)
x✝ : IsLocalization.mk' E x s ∈ ⊤
hs : ↑↑s ≠ 0
⊢ IsLocalization.mk' E x s ∈ adjoin F ↑(Algebra.EssFiniteType.finset F E)
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : ↑((↑i + 1) * (↑n - ↑i)) • ((toEnd R L M) f ^ i) m = 0
⊢ False

Tactic:
smul_eq_zero,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : ↑((↑i + 1) * (↑n - ↑i)) = 0 ∨ ((toEnd R L M) f ^ i) m = 0
⊢ False
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
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
x : L
φ : Module.End R M := (toEnd R L M) x
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ y, (φ ^ i) y = (φ ^ (N + k)) m
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
hN : f₁ ^ N = 0
h₁ : Commute f₁ f₂
x✝¹ : L
x✝ : M
⊢ ((AlgebraTensorModule.curry (φ ∘ₗ ↑(toModuleHom R L M))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(toModuleHom R L M) ∘ₗ (f₁ + f₂))) x✝¹) x✝

Tactic:
simp [φ, f₁, f₂]

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

Goal state before:
pp: R : Type u_2
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
x : L
k : ℕ
⊢ ∀ (m : M) (l : ℕ), ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l

Tactic:
intro m l

Goal state after:
R : Type u_2
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
x : L
k : ℕ
m : M
l : ℕ
⊢ ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case neg
L : Type u_2
inst✝⁵ : LieRing L
K : Type u_4
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ LieSubmodule.restr I H ⊓ genWeightSpace L ⇑α ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H ⇑α

Tactic:
exact le_sup_of_le_right (le_iSup₂_of_le α hα le_rfl)

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✝ : IsAddTorsionFree L
i : ι
this : NoZeroSMulDivisors ℤ L
⊢ b.A i i = 2

Tactic:
have aux : (b.A i i - 2) • b.e i = 0 := by
    rw [sub_smul, ofNat_smul_eq_nsmul, ← (b.sl2 i).lie_h_e_nsmul, b.lie_h_e i i]; abel

Goal state after:
ι : 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✝ : IsAddTorsionFree L
i : ι
this : NoZeroSMulDivisors ℤ L
aux : (b.A i i - 2) • b.e i = 0
⊢ b.A i i = 2
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
this : FiniteDimensional K V
⊢ (b.dualBasis.repr ((B.toDual hB) x)) i = (B x) (b i)

Tactic:
Basis.dualBasis_repr,

Goal state after:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
this : FiniteDimensional K V
⊢ ((B.toDual hB) x) (b i) = (B x) (b i)
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
⊢ Submodule.map (Submodule.subtype W) (domRestrict B W).ker = W ⊓ B.orthogonal ⊤

Tactic:
rw [orthogonal_top_eq_ker b]

Goal state after:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
⊢ Submodule.map (Submodule.subtype W) (domRestrict B W).ker = W ⊓ ker B
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✝ : HasTrivialRadical R L
h : center R L = ⊤
⊢ Subsingleton L

Tactic:
center_eq_bot

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
h : ⊥ = ⊤
⊢ Subsingleton L
Module: Mathlib.LinearAlgebra.PID

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
⊢ (trace R ↥p) (f.restrict hf') = (trace R M) f

Tactic:
obtain ⟨n, snf⟩ := p.smithNormalForm (Module.Free.chooseBasis R M)

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
⊢ (trace R ↥p) (f.restrict hf') = (trace R M) f
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
x y z : L
⊢ -((traceForm R L M) y) ⁅x, z⁆ - ((traceForm R L M) ⁅x, y⁆) z = 0

Tactic:
traceForm_apply_lie_apply',

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
x y z : L
⊢ -((traceForm R L M) y) ⁅x, z⁆ - -((traceForm R L M) y) ⁅x, z⁆ = 0
Module: Mathlib.LinearAlgebra.FiniteSpan

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e) Φ Φ
e' : ↑Φ ≃ ↑Φ := BijOn.equiv (⇑e) he
this : Finite ↑Φ
k : ℕ
hk₀ : k > 0
m : M
hm : m ∈ span R Φ
x : M
hx : x ∈ Φ
hk : (e' ^ k) ⟨x, hx⟩ = 1 ⟨x, hx⟩
⊢ ↑((MapsTo.restrict (⇑e) Φ Φ ⋯)^[k] ⟨x, hx⟩) = x

Tactic:
rwa [Equiv.Perm.coe_one, id_eq, Subtype.ext_iff, Equiv.Perm.coe_pow] at hk

Goal state after:
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
P : R[X]
p_ne_zero : P ≠ 0
⊢ P ∈ span R (↑S '' Set.Iio (P.natDegree + 1))

Tactic:
span_degreeLT _ (by grind),

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
P : R[X]
p_ne_zero : P ≠ 0
⊢ P ∈ degreeLT R (P.natDegree + 1)
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:
rw [lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα, SetLike.mem_coe,
        Submodule.mem_span_singleton]

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 (-⇑α)
⊢ ∃ a,
    a • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) =
      ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
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
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
⊢ ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) =
    ↑(((killingForm K L) e) f' • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))

Tactic:
rw [Submodule.coe_smul_of_tower]

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 1 (U R (-↑n)) = ↑(-↑n) + 1
ih2 : eval 1 (U R (-↑n + 1)) = ↑(-↑n + 1) + 1
⊢ eval 1 (U R (-↑n - 1)) = ↑(-↑n - 1) + 1

Tactic:
simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one,
      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 1 (U R (-↑n)) = ↑(-↑n) + 1
ih2 : eval 1 (U R (-↑n + 1)) = ↑(-↑n + 1) + 1
⊢ 2 * (-↑n + 1) - (-↑n + 1 + 1) = -↑n
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, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)

Tactic:
by
  obtain ⟨e, heα : e ∈ rootSpace H α, he₀ : e ≠ 0⟩ := α.exists_ne_zero
  obtain ⟨f', hfα, hf⟩ : ∃ f ∈ rootSpace H (-α), killingForm K L e f ≠ 0 := by
    contrapose! he₀
    simpa using mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H heα he₀
  have hef := lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα
  let h : H := ⟨⁅e, f'⁆, hef ▸ Submodule.smul_mem _ _ (Submodule.coe_mem _)⟩
  have hh : α h ≠ 0 := by
    have : h = killingForm K L e f' • (cartanEquivDual H).symm α := by
      simp only [h, Subtype.ext_iff, hef]
      rw [Submodule.coe_smul_of_tower]
    rw [this, map_smul, smul_eq_mul, ne_eq, mul_eq_zero, not_or]
    exact ⟨hf, root_apply_cartanEquivDual_symm_ne_zero hα⟩
  let f := (2 * (α h)⁻¹) • f'
  replace hef : ⁅⁅e, f⁆, e⁆ = 2 • e := by
    have : ⁅⁅e, f'⁆, e⁆ = α h • e := lie_eq_smul_of_mem_rootSpace heα h
    rw [lie_smul, smul_lie, this, ← smul_assoc, smul_eq_mul, mul_assoc, inv_mul_cancel₀ hh,
      mul_one, two_smul, two_smul]
  refine ⟨⁅e, f⁆, e, f, ⟨fun contra ↦ ?_, rfl, hef, ?_⟩, heα, Submodule.smul_mem _ _ hfα⟩
  · rw [contra] at hef
    have : IsAddTorsionFree L := .of_isTorsionFree K L
    simp only [zero_lie, eq_comm (a := (0 : L)), smul_eq_zero, OfNat.ofNat_ne_zero, false_or] at hef
    contradiction
  · have : ⁅⁅e, f'⁆, f'⁆ = - α h • f' := lie_eq_smul_of_mem_rootSpace hfα h
    rw [lie_smul, lie_smul, smul_lie, this]
    simp [← smul_assoc, f, hh, mul_comm _ (2 * (α h)⁻¹)]

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
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) =
    ↑(((killingForm K L) e) f • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))

Tactic:
rw [Submodule.coe_smul_of_tower]

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : U R (↑n + 1 + 1) = X * U R (↑n + 1) + T R (↑n + 1 + 1)
ih2 : U R (↑n + 1) = X * U R ↑n + T R (↑n + 1)
h₁ : U R (↑n + 1 + 2) = 2 * X * U R (↑n + 1 + 1) - U R (↑n + 1)
h₂ : U R (↑n + 2) = 2 * X * U R (↑n + 1) - U R ↑n
⊢ U R (↑n + 2 + 1) = X * U R (↑n + 2) + T R (↑n + 2 + 1)

Tactic:
have h₃ := T_add_two R (n + 1)

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : U R (↑n + 1 + 1) = X * U R (↑n + 1) + T R (↑n + 1 + 1)
ih2 : U R (↑n + 1) = X * U R ↑n + T R (↑n + 1)
h₁ : U R (↑n + 1 + 2) = 2 * X * U R (↑n + 1 + 1) - U R (↑n + 1)
h₂ : U R (↑n + 2) = 2 * X * U R (↑n + 1) - U R ↑n
h₃ : T R (↑n + 1 + 2) = 2 * X * T R (↑n + 1 + 1) - T R (↑n + 1)
⊢ U R (↑n + 2 + 1) = X * U R (↑n + 2) + T R (↑n + 2 + 1)