mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ mk (y✝¹ ⊔ y✝)

Tactic:
mk_le

Goal state after:
case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝ ≤ y✝¹ ⊔ y✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h.h
x : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝² ≤ mk y✝ → mk y✝¹ ≤ mk y✝ → mk (y✝² ⊔ y✝¹) ≤ mk y✝

Tactic:
mk_le

Goal state after:
case h.h.h
x : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝² ≤ y✝ → y✝¹ ≤ y✝ → y✝² ⊔ y✝¹ ≤ y✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk (y✝¹ ⊓ y✝) ≤ mk y✝¹

Tactic:
mk_le

Goal state after:
case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝¹ ⊓ y✝ ≤ y✝¹
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk (y✝¹ ⊓ y✝) ≤ mk y✝

Tactic:
mk_le

Goal state after:
case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝¹ ⊓ y✝ ≤ y✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h.h
x : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝² ≤ mk y✝¹ → mk y✝² ≤ mk y✝ → mk y✝² ≤ mk (y✝¹ ⊓ y✝)

Tactic:
mk_le

Goal state after:
case h.h.h
x : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝² ≤ y✝¹ → y✝² ≤ y✝ → y✝² ≤ y✝¹ ⊓ y✝
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: l✝ : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m l✝ R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l✝), Commute (A i j) x
k : p
l : l✝
⊢ ∑ x, ∑ x_1, X.vec (x, x_1) * (B x k * A x_1 l) = ∑ x, ∑ x_1, X x_1 x * B x k * A x_1 l

Tactic:
mul_assoc,

Goal state after:
l✝ : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m l✝ R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l✝), Commute (A i j) x
k : p
l : l✝
⊢ ∑ x, ∑ x_1, X.vec (x, x_1) * (B x k * A x_1 l) = ∑ x, ∑ x_1, X x_1 x * (B x k * A x_1 l)
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ ofNat n).det

pp: case negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ -[n+1]).det

Tactic:
· simpa using h.pow n

Goal state after:
case negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ -[n+1]).det
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℤ
⊢ A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹

Tactic:
mul_assoc,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℤ
⊢ A ^ (n - 1) = A ^ (n - 1) * (A * A⁻¹)
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ A * X ^ n.succ * ↑hx'.unit⁻¹ • (X ^ n.succ).adjugate = Y ^ n.succ * (↑hy'.unit⁻¹ • (Y ^ n.succ).adjugate * A)

Tactic:
mul_assoc,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ A * (X ^ n.succ * ↑hx'.unit⁻¹ • (X ^ n.succ).adjugate) = Y ^ n.succ * (↑hy'.unit⁻¹ • (Y ^ n.succ).adjugate * A)
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosSemidef
this : (star (↑U * ↑U⁻¹) * x * ↑U * ↑U⁻¹).PosSemidef
⊢ x.PosSemidef

Tactic:
mul_assoc,

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosSemidef
this : (star (↑U * ↑U⁻¹) * x * (↑U * ↑U⁻¹)).PosSemidef
⊢ x.PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosDef
this : (star (↑U * ↑U⁻¹) * x * ↑U * ↑U⁻¹).PosDef
⊢ x.PosDef

Tactic:
mul_assoc,

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosDef
this : (star (↑U * ↑U⁻¹) * x * (↑U * ↑U⁻¹)).PosDef
⊢ x.PosDef
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: case refine_3
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
n : ℕ
a : R
hna : ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x
⊢ ((aeval f) (X * X ^ n * C a)) x = eval μ (X * X ^ n * C a) • x

Tactic:
mul_assoc,

Goal state after:
case refine_3
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
n : ℕ
a : R
hna : ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x
⊢ ((aeval f) (X * (X ^ n * C a))) x = eval μ (X * (X ^ n * C a)) • x
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * eval r (descPochhammer R k) * (-r + ↑k) = (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))

Tactic:
mul_assoc,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) = (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n : ℕ
v w : Fin (n + 1) → K
i j : Fin (n + 1)
hw : w i ≠ 0
⊢ v i ^ ↑j * w i ^ ↑j.rev * w i ^ ↑j = v i ^ ↑j * w i ^ n

Tactic:
mul_assoc,

Goal state after:
K : Type u_2
inst✝ : Field K
n : ℕ
v w : Fin (n + 1) → K
i j : Fin (n + 1)
hw : w i ≠ 0
⊢ v i ^ ↑j * (w i ^ ↑j.rev * w i ^ ↑j) = v i ^ ↑j * w i ^ n
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
this :
  lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) =
    lieSpan R (↥(prod eι b₁ b₂)) (range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))
