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

Goal state before:
pp: case h
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hf_surj : Surjective ⇑f
hg_surj : Surjective ⇑g
inst✝ : LieModule.IsNilpotent L M
k : ℕ
hk : ↑(lowerCentralSeries R L M k) = ↑⊥
⊢ ↑(lowerCentralSeries R L₂ M₂ k) = ↑⊥

Tactic:
simp [← hf_surj.lieModule_lcs_map_eq hfg hg_surj k, hk]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p : k[X]
hp : Irreducible p
x : k
hx : eval x (p * C p.leadingCoeff⁻¹) = 0
⊢ eval x p = 0

Tactic:
simpa [hp.ne_zero] using hx

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit ((aeval a) (Multiset.map (fun x ↦ X - C x) p.roots).prod)
⊢ (σ a).Nonempty

Tactic:
obtain ⟨k, hk, _⟩ := exists_mem_of_not_isUnit_aeval_prod nu

Goal state after:
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit ((aeval a) (Multiset.map (fun x ↦ X - C x) p.roots).prod)
k : 𝕜
hk : k ∈ σ a
right✝ : eval k p = 0
⊢ (σ a).Nonempty
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
⊢ IsCoprime p q ↔ ∀ (a : K), (aeval a) p ≠ 0 ∨ (aeval a) q ≠ 0

Tactic:
refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hu h0 => ?_⟩

Goal state after:
case refine_1
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : ∀ (a : K), (aeval a) p ≠ 0 ∨ (aeval a) q ≠ 0
⊢ ¬(p = 0 ∧ q = 0)

case refine_2
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : ∀ (a : K), (aeval a) p ≠ 0 ∨ (aeval a) q ≠ 0
x : k[X]
hu : x ∈ nonunits k[X]
h0 : x ≠ 0
⊢ x ∣ p → ¬x ∣ q
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i ↦ (↑i).carrier
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
i j : ↑(insert ⊥ c)
h : (t i).toSubalgebra ≤ (t j).toSubalgebra
x : ↥(↑i).carrier
hji : ↑j ≤ ↑i
⊢ (↑i).emb x = (↑i).emb ((inclusion ⋯) x)

Tactic:
inclusion_self,

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i ↦ (↑i).carrier
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
i j : ↑(insert ⊥ c)
h : (t i).toSubalgebra ≤ (t j).toSubalgebra
x : ↥(↑i).carrier
hji : ↑j ≤ ↑i
⊢ (↑i).emb x = (↑i).emb ((AlgHom.id F ↥(t i)) x)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case right.refine_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
⊢ {α} ⊆ ↑(F⟮α⟯.toSubfield.subtype.comp f).fieldRange

Tactic:
refine Set.singleton_subset_iff.mpr ⟨AdjoinRoot.root (minpoly F α), ?_⟩
          rw [RingHom.comp_apply]
          dsimp only [coe_type_toSubfield]
          rw [AdjoinRoot.lift_root (aeval_gen_minpoly F α)]
          rfl

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

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H✝ : LieSubalgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
inst : Subsingleton ↥H
⊢ H = ⊥

Tactic:
rw [eq_bot_iff]

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H✝ : LieSubalgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
inst : Subsingleton ↥H
⊢ ∀ x ∈ H, x = 0
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case pos.add
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i ∈ s, genWeightSpace M i
hy✝ : y✝ ∈ ⨆ i ∈ s, genWeightSpace M i
hv : ⁅u, x✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
hw : ⁅u, y✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅u, x✝ + y✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
| add _ _ _ _ hv hw =>

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
χ : Weight R L M
x : L
this : genWeightSpaceOf M (χ x) x = ⊥
⊢ ⨅ x, genWeightSpaceOf M (χ x) x = ⊥

Tactic:
rw [eq_bot_iff]

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
χ : Weight R L M
x : L
this : genWeightSpaceOf M (χ x) x = ⊥
⊢ ⨅ x, genWeightSpaceOf M (χ x) x ≤ ⊥
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: 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
⊢ H.toLieSubmodule ≤ rootSpace H 0

Tactic:
by
  intro x hx
  simp only [LieSubalgebra.mem_toLieSubmodule] at hx
  simp only [mem_genWeightSpace, Pi.zero_apply, sub_zero, zero_smul]
  intro y
  obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R H H
  use k
  let f : Module.End R H := toEnd R H H y
  let g : Module.End R L := toEnd R H L y
  have hfg : g.comp (H : Submodule R L).subtype = (H : Submodule R L).subtype.comp f := rfl
  change (g ^ k).comp (H : Submodule R L).subtype ⟨x, hx⟩ = 0
  rw [Module.End.commute_pow_left_of_commute hfg k]
  have h := iterate_toEnd_mem_lowerCentralSeries R H H y ⟨x, hx⟩ k
  rw [hk, LieSubmodule.mem_bot] at h
  simp only [Submodule.subtype_apply, Function.comp_apply, Module.End.pow_apply, LinearMap.coe_comp,
    Submodule.coe_eq_zero]
  exact h

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

Goal state before:
pp: case inl
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
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
h✝ : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
h : ∀ (a : L), genWeightSpaceOf M 0 a = ⊤
⊢ IsCompl M₀ M₁

