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

Goal state before:
pp: R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
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₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
m₃ : M₃
⊢ ∀ (x_1 : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)),
    g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) x_1) = m₃ →
      ∃ k, (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k) m₃ = 0

Tactic:
rintro t rfl

Goal state after:
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
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₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
⊢ ∃ k,
    (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) t)) = 0
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ -h ≠ 0

Tactic:
by simpa using ht.h_ne_zero

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

Goal state before:
pp: case mem.mem
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
t : IsSl2Triple h e f
x y u : L
hu : u ∈ {e, f, h}
v : L
hv : v ∈ {e, f, h}
⊢ ⁅u, v⁆ ∈ span R {e, f, h}

Tactic:
push _ ∈ _ at hu hv

Goal state after:
case mem.mem
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
t : IsSl2Triple h e f
x y u v : L
hu : u = e ∨ u = f ∨ u = h
hv : v = e ∨ v = f ∨ v = h
⊢ ⁅u, v⁆ ∈ span R {e, f, h}
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case succ
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 μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ ⁅h, ((toEnd R L M) f) (((toEnd R L M) f ^ n) m)⁆ = (μ - 2 * ↑(n + 1)) • ((toEnd R L M) f) (((toEnd R L M) f ^ n) m)

Tactic:
toEnd_apply_apply,

Goal state after:
case succ
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 μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ ⁅h, ⁅f, ((toEnd R L M) f ^ n) m⁆⁆ = (μ - 2 * ↑(n + 1)) • ⁅f, ((toEnd R L M) f ^ n) m⁆
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case succ
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 μ
n : ℕ
ih : ⁅e, ((toEnd R L M) f ^ (n + 1)) m⁆ = ((↑n + 1) * (μ - ↑n)) • ((toEnd R L M) f ^ n) m
⊢ ⁅e, ((toEnd R L M) f) (((toEnd R L M) f ^ (n + 1)) m)⁆ =
    ((↑(n + 1) + 1) * (μ - ↑(n + 1))) • ((toEnd R L M) f ^ (n + 1)) m

Tactic:
toEnd_apply_apply,

Goal state after:
case succ
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 μ
n : ℕ
ih : ⁅e, ((toEnd R L M) f ^ (n + 1)) m⁆ = ((↑n + 1) * (μ - ↑n)) • ((toEnd R L M) f ^ n) m
⊢ ⁅e, ⁅f, ((toEnd R L M) f ^ (n + 1)) m⁆⁆ = ((↑(n + 1) + 1) * (μ - ↑(n + 1))) • ((toEnd R L M) f ^ (n + 1)) m
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) (((toEnd R (↥H) L) ⟨y, hy⟩) x) = 0

