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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : Module.End R M
⊢ f ∈ LieSubalgebra.map e.lieConj.toLieHom (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e)) ↔
    f ∈ skewAdjointLieSubalgebra B

Tactic:
simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]

Goal state after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : Module.End R M
⊢ e.lieConj.toLinearEquiv.symm f ∈ (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e)).toSubmodule ↔
    f ∈ skewAdjointLieSubalgebra B
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
P : Matrix n n R
h : Invertible P
A : Matrix n n R
this : (P.lieConj h) A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
⊢ A ∈ LieSubalgebra.map (P.lieConj h).symm.toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)

Tactic:
simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]

Goal state after:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : Invertible P
A : Matrix n n R
this : (P.lieConj h) A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
⊢ (P.lieConj h).symm.toLinearEquiv.symm A ∈ (skewAdjointMatricesLieSubalgebra J).toSubmodule ↔
    A ∈ skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)
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 ∈ {A | A * J l R * Aᵀ = J l R}
hb : b ∈ {A | A * J l R * Aᵀ = J l R}
⊢ a * b ∈ {A | A * J l R * Aᵀ = J l R}

Tactic:
simp only [Set.mem_ofPred_eq, transpose_mul] at *
    rw [← Matrix.mul_assoc, a.mul_assoc, a.mul_assoc, hb]
    exact ha

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

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
⊢ (Aᵀ * A).mulVecLin.ker = A.mulVecLin.ker

Tactic:
ext x
  simp only [LinearMap.mem_ker, mulVecLin_apply, ← mulVec_mulVec]
  constructor
  · intro h
    replace h := congr_arg (dotProduct x) h
    rwa [dotProduct_mulVec, dotProduct_zero, vecMul_transpose, dotProduct_self_eq_zero] at h
  · intro h
    rw [h, mulVec_zero]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
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
a : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ ⁅x, ⁅y, a z⁆⁆ - ⁅x, ⁅z, a y⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - (⁅y, ⁅x, a z⁆⁆ - ⁅y, ⁅z, a x⁆⁆ - ⁅y, a ⁅x, z⁆⁆) +
            (⁅z, ⁅x, a y⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - ⁅z, a ⁅x, y⁆⁆) -
          (⁅x, ⁅y, a z⁆⁆ - ⁅y, ⁅x, a z⁆⁆ - ⁅z, a ⁅x, y⁆⁆ - a (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)) +
        (⁅x, ⁅z, a y⁆⁆ - ⁅z, ⁅x, a y⁆⁆ - ⁅y, a ⁅x, z⁆⁆ - a (⁅x, ⁅z, y⁆⁆ - ⁅z, ⁅x, y⁆⁆)) -
      (⁅y, ⁅z, a x⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - a (⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆)) =
    0

Tactic:
leibniz_lie y x,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
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
a : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ ⁅x, ⁅y, a z⁆⁆ - ⁅x, ⁅z, a y⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆ - ⁅y, ⁅z, a x⁆⁆ - ⁅y, a ⁅x, z⁆⁆) +
            (⁅z, ⁅x, a y⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - ⁅z, a ⁅x, y⁆⁆) -
          (⁅x, ⁅y, a z⁆⁆ - (⁅⁅y, x⁆, a z⁆ + ⁅x, ⁅y, a z⁆⁆) - ⁅z, a ⁅x, y⁆⁆ - a (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)) +
        (⁅x, ⁅z, a y⁆⁆ - ⁅z, ⁅x, a y⁆⁆ - ⁅y, a ⁅x, z⁆⁆ - a (⁅x, ⁅z, y⁆⁆ - ⁅z, ⁅x, y⁆⁆)) -
      (⁅y, ⁅z, a x⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - ⁅x, a ⁅y, z⁆⁆ - a (⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆)) =
    0
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (((coeLinearMap fun i ↦ Submodule.baseChange S (ℳ i)) ∘ₗ lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ∘ₗ
        ↑(directSumRight R S S fun i ↦ ↥(ℳ i))) ∘ₗ
      ↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) =
    LinearMap.id

