[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
⊢ x /ᵒᶠ 0 = x
[PROOFSTEP]
refine
  Finsupp.ext fun _ =>
    ?_
      -- porting note: `ext` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ↑(x /ᵒᶠ 0) x✝ = ↑x x✝
[PROOFSTEP]
simp only [AddMonoidAlgebra.divOf_apply, zero_add]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a b : G
⊢ x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b
[PROOFSTEP]
refine
  Finsupp.ext fun _ =>
    ?_
      -- porting note: `ext` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a b x✝ : G
⊢ ↑(x /ᵒᶠ (a + b)) x✝ = ↑(x /ᵒᶠ a /ᵒᶠ b) x✝
[PROOFSTEP]
simp only [AddMonoidAlgebra.divOf_apply, add_assoc]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
⊢ of' k G a * x /ᵒᶠ a = x
[PROOFSTEP]
refine
  Finsupp.ext fun _ =>
    ?_
      -- porting note: `ext` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ↑(of' k G a * x /ᵒᶠ a) x✝ = ↑x x✝
[PROOFSTEP]
rw [AddMonoidAlgebra.divOf_apply, of'_apply, single_mul_apply_aux, one_mul]
[GOAL]
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ∀ (a_1 : G), a + a_1 = a + x✝ ↔ a_1 = x✝
[PROOFSTEP]
intro c
[GOAL]
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ c : G
⊢ a + c = a + x✝ ↔ c = x✝
[PROOFSTEP]
exact add_right_inj _
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a : G
⊢ x * of' k G a /ᵒᶠ a = x
[PROOFSTEP]
refine
  Finsupp.ext fun _ =>
    ?_
      -- porting note: `ext` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a x✝ : G
⊢ ↑(x * of' k G a /ᵒᶠ a) x✝ = ↑x x✝
[PROOFSTEP]
rw [AddMonoidAlgebra.divOf_apply, of'_apply, mul_single_apply_aux, mul_one]
[GOAL]
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a x✝ : G
⊢ ∀ (a_1 : G), a_1 + a = a + x✝ ↔ a_1 = x✝
[PROOFSTEP]
intro c
[GOAL]
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a x✝ c : G
⊢ c + a = a + x✝ ↔ c = x✝
[PROOFSTEP]
rw [add_comm]
[GOAL]
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a x✝ c : G
⊢ a + c = a + x✝ ↔ c = x✝
[PROOFSTEP]
exact add_right_inj _
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
⊢ of' k G a /ᵒᶠ a = 1
[PROOFSTEP]
simpa only [one_mul] using mul_of'_divOf (1 : AddMonoidAlgebra k G) a
[GOAL]
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
⊢ ¬¬∃ g₂, g' = g + g₂
[PROOFSTEP]
rwa [Classical.not_not]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
⊢ of' k G g * x %ᵒᶠ g = 0
[PROOFSTEP]
refine
  Finsupp.ext fun g' =>
    ?_
      -- porting note: `ext g'` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
g' : G
⊢ ↑(of' k G g * x %ᵒᶠ g) g' = ↑0 g'
[PROOFSTEP]
rw [Finsupp.zero_apply]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
g' : G
⊢ ↑(of' k G g * x %ᵒᶠ g) g' = 0
[PROOFSTEP]
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
[GOAL]
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
d : G
⊢ ↑(of' k G g * x %ᵒᶠ g) (g + d) = 0
[PROOFSTEP]
rw [modOf_apply_self_add]
[GOAL]
case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
g' : G
h : ¬∃ d, g' = g + d
⊢ ↑(of' k G g * x %ᵒᶠ g) g' = 0
[PROOFSTEP]
rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ x * of' k G g %ᵒᶠ g = 0
[PROOFSTEP]
refine
  Finsupp.ext fun g' =>
    ?_
      -- porting note: `ext g'` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = ↑0 g'
[PROOFSTEP]
rw [Finsupp.zero_apply]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = 0
[PROOFSTEP]
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
[GOAL]
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(x * of' k G g %ᵒᶠ g) (g + d) = 0
[PROOFSTEP]
rw [modOf_apply_self_add]
[GOAL]
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
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = 0
[PROOFSTEP]
rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, mul_single_apply_of_not_exists_add]
[GOAL]
case inr.h
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
⊢ ¬∃ d, g' = d + g
[PROOFSTEP]
simpa only [add_comm] using h
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
⊢ of' k G g %ᵒᶠ g = 0
[PROOFSTEP]
simpa only [one_mul] using mul_of'_modOf (1 : AddMonoidAlgebra k G) g
[GOAL]
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
[PROOFSTEP]
refine
  Finsupp.ext fun g' =>
    ?_
      -- porting note: `ext` doesn't work
[GOAL]
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'
[PROOFSTEP]
rw [Finsupp.add_apply]
  -- porting note: changed from `simp_rw` which can't see through the type
[GOAL]
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'
[PROOFSTEP]
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
[GOAL]
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'
[PROOFSTEP]
swap
[GOAL]
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'
[PROOFSTEP]
rw [modOf_apply_of_not_exists_add x _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h, zero_add]
[GOAL]
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)
[PROOFSTEP]
rw [modOf_apply_self_add, add_zero]
[GOAL]
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)
[PROOFSTEP]
rw [of'_apply, single_mul_apply_aux _ _ _, one_mul, divOf_apply]
[GOAL]
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
[PROOFSTEP]
intro a
[GOAL]
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
[PROOFSTEP]
exact add_right_inj _
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x
[PROOFSTEP]
rw [add_comm, divOf_add_modOf]
[GOAL]
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 ↔ x %ᵒᶠ g = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
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 → x %ᵒᶠ g = 0
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case mp.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
⊢ of' k G g * x %ᵒᶠ g = 0
[PROOFSTEP]
rw [of'_mul_modOf]
[GOAL]
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x
[PROOFSTEP]
intro h
[GOAL]
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ x
[PROOFSTEP]
rw [← divOf_add_modOf x g, h, add_zero]
[GOAL]
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ of' k G g * (x /ᵒᶠ g)
[PROOFSTEP]
exact dvd_mul_right _ _
