mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : n₀ ∈ K[n₁ + s₁]
s₀ : End K V
hs₀ : s₀ ∈ K[n₁ + s₁]
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
n s : End K V
hn : IsNilpotent n
hs : s.IsSemisimple
hc : Commute n s
heq : n₁ + s₁ = n + s
hsf : Commute s (n₁ + s₁)
hnf : Commute n (n₁ + s₁)
⊢ IsNilpotent (s - s₀)

Tactic:
rw [show s - s₀ = n₀ - n by grind]

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : n₀ ∈ K[n₁ + s₁]
s₀ : End K V
hs₀ : s₀ ∈ K[n₁ + s₁]
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
n s : End K V
hn : IsNilpotent n
hs : s.IsSemisimple
hc : Commute n s
heq : n₁ + s₁ = n + s
hsf : Commute s (n₁ + s₁)
hnf : Commute n (n₁ + s₁)
⊢ IsNilpotent (n₀ - n)
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case zero
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ⇑f
⊢ map f (derivedSeries R L' 0) = derivedSeries R L 0

Tactic:
change (⊤ : LieIdeal R L').map f = ⊤
    rw [← f.idealRange_eq_map]
    exact f.idealRange_eq_top_of_surjective h

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable ↥I
⊢ (match derivedLengthOfIdeal R L I with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I) =
      ⊥ ↔
    I = ⊥

Tactic:
split

Goal state after:
case h_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable ↥I
x✝ : ℕ
heq✝ : derivedLengthOfIdeal R L I = 0
⊢ ⊥ = ⊥ ↔ I = ⊥

case h_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable ↥I
x✝ k✝ : ℕ
heq✝ : derivedLengthOfIdeal R L I = k✝.succ
⊢ derivedSeriesOfIdeal R L k✝ I = ⊥ ↔ I = ⊥
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝ k : ℕ
h✝ : IsSolvable ↥⊥
h : derivedLengthOfIdeal R L ⊥ = k.succ
left✝ : IsLieAbelian ↥(derivedSeriesOfIdeal R L k ⊥)
h₂ : derivedSeriesOfIdeal R L k ⊥ ≠ ⊥
⊢ False

Tactic:
apply h₂

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝ k : ℕ
h✝ : IsSolvable ↥⊥
h : derivedLengthOfIdeal R L ⊥ = k.succ
left✝ : IsLieAbelian ↥(derivedSeriesOfIdeal R L k ⊥)
h₂ : derivedSeriesOfIdeal R L k ⊥ ≠ ⊥
⊢ derivedSeriesOfIdeal R L k ⊥ = ⊥
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: case refine_1
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
⊢ {x | ∃ x_1, ∃ n ∈ N, ⁅x_1, n⁆ = x} ⊆
    ↑(Submodule.span R ((fun a ↦ ⁅x, a⁆) '' ↑↑N ∪ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}))

Tactic:
rintro z ⟨y, n, hn : n ∈ N, rfl⟩
    obtain ⟨t, z, hz, rfl⟩ := exists_smul_add_of_span_sup_eq_top hxI y
    simp only [SetLike.mem_coe, Submodule.span_union, Submodule.mem_sup]
    exact
      ⟨t • ⁅x, n⁆, Submodule.subset_span ⟨t • n, N.smul_mem' t hn, lie_smul t x n⟩, ⁅z, n⁆,
        Submodule.subset_span ⟨z, hz, n, hn, rfl⟩, by simp⟩

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

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x r : S
⊢ m • r = m • eval x (C r)

Tactic:
eval_C

Goal state after:
M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x r : S
⊢ m • r = m • r
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
⊢ LieAlgebra.IsEngelian R L₂

Tactic:
by
  intro M _i1 _i2 _i3 _i4 h'
  let : LieRingModule L M := LieRingModule.compLieHom M f
  let : LieModule R L M := compLieHom M f
  have hnp : ∀ x, IsNilpotent (toEnd R L M x) := fun x => h' (f x)
  have surj_id : Function.Surjective (LinearMap.id : M →ₗ[R] M) := Function.surjective_id
  have : LieModule.IsNilpotent L M := h M hnp
  apply hf.lieModuleIsNilpotent _ surj_id
  aesop

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
inst✝ : LieModule R L M
⊢ ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)

Tactic:
by
  induction k with
  | zero => simp
  | succ k ih =>
    simp_rw [lowerCentralSeries_succ, lcs_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (I.lcs M k).mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule, LieSubmodule.mem_top,
      true_and, (I : LieSubalgebra R L).coe_bracket_of_module]
    simp

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
⊢ f.fieldRange.toSubfield = (IntermediateField.adjoin F ↑g.range).toSubfield

Tactic:
simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]

Goal state after:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
⊢ (↑f).fieldRange = Subfield.closure (Set.range ⇑(algebraMap F L) ∪ ↑g.range)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ f.fieldRange.toSubfield = (IntermediateField.adjoin F s).toSubfield

Tactic:
simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]

Goal state after:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑f).fieldRange = Subfield.closure (Set.range ⇑(algebraMap F L) ∪ s)
Module: Mathlib.RingTheory.Adjoin.Dimension

Goal state before:
pp: case neg.inr
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
this✝ :
  ∀ (A B : Subalgebra R S) [Free R ↥A] [Free R ↥B],
    ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B) → ¬Module.Finite R ↥A → finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
hA : ¬¬Module.Finite R ↥A
this : finrank R ↥(B ⊔ A) ≤ finrank R ↥B * finrank R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
sup_comm,

Goal state after:
case neg.inr
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
this✝ :
  ∀ (A B : Subalgebra R S) [Free R ↥A] [Free R ↥B],
    ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B) → ¬Module.Finite R ↥A → finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
hA : ¬¬Module.Finite R ↥A
this : finrank R ↥(A ⊔ B) ≤ finrank R ↥B * finrank R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₂ ⟨x✝³ * x✝², ⋯⟩

Tactic:
by convert! congr_arg₂ (· * ·) h₁ h₂ <;> rw [← map_mul] <;> rfl

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝⁷ : Field F
E : Type u_2
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E1 E2 : IntermediateField K L
inst✝¹ : FiniteDimensional K ↥E1
inst✝ : FiniteDimensional K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
this : g.range = (E1 ⊔ E2).toSubalgebra
⊢ FiniteDimensional K ↥(E1 ⊔ E2)

Tactic:
by
    have h : FiniteDimensional K (Subalgebra.toSubmodule g.range) :=
      g.toLinearMap.finiteDimensional_range
    rwa [this] at h

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

Goal state before:
pp: case refine_1
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)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
⊢ ∃ k,
    (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) 0)) = 0

Tactic:
use 0

Goal state after:
case h
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)
F : Module.End R M₃ := ⋯
⊢ (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ 0) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) 0)) = 0
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✝ : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
⊢ ⁅e, m⁆ = 0

Tactic:
by
    suffices 2 • ⁅e, m⁆ = 0 by simpa using this
    rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]

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

Goal state before:
pp: case mem.mem.inr.inl.inr.inr
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
e x y u v : L
t : IsSl2Triple v e u
__spread✝⁻⁰ : Submodule R L := span R {e, u, v}
⊢ ⁅u, v⁆ ∈ span R {e, u, v}

Tactic:
rw [← lie_skew, t.lie_h_f_nsmul, neg_neg]

Goal state after:
case mem.mem.inr.inl.inr.inr
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
e x y u v : L
t : IsSl2Triple v e u
__spread✝⁻⁰ : Submodule R L := span R {e, u, v}
⊢ 2 • u ∈ span R {e, u, v}
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
x : L
hx : x ∈ H
⊢ x ∈ rootSpace H 0

Tactic:
simp only [mem_genWeightSpace, Pi.zero_apply, sub_zero, zero_smul]

Goal state after:
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 : L
hx : x ∈ H
⊢ ∀ (x_1 : ↥H), ∃ k, ((toEnd R (↥H) L) x_1 ^ k) x = 0
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w : M₁
⊢ φ w = ψ w

Tactic:
refine eq_of_sub_eq_zero (b.1 _ ?_)

Goal state after:
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w : M₁
⊢ ∀ (y : M₁), (B (φ w - ψ w)) y = 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case mem.add
ι : 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
x y : L
i : ι
v w : L
hx✝ : v ∈ Submodule.span R (range b.h)
hy✝ : w ∈ Submodule.span R (range b.h)
hv : ⁅v, b.e i⁆ ∈ lieSpan R L (range b.e)
hw : ⁅w, b.e i⁆ ∈ lieSpan R L (range b.e)
⊢ ⁅v + w, b.e i⁆ ∈ lieSpan R L (range b.e)

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

Goal state after:
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
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
⊢ (B (∑ i ∈ s, w i • v i)) (v i) = 0

Tactic:
hs,

Goal state after:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
⊢ (B 0) (v i) = 0
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 := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
⊢ ¬I ≤ J'

Tactic:
intro hIJ'

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'
⊢ False
Module: Mathlib.Algebra.Lie.Weights.Linear

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
χ : L → R
inst✝ : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
a✝ : Nontrivial ↥(shiftedGenWeightSpace R L M χ)
⊢ t • ⁅x, ↑m⁆ - χ x • t • ↑m = t • ↑⁅x, m⁆

Tactic:
smul_comm (χ x),

Goal state after:
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
χ : L → R
inst✝ : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
a✝ : Nontrivial ↥(shiftedGenWeightSpace R L M χ)
⊢ t • ⁅x, ↑m⁆ - t • χ x • ↑m = t • ↑⁅x, m⁆
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v x : α
hx : Fin (count x (v ::ₘ m))
⊢ ((if h : x = v ∧ ↑hx = count v m then none else some ⟨x, ⟨↑hx, ⋯⟩⟩).elim ⟨v, ⟨count v m, ⋯⟩⟩ fun x ↦
      ⟨x.fst, Fin.castLE ⋯ x.snd⟩) =
    ⟨x, hx⟩

Tactic:
split

Goal state after:
case isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v x : α
hx : Fin (count x (v ::ₘ m))
h✝ : x = v ∧ ↑hx = count v m
⊢ (none.elim ⟨v, ⟨count v m, ⋯⟩⟩ fun x ↦ ⟨x.fst, Fin.castLE ⋯ x.snd⟩) = ⟨x, hx⟩

case isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v x : α
hx : Fin (count x (v ::ₘ m))
h✝ : ¬(x = v ∧ ↑hx = count v m)
⊢ ((some ⟨x, ⟨↑hx, ⋯⟩⟩).elim ⟨v, ⟨count v m, ⋯⟩⟩ fun x ↦ ⟨x.fst, Fin.castLE ⋯ x.snd⟩) = ⟨x, hx⟩
Module: Mathlib.Data.Multiset.Fintype

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

Tactic:
split

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

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

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

Tactic:
split <;> simp_all

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

Goal state before:
pp: case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi)) (map (Ideal.Quotient.mk (maxIdeal k)) X) -
      eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi))
        (C ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X ⟨fi.fst, fi.snd⟩))) =
    0

Tactic:
eval_C

Goal state after:
case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi)) (map (Ideal.Quotient.mk (maxIdeal k)) X) -
      (Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X ⟨fi.fst, fi.snd⟩) =
    0
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
⊢ (killingForm R (LieDerivation R L L)).restrict
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L) (ad R L).idealRange).toSubmodule =
    killingForm R ↥(LieIdeal.toLieSubalgebra R (LieDerivation R L L) (ad R L).idealRange)

Tactic:
← LieIdeal.killingForm_eq

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
⊢ killingForm R ↥(ad R L).idealRange =
    killingForm R ↥(LieIdeal.toLieSubalgebra R (LieDerivation R L L) (ad R L).idealRange)
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ (ad R L).range.toSubmodule = ⊤.toSubmodule

Tactic:
apply LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot
    (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl (killingForm_restrict_range_ad_nondegenerate R L)

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule = ⊥
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
D : LieDerivation R L L
⊢ D ∈ (ad R L).range

Tactic:
range_ad_eq_top R L

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
D : LieDerivation R L L
⊢ D ∈ ⊤