Tactic:
← LinearEquiv.eq_comp_toLinearMap_symm

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ ((coeLinearMap fun i ↦ Submodule.baseChange S (ℳ i)) ∘ₗ lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ∘ₗ
      ↑(directSumRight R S S fun i ↦ ↥(ℳ i)) =
    LinearMap.id ∘ₗ ↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)).symm
Module: Mathlib.Algebra.Lie.Graded

Goal state before:
pp: case hadd.hadd.e_a
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j i : ι
a : ↥(ℒ i)
f✝ : ⨁ (i : ι), ↥(ℒ i)
a✝³ : f✝ i = 0
a✝² : a ≠ 0
k : ι
b : ↥(ℒ k)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f k = 0
a✝ : b ≠ 0
ih :
  ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
          ⁅(of (fun i ↦ ↥(ℒ i)) i) a, f⁆)
        j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆
          j) -
      ↑(⁅f, φ i • (of (fun x ↦ ↥(ℒ x)) i) a⁆ j)
this : (decompose ℒ).symm ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆ ∈ ℒ (i + k)
⊢ ↑((φ (i + k) • ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆) j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a, φ k • (of (fun x ↦ ↥(ℒ x)) k) b⁆ j) -
      ↑((φ i • -⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun x ↦ ↥(ℒ x)) k) b⁆) j)

Tactic:
add_comm i k,

Goal state after:
case hadd.hadd.e_a
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j i : ι
a : ↥(ℒ i)
f✝ : ⨁ (i : ι), ↥(ℒ i)
a✝³ : f✝ i = 0
a✝² : a ≠ 0
k : ι
b : ↥(ℒ k)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f k = 0
a✝ : b ≠ 0
ih :
  ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
          ⁅(of (fun i ↦ ↥(ℒ i)) i) a, f⁆)
        j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆
          j) -
      ↑(⁅f, φ i • (of (fun x ↦ ↥(ℒ x)) i) a⁆ j)
this : (decompose ℒ).symm ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆ ∈ ℒ (i + k)
⊢ ↑((φ (k + i) • ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆) j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a, φ k • (of (fun x ↦ ↥(ℒ x)) k) b⁆ j) -
      ↑((φ i • -⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun x ↦ ↥(ℒ x)) k) b⁆) j)
