mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
y : L₂
f : ι₁ →₀ R
hf : (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) f = (0, y)
this : f = 0
⊢ y = 0

Tactic:
aesop (add simp Prod.ext_iff)

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
i₀ : Fin (n + 1)
hi₀ : w i₀ ≠ 0
⊢ ↑↑(Perm.sign (swap 0 i₀)) ≠ 0

Tactic:
by simp [show 0 ≠ i₀ by rintro rfl; contradiction]

Goal state after:
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
⊢ eval (v i) (∑ i ∈ s, (interpolate (insert i (t \ s)) v) r * Lagrange.basis s v i) = r i

Tactic:
simp_rw [eval_finsetSum, eval_mul]

Goal state after:
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
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₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
L : LieSubalgebra K (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅K⁆ L₁ := (LieHom.fst K L₁ L₂).comp L.incl
p₂ : ↥L →ₗ⁅K⁆ L₂ := (LieHom.snd K L₁ L₂).comp L.incl
disj : Disjoint p₁.ker p₂.ker
I₁ : LieIdeal K L₂ := LieIdeal.map p₂ p₁.ker
this✝ : Nontrivial L₂
this : prod eι b₁ b₂ ≠ ⊤
⊢ I₁ ≠ ⊤

Tactic:
contrapose this

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₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
L : LieSubalgebra K (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅K⁆ L₁ := (LieHom.fst K L₁ L₂).comp L.incl
p₂ : ↥L →ₗ⁅K⁆ L₂ := (LieHom.snd K L₁ L₂).comp L.incl
disj : Disjoint p₁.ker p₂.ker
I₁ : LieIdeal K L₂ := LieIdeal.map p₂ p₁.ker
this✝ : Nontrivial L₂
this : I₁ = ⊤
⊢ prod eι b₁ b₂ = ⊤
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
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:
intro i hi
    rw [eval_nodal_at_node hi]
    replace hi : i ∈ G := by simpa using hi
    obtain ⟨g, rfl⟩ : ∃ g : G, g.val = i := ⟨⟨i, hi⟩, rfl⟩
    simp [← Units.val_pow_eq_pow_val, ← Subgroup.coe_pow G]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (∏ i ∈ insert i s, φ i) (∑ i ∈ insert i s, n i)

Tactic:
simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ IsWeightedHomogeneous w (φ i * ∏ i ∈ s, φ i) (n i + ∑ i ∈ s, n i)
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 : Ideal A
⊢ (homogeneousHull 𝒜 I).toIdeal = ⨆ i, span (⇑(GradedRing.proj 𝒜 i) '' ↑I)

Tactic:
rw [← Ideal.span_iUnion]

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 : Ideal A
⊢ (homogeneousHull 𝒜 I).toIdeal = span (⋃ i, ⇑(GradedRing.proj 𝒜 i) '' ↑I)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, (φ i_1).IsHomogeneous (n i_1)
⊢ (∏ i ∈ insert i s, φ i).IsHomogeneous (∑ i ∈ insert i s, n i)

Tactic:
simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]

Goal state after:
case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, (φ i_1).IsHomogeneous (n i_1)
⊢ (φ i * ∏ i ∈ s, φ i).IsHomogeneous (n i + ∑ i ∈ s, n i)
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 𝒜
x : A
hx : x ∈ 𝒜₊.toAddSubmonoid
⊢ x ∈ ⨆ i, ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)

Tactic:
classical rw [← DirectSum.sum_support_decompose 𝒜 x]

Goal state after:
ι : 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 𝒜
x : A
hx : x ∈ 𝒜₊.toAddSubmonoid
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i) ∈ ⨆ i, ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg.hnc
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬(weight w) x = n

Tactic:
hp zero_coeff

Goal state after:
case neg.hnc
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬m = n
Module: Mathlib.Algebra.Lie.Character

