k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g) g' = ↑x g'
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x
refine Finsupp.ext fun g' => ?_
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) g' + ↑(x %ᵒᶠ g) g' = ↑x g'
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g) g' = ↑x g'
rw [Finsupp.add_apply]
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) (g + d) + ↑(x %ᵒᶠ g) (g + d) = ↑x (g + d)

case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ↑(of' k G g * (x /ᵒᶠ g)) g' + ↑(x %ᵒᶠ g) g' = ↑x g'
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) g' + ↑(x %ᵒᶠ g) g' = ↑x g'
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ↑(of' k G g * (x /ᵒᶠ g)) g' + ↑(x %ᵒᶠ g) g' = ↑x g'

case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) (g + d) + ↑(x %ᵒᶠ g) (g + d) = ↑x (g + d)
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) (g + d) + ↑(x %ᵒᶠ g) (g + d) = ↑x (g + d)

case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ↑(of' k G g * (x /ᵒᶠ g)) g' + ↑(x %ᵒᶠ g) g' = ↑x g'
swap
no goals
case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ↑(of' k G g * (x /ᵒᶠ g)) g' + ↑(x %ᵒᶠ g) g' = ↑x g'
rw [modOf_apply_of_not_exists_add x _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h,
  zero_add]
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) (g + d) = ↑x (g + d)
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) (g + d) + ↑(x %ᵒᶠ g) (g + d) = ↑x (g + d)
rw [modOf_apply_self_add, add_zero]
case inl.intro.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ∀ (a : G), g + a = g + d ↔ a = d
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) (g + d) = ↑x (g + d)
rw [of'_apply, single_mul_apply_aux _ _ _, one_mul, divOf_apply]
case inl.intro.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d a : G
⊢ g + a = g + d ↔ a = d
case inl.intro.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ∀ (a : G), g + a = g + d ↔ a = d
intro a
no goals
case inl.intro.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d a : G
⊢ g + a = g + d ↔ a = d
exact add_right_inj _