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,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆
          j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
              (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
                ((of (fun i ↦ ↥(ℒ i)) k) b)⁆
            j) +
        ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
              (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆
            j) -
      ↑((φ i • ⁅(of (fun i ↦ ↥(ℒ i)) k) b, (of (fun i ↦ ↥(ℒ i)) i) a⁆) j)

Tactic:
hM k (of (ℒ ·) k b) (by simp),

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)
⊢ ↑((φ (i + k) • ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆) j) +
      ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆
          j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a, φ k • (of (fun x ↦ ↥(ℒ x)) k) b⁆ j) +
        ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
              (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆
            j) -
      ↑((φ i • ⁅(of (fun i ↦ ↥(ℒ i)) k) b, (of (fun i ↦ ↥(ℒ i)) i) a⁆) j)