Goal state before:
pp: R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
ψ : Module.Dual R L
x y : L
⊢ ψ.toFun 0 = ψ.toFun y * ψ.toFun x - ψ.toFun y * ψ.toFun x

Tactic:
sub_self,

Goal state after:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
ψ : Module.Dual R L
x y : L
⊢ ψ.toFun 0 = 0
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
x : ChooseBasisIndex R L → R
hx : (eval x) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0
c : ChooseBasisIndex R L →₀ R := Finsupp.equivFunOnFinite.symm x
⊢ ∃ x, φ.IsNilRegular x

Tactic:
use b.repr.symm c

Goal state after:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := ⋯
bₘ : Basis (ChooseBasisIndex R M) R M := ⋯
n : ℕ := ⋯
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
x : ChooseBasisIndex R L → R
hx : (eval x) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0
c : ChooseBasisIndex R L →₀ R := ⋯
⊢ φ.IsNilRegular (b.repr.symm c)
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: case refine_1
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #↑s ≤ f.rank
⊢ ∃ s_1, lift.{v', v} #↑s_1 = lift.{v, v'} #↑s ∧ LinearIndepOn K (⇑f) s_1

Tactic:
refine ⟨g '' s, Cardinal.mk_image_eq_lift _ _ fg.injective, ?_⟩

Goal state after:
case refine_1
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #↑s ≤ f.rank
⊢ LinearIndepOn K (⇑f) (⇑g '' s)
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
⊢ ((lieCharpoly R M x y).coeff i).natDegree ≤ j

Tactic:
rw [← mul_one j, lieCharpoly, coeff_map]

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
⊢ (↑(MvPolynomial.aeval fun i ↦ C (((chooseBasis R L).repr y) i) * X + C (((chooseBasis R L).repr x) i))
        (((↑φ).polyCharpoly (chooseBasis R L)).coeff i)).natDegree ≤
    j * 1
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
⊢ ∃ V U e, IsUnit V ∧ IsUnit U ∧ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e

Tactic:
obtain ⟨L, L', D, hM0⟩ := Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec M

Goal state after:
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
⊢ ∃ V U e, IsUnit V ∧ IsUnit U ∧ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e
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 : ↥(twoCochain R L M)
x : L
x✝¹ : R
x✝ : L
⊢ {
      toFun := fun z ↦
        ⁅x, (a (x✝¹ • x✝)) z⁆ - ⁅x✝¹ • x✝, (a x) z⁆ + ⁅z, (a x) (x✝¹ • x✝)⁆ - (a ⁅x, x✝¹ • x✝⁆) z +
            (a ⁅x, z⁆) (x✝¹ • x✝) -
          (a ⁅x✝¹ • x✝, z⁆) x,
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ •
      { toFun := fun z ↦ ⁅x, (a x✝) z⁆ - ⁅x✝, (a x) z⁆ + ⁅z, (a x) x✝⁆ - (a ⁅x, x✝⁆) z + (a ⁅x, z⁆) x✝ - (a ⁅x✝, z⁆) x,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by ext; simp; abel_nf; simp

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 : ↥(twoCochain R L M)
x✝¹ : R
x✝ : L
⊢ {
      toFun := fun y ↦
        {
          toFun := fun z ↦
            ⁅x✝¹ • x✝, (a y) z⁆ - ⁅y, (a (x✝¹ • x✝)) z⁆ + ⁅z, (a (x✝¹ • x✝)) y⁆ - (a ⁅x✝¹ • x✝, y⁆) z +
                (a ⁅x✝¹ • x✝, z⁆) y -
              (a ⁅y, z⁆) (x✝¹ • x✝),
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ •
      {
        toFun := fun y ↦
          {
            toFun := fun z ↦
              ⁅x✝, (a y) z⁆ - ⁅y, (a x✝) z⁆ + ⁅z, (a x✝) y⁆ - (a ⁅x✝, y⁆) z + (a ⁅x✝, z⁆) y - (a ⁅y, z⁆) x✝,
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by ext; simp; abel_nf; simp

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
x✝¹ : R
x✝ : ↥(twoCochain R L M)
⊢ {
      toFun := fun x ↦
        {
          toFun := fun y ↦
            {
              toFun := fun z ↦
                ⁅x, ((x✝¹ • x✝) y) z⁆ - ⁅y, ((x✝¹ • x✝) x) z⁆ + ⁅z, ((x✝¹ • x✝) x) y⁆ - ((x✝¹ • x✝) ⁅x, y⁆) z +
                    ((x✝¹ • x✝) ⁅x, z⁆) y -
                  ((x✝¹ • x✝) ⁅y, z⁆) x,
              map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ •
      {
        toFun := fun x ↦
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x, (x✝ y) z⁆ - ⁅y, (x✝ x) z⁆ + ⁅z, (x✝ x) y⁆ - (x✝ ⁅x, y⁆) z + (x✝ ⁅x, z⁆) y - (x✝ ⁅y, z⁆) x,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by ext; simp; abel_nf; simp

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✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ GradedMonoid.mk (f (Multiplicative.toAdd (Multiplicative.ofAdd m)))
      (r • ⟨single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩) =
    GradedMonoid.mk (f m) ⟨single m r, ⋯⟩

Tactic:
refine Sigma.subtype_ext rfl ?_

Goal state after:
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ ↑(GradedMonoid.mk (f (Multiplicative.toAdd (Multiplicative.ofAdd m)))
          (r • ⟨single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩)).snd =
    ↑(GradedMonoid.mk (f m) ⟨single m r, ⋯⟩).snd
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.coeff.support
ih :
  ∀ (hx : y ∈ gradeBy R (⇑f) (f m)),
    (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, hx⟩
hmby : single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.coeff.support ⊆ ⇑f ⁻¹' {f m}
ih' : (decomposeAux f) y = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, h2⟩ := ih h2
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b, ⋯⟩ +
      (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, h2⟩ =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b + y, hmby⟩

Tactic:
← map_add

Goal state after:
case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.coeff.support
ih :
  ∀ (hx : y ∈ gradeBy R (⇑f) (f m)),
    (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, hx⟩
hmby : single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.coeff.support ⊆ ⇑f ⁻¹' {f m}
ih' : (decomposeAux f) y = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, h2⟩ := ih h2
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) (⟨single m b, ⋯⟩ + ⟨y, h2⟩) =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b + y, hmby⟩
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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ (ofProd c)
      (⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).1⁆,
        (↑↑c ((ofProd c).symm (x + y)).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).2⁆ -
          ⁅((ofProd c).symm z).1, ((ofProd c).symm (x + y)).2⁆) =
    (ofProd c)
        (⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆) +
      (ofProd c)
        (⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆)

Tactic:
rw [← of_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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ (ofProd c)
      (⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).1⁆,
        (↑↑c ((ofProd c).symm (x + y)).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).2⁆ -
          ⁅((ofProd c).symm z).1, ((ofProd c).symm (x + y)).2⁆) =
    (ofProd c)
      ((⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆) +
        (⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆))
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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ (ofProd c)
      (⁅((ofProd c).symm x).1, ((ofProd c).symm (y + z)).1⁆,
        (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm (y + z)).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm (y + z)).2⁆ -
          ⁅((ofProd c).symm (y + z)).1, ((ofProd c).symm x).2⁆) =
    (ofProd c)
        (⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ -
            ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆) +
      (ofProd c)
        (⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆)

Tactic:
rw [← of_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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ (ofProd c)
      (⁅((ofProd c).symm x).1, ((ofProd c).symm (y + z)).1⁆,
        (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm (y + z)).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm (y + z)).2⁆ -
          ⁅((ofProd c).symm (y + z)).1, ((ofProd c).symm x).2⁆) =
    (ofProd c)
      ((⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ -
            ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆) +
        (⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆))