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

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R (M₁ × M₂) := b₁.prod b₂
⊢ ((toMatrix b b) (f₁.prodMap f₂)).charpoly = ((toMatrix b₁ b₁) f₁).charpoly * ((toMatrix b₂ b₂) f₂).charpoly

Tactic:
toMatrix_prodMap b₁ b₂ f₁ f₂,

Goal state after:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R (M₁ × M₂) := b₁.prod b₂
⊢ (fromBlocks ((toMatrix b₁ b₁) f₁) 0 0 ((toMatrix b₂ b₂) f₂)).charpoly =
    ((toMatrix b₁ b₁) f₁).charpoly * ((toMatrix b₂ b₂) f₂).charpoly
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
⊢ weightedHomogeneousSubmodule R w m = AddMonoidAlgebra.supported R R {d | (weight w) d = m}

Tactic:
ext x
  simp [IsWeightedHomogeneous]
  simp [AddMonoidAlgebra.mem_supported, Set.subset_def, MvPolynomial, coeff]

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✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i) ∈ homogeneousCore' 𝒜 I

Tactic:
exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, isHomogeneousElem_coe _⟩, h _ hx, rfl⟩

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 𝒜
i : ι
r : A
hr : r = 0
⊢ ↑(((decompose 𝒜) r) i) ∈ ⊥

Tactic:
rw [hr, decompose_zero, zero_apply]

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : r = 0
⊢ ↑0 ∈ ⊥
Module: Mathlib.Algebra.Lie.CartanCriterion

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

Tactic:
by
    rwa [← solvable_iff_equiv_solvable LieSubalgebra.topEquiv (R := R)]

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✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
⊢ ↑(((decompose 𝒜) r) i) ∈ RingHom.ker (projZeroRingHom 𝒜)

Tactic:
by
    change (decompose 𝒜 (decompose 𝒜 r _ : A) 0 : A) = 0
    by_cases h : i = 0
    · rw [h, hr, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
    · rw [decompose_of_mem_ne 𝒜 (SetLike.coe_mem _) h]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
s : σ →₀ ℕ
hs : s ∈ φ.support
⊢ n = ∑ i ∈ s.support, s i

Tactic:
by
  simp [← hφ <| mem_support_iff.mp hs, ← degree_apply, degree_eq_weight_one, Pi.one_def]

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

Goal state before:
pp: case h.inr
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
⊢ d i = 0 i

Tactic:
Pi.zero_apply

Goal state after:
case h.inr
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
⊢ d i = 0
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : DecidableEq ιM
bₘ : Basis ιM R M
⊢ φ.polyCharpoly b = Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM)

Tactic:
polyCharpoly,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : DecidableEq ιM
bₘ : Basis ιM R M
⊢ φ.polyCharpolyAux b (Free.chooseBasis R M) =
    Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM)
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : Nontrivial R
⊢ (φ.polyCharpoly b).natDegree = finrank R M

Tactic:
polyCharpoly,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : Nontrivial R
⊢ (φ.polyCharpolyAux b (Free.chooseBasis R M)).natDegree = finrank R M
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ((φ.polyCharpoly b).coeff i).IsHomogeneous j

Tactic:
polyCharpoly,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ((φ.polyCharpolyAux b (Free.chooseBasis R M)).coeff i).IsHomogeneous j
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
φ : L →ₗ[R] End R M
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
x : L
⊢ Polynomial.map (eval ⇑(b.repr x)) (φ.polyCharpoly b) = charpoly (φ x)

Tactic:
polyCharpoly,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
φ : L →ₗ[R] End R M
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
x : L
⊢ Polynomial.map (eval ⇑(b.repr x)) (φ.polyCharpolyAux b (Free.chooseBasis R M)) = charpoly (φ x)
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
φ : L →ₗ[R] End R M
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
x : L
i : ℕ
⊢ (eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff i) = (charpoly (φ x)).coeff i