Tactic:
toEnd_apply_apply,

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅⟨y, hy⟩, x⁆ = 0
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case succ
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
hm : ⁅h, m⁆ = μ • m
n : ℕ
ih : ⁅h, ((toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((toEnd R L M) e ^ n) m
⊢ ⁅h, ((toEnd R L M) e) (((toEnd R L M) e ^ n) m)⁆ = (μ + 2 * ↑(n + 1)) • ((toEnd R L M) e) (((toEnd R L M) e ^ n) m)

Tactic:
toEnd_apply_apply,

Goal state after:
case succ
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
hm : ⁅h, m⁆ = μ • m
n : ℕ
ih : ⁅h, ((toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((toEnd R L M) e ^ n) m
⊢ ⁅h, ⁅e, ((toEnd R L M) e ^ n) m⁆⁆ = (μ + 2 * ↑(n + 1)) • ⁅e, ((toEnd R L M) e ^ n) m⁆
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case succ
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
hm : ⁅h, m⁆ = μ • m
n : ℕ
ih : ⁅h, ((toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((toEnd R L M) e ^ n) m
⊢ ⁅h, ((toEnd R L M) e ^ (n + 1)) m⁆ = (μ + 2 * ↑(n + 1)) • ((toEnd R L M) e ^ (n + 1)) m

Tactic:
rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, Nat.cast_add, Nat.cast_one,
      leibniz_lie h, IsSl2Triple.lie_h_e_smul R t, smul_lie, ih, lie_smul, ← add_smul]

Goal state after:
case succ
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
hm : ⁅h, m⁆ = μ • m
n : ℕ
ih : ⁅h, ((toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((toEnd R L M) e ^ n) m
⊢ (2 + (μ + 2 * ↑n)) • ⁅e, ((toEnd R L M) e ^ n) m⁆ = (μ + 2 * (↑n + 1)) • ⁅e, ((toEnd R L M) e ^ n) m⁆
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
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Nontrivial M
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ : ((toEnd R L M) h).HasEigenvalue μ₀
m₀ : M
hm₀ : ((toEnd R L M) h).HasEigenvector μ₀ m₀
evals : ℕ → R := fun n ↦ μ₀ + 2 * ↑n
e_vecs : ℕ → M := fun n ↦ ((toEnd R L M) e ^ n) m₀
contra : ∀ (k : ℕ), e_vecs k ≠ 0
h_inj : Function.Injective evals
μ : ↑(range evals)
n : ℕ := Exists.choose ⋯
⊢ ((toEnd R L M) h) (e_vecs n) = ↑μ • e_vecs n

Tactic:
toEnd_apply_apply,

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
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Nontrivial M
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ : ((toEnd R L M) h).HasEigenvalue μ₀
m₀ : M
hm₀ : ((toEnd R L M) h).HasEigenvector μ₀ m₀
evals : ℕ → R := fun n ↦ μ₀ + 2 * ↑n
e_vecs : ℕ → M := fun n ↦ ((toEnd R L M) e ^ n) m₀
contra : ∀ (k : ℕ), e_vecs k ≠ 0
h_inj : Function.Injective evals
μ : ↑(range evals)
n : ℕ := Exists.choose ⋯
⊢ ⁅h, e_vecs n⁆ = ↑μ • e_vecs n
Module: Mathlib.LinearAlgebra.BilinearForm.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_9
b : Basis ι R M
x y : M
⊢ ((b.repr x).sum fun i xi ↦ (b.repr y).sum fun j yj ↦ xi • yj • (B (b i)) (b j)) = (B x) y

Tactic:
conv_rhs => rw [← b.linearCombination_repr x, ← b.linearCombination_repr y]
  simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, sum_left, sum_right, smul_left, smul_right,
    smul_eq_mul]

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

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommMonoid M
R : Type u_8
inst✝² : Field R
inst✝¹ : NeZero 2
inst✝ : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
⊢ (B x) y = ((B (x + y)) (x + y) - (B x) x - (B y) y) / 2

Tactic:
by
  simp only [map_add, LinearMap.add_apply]
  rw [hB.eq y x]
  ring_nf
  rw [mul_assoc, inv_mul_cancel₀ two_ne_zero, mul_one]

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ sSup ((Ta ∪ Tb) ∩ (Ta ∪ Tc)) = sSup Ta ⊔ sSup (Tb ∩ Tc)

pp: case hT₁
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ Ta ∪ Tb ⊆ S

pp: case hT₂
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ Ta ∪ Tc ⊆ S

Tactic:
← sSup_union

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ sSup ((Ta ∪ Tb) ∩ (Ta ∪ Tc)) = sSup (Ta ∪ Tb ∩ Tc)

case hT₁
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ Ta ∪ Tb ⊆ S

case hT₂
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ Ta ∪ Tc ⊆ S
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
by
    obtain ⟨Ta, hTa, rfl⟩ := hS.atomistic a (h ▸ le_top)
    obtain ⟨Tb, hTb, rfl⟩ := hS.atomistic b (h ▸ le_top)
    obtain ⟨Tc, hTc, rfl⟩ := hS.atomistic c (h ▸ le_top)
    apply le_of_eq
    rw [← sSup_union, ← sSup_union, ← hS.sSup_inter hTb hTc, ← hS.sSup_inter, ← sSup_union]
    on_goal 1 => congr 1; ext
    all_goals
      simp only [Set.union_subset_iff, Set.mem_inter_iff, Set.mem_union]
      tauto

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

Goal state before:
pp: case refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (y : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) m) y = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ (B ↑m) y + (B ↑m) z = 0

Tactic:
b₂ y m <| m.2 y hy,

Goal state after:
case refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (y : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) m) y = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ 0 + (B ↑m) z = 0
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: case pos
K : Type v
inst✝ : Field K
f : K[X]
H : ∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible (Classical.choose H)

pp: case neg
K : Type v
inst✝ : Field K
f : K[X]
H : ¬∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible X

Tactic:
· exact (Classical.choose_spec H).1

Goal state after:
case neg
K : Type v
inst✝ : Field K
f : K[X]
H : ¬∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible X
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
⊢ (∀ (i : ι), ∃ n, (A ^ n)ᵀ.row i = 0) ↔ ∀ (i : ι), ∃ n, (A ^ n).col i = 0

Tactic:
row_transpose

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
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
f : End R ↥(genWeightSpaceChain M α χ p q) := ⋯
g : End R ↥(genWeightSpaceChain M α χ p q) := ⋯
x✝ : ↥(genWeightSpaceChain M α χ p q)
⊢ ↑(((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) u) x✝) = ↑(⁅f, g⁆ x✝)

Tactic:
toEnd_apply_apply,

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
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
g : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨m, hm⟩ => ⟨⁅z, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
x✝ : ↥(genWeightSpaceChain M α χ p q)
⊢ ↑⁅u, x✝⁆ = ↑(⁅f, g⁆ x✝)
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✝ : IsTrivial L M
⊢ traceForm R L M = 0

Tactic:
by
  ext x y
  suffices φ x ∘ₗ φ y = 0 by simp [traceForm_apply_apply, this]
  ext m
  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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent ((ad K L) x)
⊢ ⟨x, hx⟩ ∈ LinearMap.ker (traceForm K (↥H) L)

Tactic:
simp only [LinearMap.mem_ker]

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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent ((ad K L) x)
⊢ (traceForm K (↥H) L) ⟨x, hx⟩ = 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
α : Weight K (↥H) L
x : ↥H
⊢ (Weight.toLinear K (↥H) L α) x = α x

Tactic:
Weight.toLinear_apply

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
α : Weight K (↥H) L
x : ↥H
⊢ α x = α x
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
⊢ coroot α = 0 ↔ α.IsZero

Tactic:
by
  refine ⟨fun hα ↦ ?_, fun hα ↦ ?_⟩
  · by_contra contra
    simpa [hα, ← α.coe_coe, map_zero] using root_apply_coroot contra
  · simp [coroot, Weight.coe_toLinear_eq_zero_iff.mpr hα]

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

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

Tactic:
have h₁ := C_add_two R n
    have h₂ := C_sub_two R (-n)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 - h₁ + h₂

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 : (C R (-↑n)).comp (2 * X) = 2 * T R (-↑n)
ih2 : (C R (-↑n + 1)).comp (2 * X) = 2 * T R (-↑n + 1)
⊢ (X * C R (-↑n) - C R (-↑n + 1)).comp (2 * X) = 2 * T R (-↑n - 1)

Tactic:
T_sub_one,

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (-↑n)).comp (2 * X) = 2 * T R (-↑n)
ih2 : (C R (-↑n + 1)).comp (2 * X) = 2 * T R (-↑n + 1)
⊢ (X * C R (-↑n) - C R (-↑n + 1)).comp (2 * X) = 2 * (2 * X * T R (-↑n) - T R (-↑n + 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✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hx : x ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
β : Weight K (↥H) L
hβ : β.IsNonZero
y g : L
hy : y ∈ genWeightSpace L ⇑β
hg : g ∈ rootSpace H ⇑β
hg_ne_zero : g ≠ 0
⊢ ¬⟨g, hg⟩ = 0

Tactic:
LieSubmodule.mk_eq_zero

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✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hx : x ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
β : Weight K (↥H) L
hβ : β.IsNonZero
y g : L
hy : y ∈ genWeightSpace L ⇑β
hg : g ∈ rootSpace H ⇑β
hg_ne_zero : g ≠ 0
⊢ ¬g = 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-↑n)) = T R' (-↑n)
ih2 : map f (T R (-↑n + 1)) = T R' (-↑n + 1)
⊢ map f (T R (-↑n - 1)) = T R' (-↑n - 1)

Tactic:
T_sub_one,

Goal state after:
case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-↑n)) = T R' (-↑n)
ih2 : map f (T R (-↑n + 1)) = T R' (-↑n + 1)
⊢ map f (2 * X * T R (-↑n) - T R (-↑n + 1)) = 2 * X * T R' (-↑n) - T R' (-↑n + 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℤ
⊢ map f (C R n) = C R' n

Tactic:
by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

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
I : LieIdeal K L
⊢ LieSubmodule.restr I H =
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), rootSpace H ⇑↑α

Tactic:
refine le_antisymm ?_ (sup_le inf_le_left (iSup₂_le fun _ hα ↦ hα))
  conv_lhs => rw [lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace]
  refine sup_le_sup_left (iSup₂_le fun α hα ↦ ?_) _
  by_cases h : rootSpace H α ≤ I.restr H
  · exact le_iSup₂_of_le ⟨α, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hα⟩⟩ h inf_le_right
  · have ha := Submodule.isAtom_iff_finrank_eq_one.mpr (finrank_rootSpace_eq_one α hα)
    have : I.restr H ⊓ rootSpace H (α : H → K) = ⊥ :=
      LieSubmodule.toSubmodule_injective ((ha.not_le_iff_disjoint.mp h).symm.eq_bot)
    simp only [this, bot_le]

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 : ι
⊢ (P.toLinearMap (-P.root i)) (P.coroot j) = -P.pairing i j

Tactic:
LinearMap.map_neg₂,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ -(P.toLinearMap (P.root i)) (P.coroot j) = -P.pairing i j
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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (2 • ⇑(P.reflection i)) x = (2 • ⇑(P.reflection j)) x

Tactic:
suffices
      2 • P.toLinearMap x (P.coroot i) • P.root i = 2 • P.toLinearMap x (P.coroot j) • P.root j by
    simpa [reflection_apply, smul_sub]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ 2 • (P.toLinearMap x) (P.coroot i) • P.root i = 2 • (P.toLinearMap x) (P.coroot j) • P.root j