Module: Mathlib.Algebra.Lie.Graded

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
x y : L
⊢ { toFun := fun x ↦ (decomposeLinearEquiv ℒ).symm ((ofGradingSum ℒ φ) ((decomposeLinearEquiv ℒ) x)), map_add' := ⋯,
        map_smul' := ⋯ }
      ⁅x, y⁆ =
    ⁅x,
        { toFun := fun x ↦ (decomposeLinearEquiv ℒ).symm ((ofGradingSum ℒ φ) ((decomposeLinearEquiv ℒ) x)),
            map_add' := ⋯, map_smul' := ⋯ }
          y⁆ -
      ⁅y,
        { toFun := fun x ↦ (decomposeLinearEquiv ℒ).symm ((ofGradingSum ℒ φ) ((decomposeLinearEquiv ℒ) x)),
            map_add' := ⋯, map_smul' := ⋯ }
          x⁆

Tactic:
by simp [decomposeLinearEquiv_apply, decomposeLinearEquiv_symm_apply]

Goal state after:
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
⊢ HasCentralRadical k L ∧ ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ k ∙ LinearMap.id

Tactic:
have _i := nontrivial_of_isIrreducible k L M

Goal state after:
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
⊢ HasCentralRadical k L ∧ ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ k ∙ LinearMap.id
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
⊢ E.toKer.symm ⁅Exists.choose h (x + y), E.toKer m⁆ =
    E.toKer.symm ⁅Exists.choose h x, E.toKer m⁆ + E.toKer.symm ⁅Exists.choose h y, E.toKer m⁆

Tactic:
← map_add,

Goal state after:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
⊢ E.toKer.symm ⁅Exists.choose h (x + y), E.toKer m⁆ =
    E.toKer.symm (⁅Exists.choose h x, E.toKer m⁆ + ⁅Exists.choose h y, E.toKer m⁆)
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
aux : ∀ (z : ↥E.proj.ker), ⁅⁅Exists.choose h x, Exists.choose h y⁆, z⁆ = ⁅Exists.choose h ⁅x, y⁆, z⁆
⊢ E.toKer.symm ⁅Exists.choose h x, E.toKer (E.toKer.symm ⁅Exists.choose h y, E.toKer m⁆)⁆ =
    E.toKer.symm ⁅Exists.choose h ⁅x, y⁆, E.toKer m⁆ +
      E.toKer.symm ⁅Exists.choose h y, E.toKer (E.toKer.symm ⁅Exists.choose h x, E.toKer m⁆)⁆

Tactic:
← map_add,

Goal state after:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
aux : ∀ (z : ↥E.proj.ker), ⁅⁅Exists.choose h x, Exists.choose h y⁆, z⁆ = ⁅Exists.choose h ⁅x, y⁆, z⁆
⊢ E.toKer.symm ⁅Exists.choose h x, E.toKer (E.toKer.symm ⁅Exists.choose h y, E.toKer m⁆)⁆ =
    E.toKer.symm
      (⁅Exists.choose h ⁅x, y⁆, E.toKer m⁆ + ⁅Exists.choose h y, E.toKer (E.toKer.symm ⁅Exists.choose h x, E.toKer m⁆)⁆)
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
i : ℕ
ih : ∀ m < i, ∀ ⦃x : V⦄, x ∈ U' m → ∃ k, (T χ w ^ k) x = 0
x : V
hx : x ∈ U' i
hi : i ≠ 0
j : ℕ
hj : j < i
hj' : Submodule.map (T χ w) (U' i) ≤ U' j
k : ℕ
hk : (T χ w ^ k) ((T χ w) x) = 0
⊢ (T χ w ^ k) ((T χ w) x) = 0

Tactic:
hk

Goal state after:
case h
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
i : ℕ
ih : ∀ m < i, ∀ ⦃x : V⦄, x ∈ U' m → ∃ k, (T χ w ^ k) x = 0
x : V
hx : x ∈ U' i
hi : i ≠ 0
j : ℕ
hj : j < i
hj' : Submodule.map (T χ w) (U' i) ≤ U' j
k : ℕ
hk : (T χ w ^ k) ((T χ w) x) = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing M
inst✝ : LieAlgebra R M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x✝¹ x✝ : L
⊢ E.toKer.symm ⟨s₁ (x✝¹ + x✝) - s₂ (x✝¹ + x✝), ⋯⟩ = E.toKer.symm ⟨s₁ x✝¹ - s₂ x✝¹, ⋯⟩ + E.toKer.symm ⟨s₁ x✝ - s₂ x✝, ⋯⟩

Tactic:
← map_add,

Goal state after:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing M
inst✝ : LieAlgebra R M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x✝¹ x✝ : L
⊢ E.toKer.symm ⟨s₁ (x✝¹ + x✝) - s₂ (x✝¹ + x✝), ⋯⟩ = E.toKer.symm (⟨s₁ x✝¹ - s₂ x✝¹, ⋯⟩ + ⟨s₁ x✝ - s₂ x✝, ⋯⟩)
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case intro.refine_2.mk.refine_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
⊢ x ∈ l

Tactic:
· rw [← mem_toFinset]
      refine support_formPerm_le l ?_
      simpa using hx

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

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
this : ⁅((k ∙ z).projection ↑A ⋯) x, v⁆ = (c • e (π₂ x)) • v
⊢ ⁅x, v⁆ = (χ₀ ∘ₗ π₁ + c • ↑e ∘ₗ π₂) x • v

Tactic:
calc ⁅x, v⁆
          = ⁅π₁ x, v⁆ + ⁅projection _ _ hA.symm x, v⁆ := congr(⁅$hπ.symm, v⁆) ▸ add_lie _ _ _
        _ = χ₀ (π₁ x) • v + (c • e (π₂ x)) • v    := by rw [hv' (π₁ x), this]
        _ = _ := by simp [add_smul]

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) ↔ eval q ((monomial E.order) 1 - ∑ i, (monomial ↑i) (E.coeffs i)) = 0