Tactic:
polyCharpoly,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
φ : L →ₗ[R] End R M
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
x : L
i : ℕ
⊢ (eval ⇑(b.repr x)) ((φ.polyCharpolyAux b (Free.chooseBasis R M)).coeff i) = (charpoly (φ x)).coeff i
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
H : (φ.polyCharpoly b).coeff k = 0
⊢ (φ.polyCharpoly b').coeff k = 0

Tactic:
polyCharpoly,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
H : (φ.polyCharpolyAux b (Free.chooseBasis R M)).coeff k = 0
⊢ (φ.polyCharpolyAux b' (Free.chooseBasis R M)).coeff k = 0
Module: Mathlib.LinearAlgebra.Matrix.Diagonal

Goal state before:
pp: m : Type u_1
inst✝³ : Fintype m
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hIJ : IsCompl {i | w i ≠ 0} {i | w i = 0}
B₁ : ⨆ i ∈ {i | w i ≠ 0}, (single K (fun x ↦ K) i).range = ⨅ i ∈ {i | w i = 0}, (proj i).ker
⊢ Module.rank K ↥(⨅ i ∈ {i | w i = 0}, (proj i).ker) = Module.rank K ({ i // w i ≠ 0 } → K)

Tactic:
exact iInfKerProjEquiv K (fun _ ↦ K) hIJ.disjoint hIJ.codisjoint.top_le |>.rank_eq

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ fromBlocks 0ᵀ 1ᵀ (-1)ᵀ 0ᵀ = fromBlocks (-1 • 0) (-1 • -1) (-1 • 1) (-1 • 0)

Tactic:
Matrix.transpose_zero,

Goal state after:
l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ fromBlocks 0 1ᵀ (-1)ᵀ 0 = fromBlocks (-1 • 0) (-1 • -1) (-1 • 1) (-1 • 0)
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]
  rw [h, PD, s_as_blocks, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul]
  simp [two_smul]

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

Goal state before:
pp: m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
a✝ : Nontrivial R
⊢ A.det • (B * 1) = A.det • B

Tactic:
Matrix.mul_one

Goal state after:
m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
a✝ : Nontrivial R
⊢ A.det • B = A.det • B
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
⊢ ∀ {a b : Derivation R A' A' × Derivation R A A},
    a ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2} →
      b ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2} →
        a + b ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
⊢ ∀ (c : R) {x : Derivation R A' A' × Derivation R A A},
    x ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2} →
      c • x ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝³ x✝² : Derivation R A A
z x✝¹ x✝ : A ⊗[R] L
hx :
  { toFun := ⇑(LinearMap.rTensor L ↑⁅x✝³, x✝²⁆), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } x✝¹ =
    ⁅{ toFun := ⇑(LinearMap.rTensor L ↑x✝³), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ },
        { toFun := ⇑(LinearMap.rTensor L ↑x✝²), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }⁆
      x✝¹
hy :
  { toFun := ⇑(LinearMap.rTensor L ↑⁅x✝³, x✝²⁆), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } x✝ =
    ⁅{ toFun := ⇑(LinearMap.rTensor L ↑x✝³), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ },
        { toFun := ⇑(LinearMap.rTensor L ↑x✝²), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }⁆
      x✝
⊢ { toFun := ⇑(LinearMap.rTensor L ↑⁅x✝³, x✝²⁆), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } (x✝¹ + x✝) =
    ⁅{ toFun := ⇑(LinearMap.rTensor L ↑x✝³), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ },
        { toFun := ⇑(LinearMap.rTensor L ↑x✝²), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }⁆
      (x✝¹ + x✝)

Tactic:
simp_all

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝³ x✝² : Derivation R A A
z x✝¹ x✝ : A ⊗[R] L
hx :
  (LinearMap.rTensor L ⁅↑x✝³, ↑x✝²⁆) x✝¹ =
    (LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝¹) -
      (LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝¹)
hy :
  (LinearMap.rTensor L ⁅↑x✝³, ↑x✝²⁆) x✝ =
    (LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝) -
      (LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝)
⊢ (LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝¹) -
        (LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝¹) +
      ((LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝) -
        (LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝)) =
    (LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝¹) +
        (LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝) -
      ((LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝¹) +
        (LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝))
Module: Mathlib.Algebra.Lie.DirectSum

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

Tactic:
toAddMonoid_of,

Goal state after:
case inl
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
i : ι
y x : L i
⊢ (↑(f i)).toAddMonoidHom ⁅x, y⁆ = ⁅(↑(f i)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom y⁆
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
M : Matrix (l ⊕ l) (l ⊕ l) R
hM : M ∈ symplecticGroup l R
A : Matrix l l R := M.toBlocks₁₁
B : Matrix l l R := M.toBlocks₁₂
C : Matrix l l R := M.toBlocks₂₁
D : Matrix l l R := M.toBlocks₂₂
X : Matrix l l R
hX_symm : X.IsSymm
hA_isUnit : IsUnit (M.toBlocks₁₁ + X * M.toBlocks₂₁).det
Lx_mul : fromBlocks 1 X 0 1 * M = fromBlocks (A + X * C) (B + X * D) C D
⊢ fromBlocks 1 X 0 1 ∈ symplecticGroup l R

Tactic:
simp [mem_iff, fromBlocks_transpose, hX_symm.eq, J, fromBlocks_multiply]

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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
x✝ : L
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [UniversalEnvelopingAlgebra]

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x : X
⊢ ((lift R) f) (of R x) = f x

Tactic:
by
  rw [← @Function.comp_apply _ _ _ (lift R f) (of R) x, of_comp_lift]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : ι
a b : R[M]
ha : a ∈ gradeBy R (⇑f) i
hb : b ∈ gradeBy R (⇑f) j
c : M
hc : c ∈ (a * b).coeff.support
⊢ f c = i + j

Tactic:
obtain ⟨ma, hma, mb, hmb, rfl⟩ : ∃ y ∈ a.coeff.support, ∃ z ∈ b.coeff.support, y + z = c :=
      Finset.mem_add.1 <| support_coeff_mul_subset a b hc
    rw [map_add, ha ma hma, hb mb hmb]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ x ∈ a✝

Tactic:
simp_all

Goal state after:
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⁆
⊢ ⁅Exists.choose h x, E.toKer (E.toKer.symm ⁅Exists.choose h y, E.toKer m⁆)⁆ =
    ⁅Exists.choose h ⁅x, y⁆, E.toKer m⁆ + ⁅Exists.choose h y, E.toKer (E.toKer.symm ⁅Exists.choose h x, E.toKer m⁆)⁆

Tactic:
LieEquiv.apply_symm_apply,

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⁆
⊢ ⁅Exists.choose h x, ⁅Exists.choose h y, E.toKer m⁆⁆ =
    ⁅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.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⁆
⊢ ⁅Exists.choose h x, ⁅Exists.choose h y, E.toKer m⁆⁆ =
    ⁅Exists.choose h ⁅x, y⁆, E.toKer m⁆ + ⁅Exists.choose h y, E.toKer (E.toKer.symm ⁅Exists.choose h x, E.toKer m⁆)⁆

Tactic:
LieEquiv.apply_symm_apply,

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⁆
⊢ ⁅Exists.choose h x, ⁅Exists.choose h y, E.toKer m⁆⁆ =
    ⁅Exists.choose h ⁅x, y⁆, E.toKer m⁆ + ⁅Exists.choose h y, ⁅Exists.choose h x, E.toKer m⁆⁆
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : ¬orderOf (p.cycleOf x) ∣ n.succ
⊢ n + 1 = m + 1

Tactic:
have hm' : ¬orderOf (p.cycleOf x) ∣ m.succ := Nat.not_dvd_of_pos_of_lt m.zero_lt_succ hm

Goal state after:
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : ¬orderOf (p.cycleOf x) ∣ n.succ
hm' : ¬orderOf (p.cycleOf x) ∣ m.succ
⊢ n + 1 = m + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case intro.refine_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
val✝ : Fintype α
x : α
hx : f x ≠ x
hy : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ ∀ (y : Cycle α), (fun s ↦ ∃ (h : s.Nodup), s.formPerm h = f) y → y = ↑(f.toList x)

Tactic:
rintro ⟨l⟩ ⟨hn, rfl⟩

Goal state after:
case intro.refine_2.mk
α : 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
⊢ Quot.mk (⇑(IsRotated.setoid α)) l = ↑((Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).toList x)