case intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
M : Type u_1
inst✝ : AddMonoid M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), ↑f (↑(monomial n) a) = ↑g (↑(monomial n) a)
n : ℕ
a : R
⊢ ↑f (↑(monomial n) a) = ↑g (↑(monomial n) a)
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
M : Type u_1
inst✝ : AddMonoid M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), ↑f (↑(monomial n) a) = ↑g (↑(monomial n) a)
⊢ Set.EqOn ↑f ↑g {p | ∃ n a, p = ↑(monomial n) a}
rintro p ⟨n, a, rfl⟩
no goals
case intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
M : Type u_1
inst✝ : AddMonoid M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), ↑f (↑(monomial n) a) = ↑g (↑(monomial n) a)
n : ℕ
a : R
⊢ ↑f (↑(monomial n) a) = ↑g (↑(monomial n) a)
exact h n a