Tactic:
Polynomial.eval

Goal state after:
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) ↔ eval₂ (RingHom.id R) q ((monomial E.order) 1 - ∑ i, (monomial ↑i) (E.coeffs i)) = 0
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
⊢ IsFractional S I

Tactic:
by
  obtain ⟨a, a_mem, ha⟩ := J.isFractional
  use a, a_mem
  intro b b_mem
  exact ha b (hIJ b_mem)

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ (Algebra.linearMap R₁ K).range ≤ 1

Tactic:
one_eq_range

Goal state after:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I ≠ ⊥
i : K
hi : i ∈ I
⊢ (Algebra.linearMap R₁ K).range ≤ (Algebra.linearMap R₁ K).range
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
β : ↥LieSubalgebra.root
hβ : β ∈ I.rootSet
⊢ corootSubmodule ↑β ≤ sl2SubmoduleOfRoot ⋯

Tactic:
rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_right

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
⊢ I / J = I * J⁻¹

Tactic:
obtain rfl | hJ := eq_or_ne J 0

Goal state after:
case inl
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J I : FractionalIdeal A⁰ K
⊢ I / 0 = I * 0⁻¹

case inr
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I / J = I * J⁻¹
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ (FractionRing A)
hI : I ≠ ⊥
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J
h₂ : I * (spanSingleton A⁰ ((algebraMap A (FractionRing A)) a) * (↑J)⁻¹) = 1
⊢ I * I⁻¹ = 1

Tactic:
mul_inv_cancel_iff

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ (FractionRing A)
hI : I ≠ ⊥
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J
h₂ : I * (spanSingleton A⁰ ((algebraMap A (FractionRing A)) a) * (↑J)⁻¹) = 1
⊢ ∃ J, I * J = 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mp
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
hx' : z • x ∈ spanSingleton S x
h : (IsLocalization.map P' (RingHom.id R) ⋯) (z • x) ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z_1, z_1 • (IsLocalization.map P' (RingHom.id R) ⋯) x = (IsLocalization.map P' (RingHom.id R) ⋯) (z • x)

Tactic:
use z

Goal state after:
case h
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
hx' : z • x ∈ spanSingleton S x
h : (IsLocalization.map P' (RingHom.id R) ⋯) (z • x) ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ z • (IsLocalization.map P' (RingHom.id R) ⋯) x = (IsLocalization.map P' (RingHom.id R) ⋯) (z • x)
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : y ∈ R₁⁰
⊢ spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔ Ideal.span {x} * I = Ideal.span {y} * J

Tactic:
by
  have :
    spanSingleton R₁⁰ (IsLocalization.mk' _ (1 : R₁) ⟨y, hy⟩) *
        spanSingleton R₁⁰ (algebraMap R₁ K y) =
      1 := by
    rw [spanSingleton_mul_spanSingleton, mul_comm, ← IsLocalization.mk'_eq_mul_mk'_one,
      IsLocalization.mk'_self, spanSingleton_one]
  let y' : (FractionalIdeal R₁⁰ K)ˣ := Units.mkOfMulEqOne _ _ this
  have coe_y' : ↑y' = spanSingleton R₁⁰ (IsLocalization.mk' K (1 : R₁) ⟨y, hy⟩) := rfl
  refine Iff.trans ?_ (y'.mul_right_inj.trans coeIdeal_inj)
  rw [coe_y', coeIdeal_mul, coeIdeal_span_singleton, coeIdeal_mul, coeIdeal_span_singleton, ←
    mul_assoc, spanSingleton_mul_spanSingleton, ← mul_assoc, spanSingleton_mul_spanSingleton,
    mul_comm (mk' _ _ _), ← IsLocalization.mk'_eq_mul_mk'_one, mul_comm (mk' _ _ _), ←
    IsLocalization.mk'_eq_mul_mk'_one, IsLocalization.mk'_self, spanSingleton_one, one_mul]

Goal state after: