case mk
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
hx : x ∈ gradeBy R (↑f) i
⊢ ↑(decomposeAux f) ↑{ val := x, property := hx } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := x, property := hx }
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : { x // x ∈ gradeBy R (↑f) i }
⊢ ↑(decomposeAux f) ↑x = ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) x
obtain ⟨x, hx⟩ := x
case mk
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
⊢ ∀ (hx : x ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := x, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := x, property := hx }
case mk
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
hx : x ∈ gradeBy R (↑f) i
⊢ ↑(decomposeAux f) ↑{ val := x, property := hx } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := x, property := hx }
revert hx
case mk.refine'_1
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
⊢ ∀ (hx : 0 ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := 0, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := 0, property := hx }

case mk.refine'_2
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := f_1, property := hx } =
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := f_1, property := hx }) →
          ∀ (hx : Finsupp.single a b + f_1 ∈ gradeBy R (↑f) i),
            ↑(decomposeAux f) ↑{ val := Finsupp.single a b + f_1, property := hx } =
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i)
                { val := Finsupp.single a b + f_1, property := hx }
case mk
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
⊢ ∀ (hx : x ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := x, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := x, property := hx }
refine' Finsupp.induction x _ _
case mk.refine'_1
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
hx : 0 ∈ gradeBy R (↑f) i
⊢ ↑(decomposeAux f) ↑{ val := 0, property := hx } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := 0, property := hx }
case mk.refine'_1
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
⊢ ∀ (hx : 0 ∈ gradeBy R (↑f) i),
    ↑(decomposeAux f) ↑{ val := 0, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := 0, property := hx }
intro hx
case mk.refine'_1
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
hx : 0 ∈ gradeBy R (↑f) i
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := 0, property := hx } =
    ↑(decomposeAux f) ↑{ val := 0, property := hx }
case mk.refine'_1
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
hx : 0 ∈ gradeBy R (↑f) i
⊢ ↑(decomposeAux f) ↑{ val := 0, property := hx } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := 0, property := hx }
symm
no goals
case mk.refine'_1
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra R M
hx : 0 ∈ gradeBy R (↑f) i
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := 0, property := hx } =
    ↑(decomposeAux f) ↑{ val := 0, property := hx }
exact AddMonoidHom.map_zero _
case mk.refine'_2
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) i
⊢ ↑(decomposeAux f) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
case mk.refine'_2
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := f_1, property := hx } =
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := f_1, property := hx }) →
          ∀ (hx : Finsupp.single a b + f_1 ∈ gradeBy R (↑f) i),
            ↑(decomposeAux f) ↑{ val := Finsupp.single a b + f_1, property := hx } =
              ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i)
                { val := Finsupp.single a b + f_1, property := hx }
intro m b y hmy hb ih hmby
case mk.refine'_2
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) i
this : Disjoint (Finsupp.single m b).support y.support
⊢ ↑(decomposeAux f) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
case mk.refine'_2
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) i
⊢ ↑(decomposeAux f) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
have : Disjoint (Finsupp.single m b).support y.support := by
  simpa only [Finsupp.support_single_ne_zero _ hb, Finset.disjoint_singleton_left]
case mk.refine'_2
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := 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) ↑{ val := Finsupp.single m b + y, property := hmby✝ } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby✝ }
case mk.refine'_2
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) i
this : Disjoint (Finsupp.single m b).support y.support
⊢ ↑(decomposeAux f) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
rw [mem_gradeBy_iff, Finsupp.support_add_eq this, Finset.coe_union, Set.union_subset_iff]
  at hmby
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := 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) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
case mk.refine'_2
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := 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) ↑{ val := Finsupp.single m b + y, property := hmby✝ } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby✝ }
cases' hmby with h1 h2
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := 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) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := 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) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
have : f m = i := by
  rwa [Finsupp.support_single_ne_zero _ hb, Finset.coe_singleton, Set.singleton_subset_iff]
    at h1
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := 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) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := Finsupp.single m b + y, property := hmby }
subst this
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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 => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
        { val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
      ↑(decomposeAux f) y =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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) ↑{ val := Finsupp.single m b + y, property := hmby } =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
simp only [AlgHom.map_add, Submodule.coe_mk, decomposeAux_single f m]
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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) ↑{ val := y, property := h2 } =
  ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
        { val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
      ↑(decomposeAux f) y =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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 => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
        { val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
      ↑(decomposeAux f) y =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
let ih' := ih h2
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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 => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
        { val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
      ↑(decomposeAux f) y =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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) ↑{ val := y, property := h2 } =
  ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
        { val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
      ↑(decomposeAux f) y =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
dsimp at ih'
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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 => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
      ({ val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
        { val := y, property := h2 }) =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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 => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
        { val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
      ↑(decomposeAux f) y =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
rw [ih', ← AddMonoidHom.map_add]
case mk.refine'_2.intro.h
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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 => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ GradedMonoid.mk (↑f m)
      ({ val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
        { val := y, property := h2 }) =
    GradedMonoid.mk (↑f m) { val := Finsupp.single m b + y, property := hmby }
case mk.refine'_2.intro
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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 => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m))
      ({ val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
        { val := y, property := h2 }) =
    ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := Finsupp.single m b + y, property := hmby }
apply DirectSum.of_eq_of_gradedMonoid_eq
no goals
case mk.refine'_2.intro.h
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := 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 => { x // x ∈ gradeBy R (↑f) i }) (↑f m)) { val := y, property := h2 } :=
  ih h2
⊢ GradedMonoid.mk (↑f m)
      ({ val := Finsupp.single m b, property := (_ : Finsupp.single m b ∈ gradeBy R (↑f) (↑f m)) } +
        { val := y, property := h2 }) =
    GradedMonoid.mk (↑f m) { val := Finsupp.single m b + y, property := hmby }
congr 2
no goals
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := hx }
hmby : Finsupp.single m b + y ∈ gradeBy R (↑f) i
⊢ Disjoint (Finsupp.single m b).support y.support
simpa only [Finsupp.support_single_ne_zero _ hb, Finset.disjoint_singleton_left]
no goals
M : Type u_1
ι : Type u_3
R : Type u_2
inst✝⁴ : DecidableEq M
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : AddMonoidAlgebra 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) ↑{ val := y, property := hx } =
      ↑(DirectSum.of (fun i => { x // x ∈ gradeBy R (↑f) i }) i) { val := y, property := 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
rwa [Finsupp.support_single_ne_zero _ hb, Finset.coe_singleton, Set.singleton_subset_iff]
  at h1