[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Nontrivial R
i j : ℕ
⊢ ↑(monomial i) 1 = ↑(monomial j) 1 ↔ i = j
[PROOFSTEP]
simp_rw [← ofFinsupp_single, ofFinsupp.injEq]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Nontrivial R
i j : ℕ
⊢ Finsupp.single i 1 = Finsupp.single j 1 ↔ i = j
[PROOFSTEP]
exact AddMonoidAlgebra.of_injective.eq_iff
[GOAL]
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Nontrivial R
m n : ℕ
h : (fun i => ↑(monomial i) 1) m = (fun i => ↑(monomial i) 1) n
⊢ m = n
[PROOFSTEP]
simpa [monomial_one_eq_iff] using h
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
⊢ Finset.card (support f) ≤ 1 ↔ ∃ n a, f = ↑(monomial n) a
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
⊢ Finset.card (support f) ≤ 1 → ∃ n a, f = ↑(monomial n) a
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
H : Finset.card (support f) ≤ 1
⊢ ∃ n a, f = ↑(monomial n) a
[PROOFSTEP]
rw [Finset.card_le_one_iff_subset_singleton] at H 
[GOAL]
case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
H : ∃ x, support f ⊆ {x}
⊢ ∃ n a, f = ↑(monomial n) a
[PROOFSTEP]
rcases H with ⟨n, hn⟩
[GOAL]
case mp.intro
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
⊢ ∃ n a, f = ↑(monomial n) a
[PROOFSTEP]
refine' ⟨n, f.coeff n, _⟩
[GOAL]
case mp.intro
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
⊢ f = ↑(monomial n) (coeff f n)
[PROOFSTEP]
ext i
[GOAL]
case mp.intro.a
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
[PROOFSTEP]
by_cases hi : i = n
[GOAL]
case pos
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : i = n
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
[PROOFSTEP]
simp [hi, coeff_monomial]
[GOAL]
case neg
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
[PROOFSTEP]
have : f.coeff i = 0 := by
  rw [← not_mem_support_iff]
  exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ coeff f i = 0
[PROOFSTEP]
rw [← not_mem_support_iff]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ ¬i ∈ support f
[PROOFSTEP]
exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))
[GOAL]
case neg
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
this : coeff f i = 0
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
[PROOFSTEP]
simp [this, Ne.symm hi, coeff_monomial]
[GOAL]
case mpr
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
⊢ (∃ n a, f = ↑(monomial n) a) → Finset.card (support f) ≤ 1
[PROOFSTEP]
rintro ⟨n, a, rfl⟩
[GOAL]
case mpr.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ Finset.card (support (↑(monomial n) a)) ≤ 1
[PROOFSTEP]
rw [← Finset.card_singleton n]
[GOAL]
case mpr.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ Finset.card (support (↑(monomial n) a)) ≤ Finset.card {n}
[PROOFSTEP]
apply Finset.card_le_of_subset
[GOAL]
case mpr.intro.intro.a
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ support (↑(monomial n) a) ⊆ {n}
[PROOFSTEP]
exact support_monomial' _ _
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
⊢ f = g
[PROOFSTEP]
set f' := f.comp (toFinsuppIso R).symm.toRingHom with hf'
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ f = g
[PROOFSTEP]
set g' := g.comp (toFinsuppIso R).symm.toRingHom with hg'
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ f = g
[PROOFSTEP]
have A : f' = g' := by
  -- Porting note: Was `ext; simp [..]; simpa [..] using h₂`.
  ext : 1
  · ext
    simp [h₁, RingEquiv.toRingHom_eq_coe]
  · refine MonoidHom.ext_mnat ?_
    simpa [RingEquiv.toRingHom_eq_coe] using h₂
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ f' = g'
[PROOFSTEP]
ext : 1
[GOAL]
case h₁
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ RingHom.comp f' AddMonoidAlgebra.singleZeroRingHom = RingHom.comp g' AddMonoidAlgebra.singleZeroRingHom
[PROOFSTEP]
ext
[GOAL]
case h₁.a
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
x✝ : R
⊢ ↑(RingHom.comp f' AddMonoidAlgebra.singleZeroRingHom) x✝ = ↑(RingHom.comp g' AddMonoidAlgebra.singleZeroRingHom) x✝
[PROOFSTEP]
simp [h₁, RingEquiv.toRingHom_eq_coe]
[GOAL]
case h_of
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ MonoidHom.comp (↑f') (AddMonoidAlgebra.of R ℕ) = MonoidHom.comp (↑g') (AddMonoidAlgebra.of R ℕ)
[PROOFSTEP]
refine MonoidHom.ext_mnat ?_
[GOAL]
case h_of
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ ↑(MonoidHom.comp (↑f') (AddMonoidAlgebra.of R ℕ)) (↑Multiplicative.ofAdd 1) =
    ↑(MonoidHom.comp (↑g') (AddMonoidAlgebra.of R ℕ)) (↑Multiplicative.ofAdd 1)
[PROOFSTEP]
simpa [RingEquiv.toRingHom_eq_coe] using h₂
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
⊢ f = g
[PROOFSTEP]
have B : f = f'.comp (toFinsuppIso R) := by
  rw [hf', RingHom.comp_assoc]
  ext x
  simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply, RingHom.coe_comp,
    RingEquiv.coe_toRingHom]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
⊢ f = RingHom.comp f' ↑(toFinsuppIso R)
[PROOFSTEP]
rw [hf', RingHom.comp_assoc]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
⊢ f = RingHom.comp f (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R))) ↑(toFinsuppIso R))
[PROOFSTEP]
ext x
[GOAL]
case a
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
x : R[X]
⊢ ↑f x = ↑(RingHom.comp f (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R))) ↑(toFinsuppIso R))) x
[PROOFSTEP]
simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply, RingHom.coe_comp,
  RingEquiv.coe_toRingHom]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = RingHom.comp f' ↑(toFinsuppIso R)
⊢ f = g
[PROOFSTEP]
have C' : g = g'.comp (toFinsuppIso R) := by
  rw [hg', RingHom.comp_assoc]
  ext x
  simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply, RingHom.coe_comp,
    RingEquiv.coe_toRingHom]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = RingHom.comp f' ↑(toFinsuppIso R)
⊢ g = RingHom.comp g' ↑(toFinsuppIso R)
[PROOFSTEP]
rw [hg', RingHom.comp_assoc]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = RingHom.comp f' ↑(toFinsuppIso R)
⊢ g = RingHom.comp g (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R))) ↑(toFinsuppIso R))
[PROOFSTEP]
ext x
[GOAL]
case a
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = RingHom.comp f' ↑(toFinsuppIso R)
x : R[X]
⊢ ↑g x = ↑(RingHom.comp g (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R))) ↑(toFinsuppIso R))) x
[PROOFSTEP]
simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply, RingHom.coe_comp,
  RingEquiv.coe_toRingHom]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = RingHom.comp f' ↑(toFinsuppIso R)
C' : g = RingHom.comp g' ↑(toFinsuppIso R)
⊢ f = g
[PROOFSTEP]
rw [B, C', A]
