-- Mathlib/Algebra/MonoidAlgebra/Grading.lean
theorem decomposeAux_coe {i : ι} (x : gradeBy R f i) :
    decomposeAux f ↑x = DirectSum.of (fun i => gradeBy R f i) i x

Proof state:
case mk.refine_2.intro
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 : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.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 : Finsupp.single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.support ⊆ ⇑f ⁻¹' {f m}
⊢ (decomposeAux f) ↑⟨Finsupp.single m b + y, hmby⟩ =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m b + y, hmby⟩

Tactic:
simp only [map_add, Submodule.coe_mk, decomposeAux_single f m]

Result:
case mk.refine_2.intro
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 : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.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 : Finsupp.single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.support ⊆ ⇑f ⁻¹' {f m}
⊢ (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m b, ⋯⟩ + (decomposeAux f) y =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m b + y, hmby⟩

Proof state:
case mk.refine_2.intro
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 : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.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 : Finsupp.single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.support ⊆ ⇑f ⁻¹' {f m}
⊢ (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m b, ⋯⟩ + (decomposeAux f) y =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m b + y, hmby⟩

Tactic:
let ih' := ih h2

Result:
case mk.refine_2.intro
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 : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.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 : Finsupp.single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.support ⊆ ⇑f ⁻¹' {f m}
ih' : (decomposeAux f) ↑⟨y, h2⟩ = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, h2⟩ := ih h2
⊢ (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m b, ⋯⟩ + (decomposeAux f) y =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m b + y, hmby⟩

Proof state:
case mk.refine_1
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
⊢ ∀ (hx : 0 ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨0, hx⟩ = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨0, hx⟩

Tactic:
intro hx

Result:
case mk.refine_1
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
hx : 0 ∈ gradeBy R (⇑f) i
⊢ (decomposeAux f) ↑⟨0, hx⟩ = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨0, hx⟩

Proof state:
case mk.refine_2.intro
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 : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.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 : Finsupp.single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.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)) ⟨Finsupp.single m b, ⋯⟩ + (decomposeAux f) y =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m b + y, hmby⟩

Tactic:
rw [ih', ← AddMonoidHom.map_add]

Result:
case mk.refine_2.intro
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 : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.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 : Finsupp.single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.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)) (⟨Finsupp.single m b, ⋯⟩ + ⟨y, h2⟩) =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m b + y, hmby⟩

Proof state:
case mk
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
hx : x ∈ gradeBy R (⇑f) i
⊢ (decomposeAux f) ↑⟨x, hx⟩ = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨x, hx⟩

Tactic:
revert hx

Result:
case mk
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
⊢ ∀ (hx : x ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨x, hx⟩ = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨x, hx⟩

Proof state:
case mk.refine_2.intro
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 : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.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 : Finsupp.single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.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)) (⟨Finsupp.single m b, ⋯⟩ + ⟨y, h2⟩) =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m b + y, hmby⟩

Tactic:
apply DirectSum.of_eq_of_gradedMonoid_eq

Result:
case mk.refine_2.intro.h
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 : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.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 : Finsupp.single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.support ⊆ ⇑f ⁻¹' {f m}
ih' : (decomposeAux f) y = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, h2⟩ := ih h2
⊢ GradedMonoid.mk (f m) (⟨Finsupp.single m b, ⋯⟩ + ⟨y, h2⟩) = GradedMonoid.mk (f m) ⟨Finsupp.single m b + y, hmby⟩