-- 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.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⟩

Tactic:
congr 2

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 →+ ι
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⟩

Tactic:
dsimp at ih'

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, ⋯⟩ + (decomposeAux f) y =
    (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 : ↥(gradeBy R (⇑f) i)
⊢ (decomposeAux f) ↑x = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) x

Tactic:
obtain ⟨x, hx⟩ := x

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
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]
⊢ ∀ (a : M) (b : R) (f_1 : M →₀ R),
    a ∉ f_1.support →
      b ≠ 0 →
        (∀ (hx : f_1 ∈ gradeBy R (⇑f) i),
            (decomposeAux f) ↑⟨f_1, hx⟩ = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨f_1, hx⟩) →
          ∀ (hx : Finsupp.single a b + f_1 ∈ gradeBy R (⇑f) i),
            (decomposeAux f) ↑⟨Finsupp.single a b + f_1, hx⟩ =
              (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨Finsupp.single a b + f_1, hx⟩

Tactic:
intro m b y hmy hb ih 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
⊢ (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
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:
refine Finsupp.induction x ?_ ?_

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⟩

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]
⊢ ∀ (a : M) (b : R) (f_1 : M →₀ R),
    a ∉ f_1.support →
      b ≠ 0 →
        (∀ (hx : f_1 ∈ gradeBy R (⇑f) i),
            (decomposeAux f) ↑⟨f_1, hx⟩ = (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨f_1, hx⟩) →
          ∀ (hx : Finsupp.single a b + f_1 ∈ gradeBy R (⇑f) i),
            (decomposeAux f) ↑⟨Finsupp.single a b + f_1, hx⟩ =
              (DirectSum.of (fun i => ↥(gradeBy R (⇑f) i)) i) ⟨Finsupp.single a b + f_1, hx⟩

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
⊢ Disjoint (Finsupp.single m b).support y.support

Tactic:
simpa only [Finsupp.support_single_ne_zero _ hb, Finset.disjoint_singleton_left]

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
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✝⟩

Tactic:
obtain ⟨h1, h2⟩ := hmby

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