Tactic:
suffices IsNilpotent L M by simp [M₀, M₁, isCompl_top_bot]
    replace h : M₀ = ⊤ := by simpa [M₀, genWeightSpace]
    rw [← LieModule.isNilpotent_of_top_iff' (R := R), ← h]
    infer_instance

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
i j : ι
⊢ -⁅b.h i, -b.h j⁆ = 0

Tactic:
lie_neg,

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
i j : ι
⊢ - -⁅b.h i, b.h j⁆ = 0
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
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
⊢ P ⊤

Tactic:
induction (⊤ : LieSubmodule R L M) using
    (LieSubmodule.wellFoundedLT_of_isArtinian R L M).induction with | ind N hN

Goal state after:
case ind
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
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
⊢ P N
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
a : α
ha : a ≤ sSup S
⊢ ∃ T ⊆ S, a = sSup T

Tactic:
obtain ⟨C, hC, rfl⟩ := IsCompactlyGenerated.exists_sSup_eq a

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
⊢ ∃ T ⊆ S, sSup C = sSup T
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
a✝ : ∀ (y : LieIdeal K L), InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ finrank K ↥x) y I → sSup {J | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h✝ : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := ⋯
this : I ≤ J ⊔ J' ⊓ I
hIJ' : I ≤ J'
⊢ J = ⊥

Tactic:
rw [eq_bot_iff]

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
a✝ : ∀ (y : LieIdeal K L), InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ finrank K ↥x) y I → sSup {J | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h✝ : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
hIJ' : I ≤ J'
⊢ J ≤ ⊥
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
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
⊢ W ⊓ B.orthogonal W = ⊥

Tactic:
rw [eq_bot_iff]

Goal state after:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
⊢ W ⊓ B.orthogonal W ≤ ⊥
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
J : LieIdeal K L
⊢ IsAtom J → ¬J = I → J ≤ orthogonal Φ hΦ_inv I

Tactic:
hJ

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
J : LieIdeal K L
hJ : IsAtom J
⊢ ¬J = I → J ≤ orthogonal Φ hΦ_inv I
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
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
x : L
hx : x ∈ I
⊢ x ∈ (insert J s').sup id

Tactic:
Finset.insert_erase hJs

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}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
x : L
hx : x ∈ I
⊢ x ∈ s.sup id
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m.prod = ∏ x, x.fst

Tactic:
by
  congr
  simp

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m.prod = ∏ x ∈ m.toEnumFinset, x.1

Tactic:
by
  congr
  simp

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
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
e : Nat.find ⋯ = 0
this : genWeightSpace M (0 • α + ⇑β) = ⊥
⊢ genWeightSpace M ⇑β = ⊥

Tactic:
simpa only [zero_smul, zero_add] using this

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
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
⊢ (α + β) x' • ⁅y, z⁆ = (α x' + β x') • ⁅y, z⁆

Tactic:
← Pi.add_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
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
⊢ (α + β) x' • ⁅y, z⁆ = (α + β) x' • ⁅y, z⁆
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:
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: motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
⊢ ∀ (a : ℤ), motive a

Tactic:
refine Chebyshev.induct motive zero one add_two ?_

Goal state after:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
⊢ ∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : R
ht : t = f y * g x - 2
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
ht' : t = g x * f y - 2
⊢ ((reflection hf * reflection hg) ^ ↑m)⁻¹ z =
    z +
        (Polynomial.eval t (S R ((-↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((-↑m - 1) / 2)) + Polynomial.eval t (S R ((-↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((-↑m - 1) / 2)) *
          (Polynomial.eval t (S R (-↑m / 2)) + Polynomial.eval t (S R ((-↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)

Tactic:
← inv_zpow,

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : R
ht : t = f y * g x - 2
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
ht' : t = g x * f y - 2
⊢ ((reflection hf * reflection hg)⁻¹ ^ ↑m) z =
    z +
        (Polynomial.eval t (S R ((-↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((-↑m - 1) / 2)) + Polynomial.eval t (S R ((-↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((-↑m - 1) / 2)) *
          (Polynomial.eval t (S R (-↑m / 2)) + Polynomial.eval t (S R ((-↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
g : ↥H → R
hg : g ∈ sU
contra : g = 0
⊢ ∃ n, n ≠ 0 ∧ g = -⇑(∑ i, n i • b.baseSupp i)

Tactic:
simpa [hsU] using hg

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this✝ : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
n : ι → ℕ
hn : n ≠ 0
hg : -⇑(∑ i, n i • b.baseSupp i) ∈ sU
contra : ∑ i, n i • b.baseSupp i = 0
this : ∀ (i : ι), (Nat.cast ∘ n) i = 0
i : ι
⊢ n i = 0 i

Tactic:
simpa using this i

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.reflection ((P.reflectionPerm j) i) = P.reflection j * P.reflection i * P.reflection j

Tactic:
ext x; simp [reflection_apply, coreflection_apply]; module

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this✝ : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
n : ι → ℕ
hn : n ≠ 0
hg : ⇑(∑ i, n i • b.baseSupp i) ∈ sV
contra : ∑ i, n i • b.baseSupp i = 0
this : ∀ (i : ι), (Nat.cast ∘ n) i = 0
i : ι
⊢ n i = 0 i

Tactic:
simpa using this i

Goal state after: