-- 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_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:
symm

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

Tactic:
subst this

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}
⊢ (decomposeAux f) ↑⟨Finsupp.single m b + y, hmby⟩ =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m b + y, hmby⟩

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

Tactic:
rwa [Finsupp.support_single_ne_zero _ hb, Finset.coe_singleton, Set.singleton_subset_iff]
  at h1

Result:
no goals

Proof state:
case mk.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 →+ ι
i : ι
x : R[M]
m : M
b : R
y : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
ih : ∀ (hx : y ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩
hmby : Finsupp.single m b + y ∈ gradeBy R (⇑f) i
this : Disjoint (Finsupp.single m b).support y.support
⊢ (decomposeAux f) ↑⟨Finsupp.single m b + y, hmby⟩ =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨Finsupp.single m b + y, hmby⟩

Tactic:
rw [mem_gradeBy_iff, Finsupp.support_add_eq this, Finset.coe_union, Set.union_subset_iff]
  at hmby

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

Tactic:
exact AddMonoidHom.map_zero _

Result:
no goals

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

Tactic:
have : f m = i := by
  rwa [Finsupp.support_single_ne_zero _ hb, Finset.coe_singleton, Set.singleton_subset_iff]
    at h1

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

Proof state:
case mk.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 →+ ι
i : ι
x : R[M]
m : M
b : R
y : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
ih : ∀ (hx : y ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩
hmby : Finsupp.single m b + y ∈ gradeBy R (⇑f) i
⊢ (decomposeAux f) ↑⟨Finsupp.single m b + y, hmby⟩ =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨Finsupp.single m b + y, hmby⟩

Tactic:
have : Disjoint (Finsupp.single m b).support y.support := by
  simpa only [Finsupp.support_single_ne_zero _ hb, Finset.disjoint_singleton_left]

Result:
case mk.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 →+ ι
i : ι
x : R[M]
m : M
b : R
y : M →₀ R
hmy : m ∉ y.support
hb : b ≠ 0
ih : ∀ (hx : y ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩
hmby : Finsupp.single m b + y ∈ gradeBy R (⇑f) i
this : Disjoint (Finsupp.single m b).support y.support
⊢ (decomposeAux f) ↑⟨Finsupp.single m b + y, hmby⟩ =
    (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨Finsupp.single m b + y, hmby⟩