⊢ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) = ⊤

Tactic:
have hr : range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) =
        Subtype.val ⁻¹' ( {(b₁.h i, b₂.h (eι i)) | i : ι₁} ∪
                          {(b₁.e i, b₂.e (eι i)) | i : ι₁} ∪
                          {(b₁.f i, b₂.f (eι i)) | i : ι₁} ) := by
      ext; simp [Subtype.ext_iff]

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
this :
  lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) =
    lieSpan R (↥(prod eι b₁ b₂)) (range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))
hr :
  range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) =
    Subtype.val ⁻¹'
      ({x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ∪ {x | ∃ i, (b₁.e i, b₂.e (eι i)) = x} ∪
        {x | ∃ i, (b₁.f i, b₂.f (eι i)) = x})
⊢ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) = ⊤
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = basisDivisor (id x) (id y) + Lagrange.basis {x, y} id y

Tactic:
basis_pair_right hxy,

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = basisDivisor (id x) (id y) + basisDivisor (id y) (id x)
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
⊢ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) = ⊤

Tactic:
suffices lieSpan R (prod eι b₁ b₂) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) =
      lieSpan R (prod eι b₁ b₂)
        (range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) by
    have hr : range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) =
        Subtype.val ⁻¹' ( {(b₁.h i, b₂.h (eι i)) | i : ι₁} ∪
                          {(b₁.e i, b₂.e (eι i)) | i : ι₁} ∪
                          {(b₁.f i, b₂.f (eι i)) | i : ι₁} ) := by
      ext; simp [Subtype.ext_iff]
    rw [this, hr]
    exact lieSpan_lieSpan_coe_preimage
  simp only [union_assoc]
  refine le_antisymm (lieSpan_mono <| by simp) (lieSpan_le.mpr <| union_subset ?_ subset_lieSpan)
  rintro - ⟨i, rfl⟩
  have hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆ := by
    simp [Subtype.ext_iff, (b₁.sl2 i).lie_e_f, (b₂.sl2 (eι i)).lie_e_f]
  rw [hef]
  apply lie_mem
  · exact subset_lieSpan <| mem_union_left _ <| mem_range_self i
  · exact subset_lieSpan <| mem_union_right _ <| mem_range_self i

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs✝ : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
⊢ ((interpolate (insert i (t \ s)) v) r).degree + (Lagrange.basis s v i).degree < ↑(#t)

Tactic:
have H : #t = 1 + (#t - #s) + (#s - 1) := by
      rw [add_assoc, tsub_add_tsub_cancel hst' hs, ← add_tsub_assoc_of_le (hs.trans hst'),
        Nat.succ_add_sub_one, zero_add]

Goal state after:
case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs✝ : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
H : #t = 1 + (#t - #s) + (#s - 1)
⊢ ((interpolate (insert i (t \ s)) v) r).degree + (Lagrange.basis s v i).degree < ↑(#t)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i

Tactic:
by_cases hi' : i ∈ s

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i

case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i
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
x : L
⊢ x ∈ engel R x

Tactic:
simp only [mem_engel_iff]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ∃ n, ((ad R L) x ^ n) x = 0
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
i : σ
⊢ i ∈ d.support → (f i ^ d i).vars ⊆ (f i).vars

Tactic:
_hi

Goal state after:
case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
i : σ
_hi : i ∈ d.support
⊢ (f i ^ d i).vars ⊆ (f i).vars
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case hlc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).leadingCoeff = (X ^ Fintype.card ↥G - 1).leadingCoeff

pp: case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ∀ i ∈ (↑G).toFinset, eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)

Tactic:
· rw [nodal_monic, leadingCoeff_sub_of_degree_lt h, monic_X_pow]

Goal state after:
case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ∀ i ∈ (↑G).toFinset, eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
⊢ nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * ∏ i ∈ s, (x - v i)

Tactic:
mul_assoc,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
⊢ nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * ((x - v i)⁻¹ * ∏ i ∈ s, (x - v 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
⊢ LieIdeal.killingCompl R L ⊤ ≤ radical R L

Tactic:
rw [← LieIdeal.solvable_iff_le_radical]
  refine LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero _ ?_
  intro x hx y _
  rw [LieModule.traceForm_comm]
  exact (LieIdeal.mem_killingCompl R L ⊤).mp hx y (LieSubmodule.mem_top y)

Goal state after:
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 𝒜
κ : Sort u_4
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
⊢ IsHomogeneous 𝒜 (⨅ i, f i)

Tactic:
by
  intro i x hx
  simp only [Ideal.mem_iInf] at hx ⊢
  exact fun j => h _ _ (hx j)

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

Goal state before:
pp: case e'_4
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
r : R
hr : (weight 1) d = n
⊢ n = degree d

Tactic:
Finsupp.degree_eq_weight_one,

Goal state after:
case e'_4
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
r : R
hr : (weight 1) d = n
⊢ n = (weight fun x ↦ 1) d
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case e'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : φ.coeff i ≠ 0
⊢ n * (weight 1) i = n * ∑ i_1 ∈ i.support, i i_1

Tactic:
weight_apply

Goal state after:
case e'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : φ.coeff i ≠ 0
⊢ (n * i.sum fun i c ↦ c • 1 i) = n * ∑ i_1 ∈ i.support, i i_1
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case e'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : φ.coeff i ≠ 0
⊢ (n * i.sum fun i c ↦ c • 1 i) = n * ∑ i_1 ∈ i.support, i i_1

Tactic:
simp_rw [smul_eq_mul, Finsupp.sum, Pi.one_apply, mul_one]

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
⊢ ((eval₂Hom (C.comp f) X) φ).IsHomogeneous n

Tactic:
simpa [one_mul] using hφ.eval₂ _ _ (fun r ↦ isHomogeneous_C _ (f r)) (isHomogeneous_X _)

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

Goal state before:
pp: case mp
M : Type u_2
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
⊢ (m x ≠ 0 → m x • w x = 0) → m x = 0

Tactic:
intro hx
    by_contra hx'
    exact absurd (hw _ _ (hx hx')) hx'

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

Goal state before:
pp: case mpr
M : Type u_2
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
⊢ m x = 0 → m x ≠ 0 → m x • w x = 0

Tactic:
order

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

Goal state before:
pp: case h
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin✝ : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := ⋯
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
hφR : ↑φ.natDegree < #R
r₀ : R
hr₀ : Polynomial.eval r₀ φ ≠ 0
⊢ (eval (Fin.cons r₀ r)) F ≠ 0

Tactic:
eval_eq_eval_mv_eval'

Goal state after:
case h
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin✝ : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
hφR : ↑φ.natDegree < #R
r₀ : R
hr₀ : Polynomial.eval r₀ φ ≠ 0
⊢ Polynomial.eval r₀ (Polynomial.map (eval r) ((finSuccEquiv R N) F)) ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : ι → R
n : ℕ
⊢ span (Set.range x) ^ n =
    Submodule.map (MvPolynomial.aeval x).toLinearMap (MvPolynomial.homogeneousSubmodule ι R 1 ^ n)

Tactic:
Submodule.map_pow,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : ι → R
n : ℕ
⊢ span (Set.range x) ^ n =
    Submodule.map (MvPolynomial.aeval x).toLinearMap (MvPolynomial.homogeneousSubmodule ι R 1) ^ n
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ Bᵀ * Aᵀ * J - Aᵀ * Bᵀ * J = J * -(A * B - B * A)

Tactic:
mul_assoc,

Goal state after:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ Bᵀ * (Aᵀ * J) - Aᵀ * Bᵀ * J = J * -(A * B - B * A)
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ Bᵀ * (Aᵀ * J) - Aᵀ * Bᵀ * J = J * -(A * B - B * A)

Tactic:
mul_assoc,

Goal state after:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ Bᵀ * (Aᵀ * J) - Aᵀ * (Bᵀ * J) = J * -(A * B - B * A)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : Matrix (p ⊕ q) (p ⊕ q) R
⊢ A ∈ ↑(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) ↔
    A ∈ ↑(so (p ⊕ q) R)

Tactic:
rw [indefiniteDiagonal_transform p q R hi]

Goal state after:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : Matrix (p ⊕ q) (p ⊕ q) R
⊢ A ∈ ↑(skewAdjointMatricesLieSubalgebra 1) ↔ A ∈ ↑(so (p ⊕ q) R)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (PD l R)ᵀ * JD l R * PD l R = 2 • S l R

Tactic:
have h : (PD l R)ᵀ * JD l R = Matrix.fromBlocks 1 1 1 (-1) := by
    simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply]

Goal state after:
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
⊢ (PD l R)ᵀ * JD l R * PD l R = 2 • S l R