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

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
hα : ¬α.IsZero
⊢ ↑(chainTopCoeff (⇑α) β') + ↑(chainBotCoeff (⇑α) β') = ↑(chainTopCoeff (⇑α) β) + ↑(chainBotCoeff (⇑α) β)

Tactic:
chainTopCoeff_of_eq_zsmul_add α β hα β' n hβ',

Goal state after:
case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
hα : ¬α.IsZero
⊢ ↑(chainTopCoeff (⇑α) β) - n + ↑(chainBotCoeff (⇑α) β') = ↑(chainTopCoeff (⇑α) β) + ↑(chainBotCoeff (⇑α) β)
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Semiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
⊢ (ρ g⁻¹) ((ρ g) x) = x

Tactic:
simp [← Module.End.mul_apply, ← map_mul]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Semiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
⊢ (ρ g) ((ρ g⁻¹) x) = x

Tactic:
simp [← Module.End.mul_apply, ← map_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

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
inst✝ : P.IsRootSystem
x : M
h : ∀ (i : ι), (P.coroot' i) x = 0
⊢ x = 0

Tactic:
replace h : x ∈ ⨅ i, ker (P.coroot' i) := by aesop

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
inst✝ : P.IsRootSystem
x : M
h : x ∈ ⨅ i, ker (P.coroot' i)
⊢ x = 0
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case zero
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Ring k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
⊢ (ρ g - LinearMap.id) (Fin.partialSum (fun j ↦ (ρ (g ^ ↑j)) x) (Fin.last (0 + 1))) = (ρ (g ^ (0 + 1))) x - x

Tactic:
simp [Fin.partialSum]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : P.root k ∈ Q
j : ι
hj : j ∈ {i | P.root i ∉ Q}
⊢ P.root j ∈ ↑(ker (P.coroot' k))

Tactic:
SetLike.mem_coe,

Goal state after:
case pos
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : P.root k ∈ Q
j : ι
hj : j ∈ {i | P.root i ∉ Q}
⊢ P.root j ∈ ker (P.coroot' k)
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

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
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
B : P.InvariantForm
i j : ι
contra : ∀ (k : ι), (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j) → (B.form (P.root i)) (P.root k) = 0
g : ↥P.weylGroup
hv : g • P.root j ∈ orbit (↥P.weylGroup) (P.root j)
⊢ (B.form (P.root ((P.weylGroupToPerm g) j))) (P.root ((P.weylGroupToPerm g) j)) = (B.form (P.root j)) (P.root j)

Tactic:
simp [← Subgroup.smul_def g]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
n : ℕ
⊢ P.root j + ↑n • P.root i ∈ range ⇑P.root ↔ ↑n ∈ Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)

Tactic:
simp [P.root_add_nsmul_mem_range_iff_le_chainTopCoeff h]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
i : ι
this : ↑(P.rootSpanMem ℚ i) ∈ span ℚ (⇑P.root '' baseOf (⇑P.root) f)
⊢ (P.rootSpan ℚ).subtype (P.rootSpanMem ℚ i) ∈ ↑(map (P.rootSpan ℚ).subtype (span ℚ (range v)))

Tactic:
SetLike.mem_coe,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
i : ι
this : ↑(P.rootSpanMem ℚ i) ∈ span ℚ (⇑P.root '' baseOf (⇑P.root) f)
⊢ (P.rootSpan ℚ).subtype (P.rootSpanMem ℚ i) ∈ map (P.rootSpan ℚ).subtype (span ℚ (range v))
Module: Mathlib.LinearAlgebra.RootSystem.Base

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
b : P.Base
inst✝ : CharZero R
f✝ : ι → ℤ
hf : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
c : ↑↑b.support → ℕ
hc : ∀ (i : ↥b.support), ↑(c i) = f' i
i : ι
hi : i ∈ Function.support f
⊢ i ∈ b.support

Tactic:
exact hf₀ hi

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
this : chainBotCoeff i j = 0 ↔ Iic (chainBotCoeff i j) = {0}
n : ℕ
h'' : P.root j - n • P.root i ∈ range ⇑P.root
h' : chainBotCoeff i j < 1
⊢ n = 0

Tactic:
Nat.lt_one_iff

Goal state after:
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
this : chainBotCoeff i j = 0 ↔ Iic (chainBotCoeff i j) = {0}
n : ℕ
h'' : P.root j - n • P.root i ∈ range ⇑P.root
h' : chainBotCoeff i j = 0
⊢ n = 0
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i : ℕ
h : ∀ j ≥ i, abv (f j - f i) < 1
⊢ ∃ r, ∀ (i : ℕ), abv (f i) < r

Tactic:
set R : ℕ → α := @Nat.rec (fun _ => α) (abv (f 0)) fun i c => max c (abv (f i.succ)) with hR

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i : ℕ
h : ∀ j ≥ i, abv (f j - f i) < 1
R : ℕ → α := Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
hR : R = Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
⊢ ∃ r, ∀ (i : ℕ), abv (f i) < r
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case refine_2
ι : 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
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
h₅ : k ∈ b.support
⊢ P.root l = ∑ m, P.root (Fin.snoc f k m)

pp: case refine_3
ι : 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
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
h₅ : k ∈ b.support
m : Fin (n + 1)
⊢ ∑ m' ≤ m, P.root (Fin.snoc f k m') ∈ range ⇑P.root

Tactic:
· simp [Fin.sum_univ_castSucc, h₁, h₃]

Goal state after:
case refine_3
ι : 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
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
h₅ : k ∈ b.support
m : Fin (n + 1)
⊢ ∑ m' ≤ m, P.root (Fin.snoc f k m') ∈ range ⇑P.root
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ mk (f + g) = mk f + mk g

Tactic:
simp [mk, ← ofCauchy_add]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ 1 ≤ ↑(const (K + 1) - f) i

Tactic:
sub_apply,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ 1 ≤ ↑(const (K + 1)) i - ↑f i
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ ↑(y✝ - f) j
i : ℕ
H : ∀ j ≥ i, mk y✝ ≤ ↑(↑f j) ∧ K ≤ ↑(y✝ - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2
j : ℕ
ij : j ≥ i
this : K / 2 ≤ ↑(y✝ - f) j + (↑f j - ↑f i)
⊢ K / 2 ≤ ↑(y✝ - const abs (↑f i)) j

Tactic:
sub_apply,

Goal state after:
case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ ↑(y✝ - f) j
i : ℕ
H : ∀ j ≥ i, mk y✝ ≤ ↑(↑f j) ∧ K ≤ ↑(y✝ - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2
j : ℕ
ij : j ≥ i
this : K / 2 ≤ ↑y✝ j - ↑f j + (↑f j - ↑f i)
⊢ K / 2 ≤ ↑(y✝ - const abs (↑f i)) j
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h₂
b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ a * ↑b + 1 ≤ (a + 1) ^ b

Tactic:
exact hb ha'

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
hA : A.IsHermitian
⊢ A.adjugate.IsHermitian

Tactic:
by simp [IsHermitian, adjugate_conjTranspose, hA.eq]

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

Goal state before:
pp: case refine_1
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ genWeightSpace L ⇑(b.baseSupp i) ≠ ⊥

pp: case refine_2
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ { toFun := ⇑(b.baseSupp i), genWeightSpace_ne_bot' := ?refine_1 } ∈ root

Tactic:
· simp only [LieSubmodule.eq_bot_iff, ne_eq, not_forall]
    exact ⟨b.e i, (mem_genWeightSpace _ _ _).mpr fun x ↦ ⟨1, by simp⟩, (b.sl2 i).e_ne_zero⟩

Goal state after:
case refine_2
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ { toFun := ⇑(b.baseSupp i), genWeightSpace_ne_bot' := ⋯ } ∈ root
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i : ι
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : b.h' i ∈ corootSpace ⇑(Weight.toLinear K (↥H) L ↑(b.baseSupp' i))
⊢ coroot ↑↑(b.baseSupportEquiv i) = b.h' i

Tactic:
by
    have _i : IsAddTorsionFree L := .of_isTorsionFree K L
    exact (eq_coroot_of_mem_corootSpace_of_two (b.baseSupp' i).val this (by simp [baseSupp'])).symm

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := ⋯
⊢ H.normalizer ≤ H

Tactic:
calc N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule := ?_
       _ = H := by rwa [sup_eq_right]

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
⊢ N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this✝ : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
this : ∀ (i : I), f ⟨μ i, ⋯⟩ = 0
⊢ f = 0

Tactic:
Submodule.linearMap_eq_zero_iff_of_eq_span f rfl

Goal state after:
L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this✝ : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
this : ∀ (i : I), f ⟨μ i, ⋯⟩ = 0
⊢ ∀ (s : ↑(Set.range μ)), f ⟨↑s, ⋯⟩ = 0
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(((decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
⊢ ↑(((of (fun i ↦ ↥(𝒜 i)) (k + i)) ⟨↑(((decompose 𝒜) r) k) * x, mem₁⟩) j) ∈ I

Tactic:
coe_of_apply

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(((decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
⊢ ↑(if k + i = j then ⟨↑(((decompose 𝒜) r) k) * x, mem₁⟩ else 0) ∈ I
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
h : ∀ (x y : L), y ∈ derivedSeries R L 1 → ((killingForm R L) x) y = 0
⊢ IsSolvable L

Tactic:
suffices IsSolvable (⊤ : LieIdeal R L) by
    rwa [← solvable_iff_equiv_solvable LieSubalgebra.topEquiv (R := R)]
  apply LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero
  aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
M : n × n → S
i : ℕ
⊢ (MvPolynomial.eval₂Hom f M) ((univ R n).coeff i) = (of (Function.curry M)).charpoly.coeff i

Tactic:
← univ_map_eval₂Hom n f M,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
M : n × n → S
i : ℕ
⊢ (MvPolynomial.eval₂Hom f M) ((univ R n).coeff i) = (Polynomial.map (MvPolynomial.eval₂Hom f M) (univ R n)).coeff i
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
I_le_J : I ≤ J
⊢ homogeneousHull 𝒜 I ≤ homogeneousHull 𝒜 J

Tactic:
by
  apply Ideal.span_mono
  rintro r ⟨hr1, ⟨x, hx⟩, rfl⟩
  exact ⟨hr1, ⟨⟨x, I_le_J hx⟩, rfl⟩⟩

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
f : R →+* S
⊢ ((map f) φ).IsHomogeneous n

Tactic:
rw [map_eq_eval₂Hom_C_comp]

Goal state after:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
f : R →+* S
⊢ ((eval₂Hom (C.comp f) X) φ).IsHomogeneous n
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ (coeLinearMap fun i ↦ weightedHomogeneousSubmodule R w i) x = ∑ᶠ (m : M), ↑(x m)

Tactic:
rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset]
  apply DirectSum.support_subset

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ ((homogeneousComponent n) p).support = {c ∈ p.support | (weight fun x ↦ 1) c = n}

Tactic:
exact support_weightedHomogeneousComponent n p

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * b * J l R * (bᵀ * aᵀ) = J l R

Tactic:
rw [← Matrix.mul_assoc, a.mul_assoc, a.mul_assoc, hb]

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * J l R * aᵀ = J l R
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case calc.step
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(Submodule.map (LinearMap.funLeft R R r) (Submodule.map A.mulVecLin ⊤)) ≤ finrank R ↥A.mulVecLin.range

Tactic:
Submodule.map_top

Goal state after:
case calc.step
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(Submodule.map (LinearMap.funLeft R R r) A.mulVecLin.range) ≤ finrank R ↥A.mulVecLin.range
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i : ι) (y : L i),
    (toModule R ι L' f') ⁅x, (of L i) y⁆ = ⁅(toModule R ι L' f') x, (toModule R ι L' f') ((of L i) y)⁆
⊢ (toModule R ι L' fun i ↦ ↑(f i)) ⁅x, y⁆ = ⁅(toModule R ι L' fun i ↦ ↑(f i)) x, (toModule R ι L' fun i ↦ ↑(f i)) y⁆

Tactic:
simp only [← LieAlgebra.ad_apply R]
        rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]
        congr; clear y; ext i y; exact this i y

Goal state after: